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

« First ‹ Previous 1 2

<deleted-account> commented on 2011-11-22 18:31 (UTC)

New version is out : http://www.msr-inria.inria.fr/Projects/math-components/ssreflect-1.3pl2.tar.gz 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/ssreflect.ml", line 1, characters 0-1: File "src/ssreflect.ml", 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 (UTC)

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.

<deleted-account> commented on 2011-08-19 18:57 (UTC)

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

<deleted-account> commented on 2011-08-19 18:48 (UTC)

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

« First ‹ Previous 1 2