Arch Linux User Repository

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!

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.

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

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

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.

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

Hi jbj, thanks for the report. Fixed.

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

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

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