Package Details: ssreflect 1.6.1-4

Git Clone URL: https://aur.archlinux.org/ssreflect.git (read-only)
Package Base: ssreflect
Description: The ssreflect unit of the mathematical components library for Coq.
Upstream URL: https://math-comp.github.io/math-comp/
Licenses: GPL
Submitter: mboes
Maintainer: wilbowma
Last Packager: wilbowma
Votes: 10
Popularity: 0.107599
First Submitted: 2010-02-19 13:35
Last Updated: 2017-02-08 22:47

Dependencies (3)

Required by (0)

Sources (1)

Latest Comments

wilbowma commented on 2017-05-08 21:14

@kaptoxic, sorry I can't reproduce and I don't recognize the error message.

kaptoxic commented on 2017-05-05 18:13

I am getting an error during build, any ideas? (Coq 8.6 should be supported.)

Error:
COQC ssreflect.v
File "./ssreflect.v", line 5, characters 0-37:
Error: while loading
/tmp/yaourt-tmp-user/aur-ssreflect/src/math-comp-math-comp-b4510cb/mathcomp/ssreflect/ssreflect_plugin.cmxs:
implementation mismatch on Unix
make[1]: *** [Makefile.coq:436: ssreflect.vo] Error 1
make: *** [Makefile:26: all] Error 2

pmates commented on 2014-07-03 10:24

For users having problems installing this, I recommend rebuilding several of the dependencies using the following modifications:
- when building camlp5-transitional add "options=('staticlibs')" to the PKGBUILD file
- when building coq edit the PKGBUILD file to use the 'usecamlp5' flag instead of 'usecamlp4'
- when building ssreflect modify the download location, as mentioned by daoo, and if you have coq 8.4pl4-1 you will have to remove the coq>=8.4 dependency since makepkg gets confused.

Anonymous comment on 2013-04-18 17:25

The download location seems to have changed to:

https://gforge.inria.fr/frs/download.php/31453/ssreflect-1.4-coq8.4.tar.gz

I think inria has redone their entire site and it looks like the downloads were moved in the process.

Also there is a project file list here:

https://gforge.inria.fr/frs/?group_id=401

mboes commented on 2012-12-22 00:56

Hi jbj, thanks for the report. Fixed.

jbj commented on 2012-11-20 15:12

I had to add a trailing slash in the "make install" line to make the files go in /usr/lib/coq/user-contrib instead of /usr/lib/coquser-contrib. Coq couldn't find them in the latter location.

So replace
make DESTDIR=$pkgdir 'COQLIB:=$(DESTDIR)/$(shell coqtop -where)' install
with
make DESTDIR=$pkgdir 'COQLIB:=$(DESTDIR)/$(shell coqtop -where)/' install

mboes commented on 2012-03-21 15:39

Thanks chneukirchen. Updated the PKGBUILD. Apparently Camlp5 made an API breaking change somewhere between 6.03 and 6.05.

chneukirchen commented on 2012-03-20 15:31

PKGBUILD is missing makedepends=('camlp5-transitional') and then needs sed -i s/Stdpp/Compat/ src/ssreflect.ml to build. Also, || return 1 is superflous.

Updated PKGBUILD: http://sprunge.us/aLej

Anonymous comment on 2011-11-22 18:31

New version is out : http://www.msr-inria.inria.fr/Projects/math-components/ssreflect-1.3pl2.tar.gz
But I have the same problem :
Error while loading "/usr/lib/coq/parsing/grammar.cma": interface mismatch on MLast.
Error while loading "/usr/lib/coq/parsing/grammar.cma": interface mismatch on MLast.
File "src/ssreflect.ml", line 1, characters 0-1:
File "src/ssreflect.ml", line 1, characters 0-1:
Error: Preprocessor error
Error: Preprocessor error

I have this problem with the AUR version of SSReflect and the new version (1.3pl2)...

mboes commented on 2011-10-11 03:03

Works for me, with both pl1 and pl2. Make sure that your installed ocaml compiler, the compiler used to compile coq, and the compiler used to compile ssreflect all have matching versions.

All comments