Package Details: ssreflect 1.9.0-1

Git Clone URL: (read-only, click to copy)
Package Base: ssreflect
Description: The ssreflect unit of the mathematical components library for Coq.
Upstream URL:
Licenses: GPL
Submitter: mboes
Maintainer: None
Last Packager: wilbowma
Votes: 9
Popularity: 0.000000
First Submitted: 2010-02-19 13:35
Last Updated: 2019-06-30 04:26

Dependencies (2)

Required by (1)

Sources (1)

Latest Comments

1 2 Next › Last »

zorun commented on 2017-07-07 22:35

Thanks for the report, I have just rebuilt coq in [community] against ocaml 4.04.1, this fixes the build issue for ssreflect.

@dschoepe please open a bug report on when you encounter this kind of issue!

dschoepe commented on 2017-07-07 20:42

Coq and ssreflect need to be compiled with the same version of the OCaml compiler. You can check whether this is the case using `ocamlc -v` and `coqc -v`. In my case they differed and rebuilding coq from source and the building the ssreflect package fixed the issue for me.

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.)

COQC ssreflect.v
File "./ssreflect.v", line 5, characters 0-37:
Error: while loading
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:

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.