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: 9
Popularity: 0.002820
First Submitted: 2010-02-19 13:35
Last Updated: 2017-02-08 22:47

Dependencies (3)

Required by (1)

Sources (1)

Latest Comments

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 https://www.archlinux.org/packages/community/x86_64/coq/ 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.)

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

All comments