Package Details: ssreflect 1.6.1-4

Git Clone URL: (read-only)
Package Base: ssreflect
Description: The ssreflect unit of the mathematical components library for Coq.
Upstream URL:
Licenses: GPL
Submitter: mboes
Maintainer: wilbowma
Last Packager: wilbowma
Votes: 10
Popularity: 0.347878
First Submitted: 2010-02-19 13:35
Last Updated: 2017-02-08 22:47

Dependencies (3)

Required by (0)

Sources (1)

Latest Comments

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:

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:

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
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/ to build. Also, || return 1 is superflous.


Anonymous comment on 2011-11-22 18:31

New version is out :
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/", line 1, characters 0-1:
File "src/", 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.

Anonymous comment on 2011-08-19 18:57

In fact, I reinstalled coq-8.3pl1-2, and this still does not compile (now the interface mismatch is on Ploc, still on the same file).

Anonymous comment on 2011-08-19 18:48

The package does not build with the current Coq version (coq-8.3pl2-2). The error is
"Error while loading "/usr/lib/coq/parsing/grammar.cma": interface mismatch on MLast."

Given that this is most likely an upstream error (because this version of SSReflect is only supposed to work with Coq 8.3pl1), I think you should strengthen the depends (coq=8.3pl1).