Package Details: ssreflect 1.9.0-1

Git Clone URL: https://aur.archlinux.org/ssreflect.git (read-only, click to copy)
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: 0918nobita
Last Packager: wilbowma
Votes: 10
Popularity: 0.000000
First Submitted: 2010-02-19 13:35 (UTC)
Last Updated: 2019-06-30 04:26 (UTC)

Dependencies (2)

Required by (1)

Sources (1)

Latest Comments

1 2 Next › Last »

zorun commented on 2017-07-07 22:35 (UTC)

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 (UTC)

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 (UTC)

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

aspirogrammer commented on 2017-05-05 18:13 (UTC)

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 (UTC)

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.

<deleted-account> commented on 2013-04-18 17:25 (UTC)

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 (UTC)

Hi jbj, thanks for the report. Fixed.

jbj commented on 2012-11-20 15:12 (UTC)

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 (UTC)

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 (UTC)

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