Ssreflect Users Discussion List

[Beta Ziliani <>]

Lucian,

To compile Ssreflect it's important to have the right version of camlp5. In my case (also an MacOS 10.6.8), the version that worked for me was camlp5 5.15

Hope it helps,
Beta

On Mon, Sep 19, 2011 at 8:15 AM, Lucian M. Patcas <> wrote:

Hello,

I've tried to compile Ssreflect 1.3pl1 on Mac without success. Here are some details:

MacOS 10.6.8
Ocaml 3.12.0 binary distribution
camlp5
Coq 8.3pl2 binary distribution

The output of make is the following:

mkdir -p bin
make -f Makefile.coq all
ocamlc.opt -c -rectypes  -I src -I /usr/local/lib/coq/kernel -I /usr/local/lib/coq/lib -I /usr/local/lib/coq/library -I /usr/local/lib/coq/parsing -I /usr/local/lib/coq/pretyping -I /usr/local/lib/coq/interp -I /usr/local/lib/coq/proofs -I /usr/local/lib/coq/tactics -I /usr/local/lib/coq/toplevel -I /usr/local/lib/coq/plugins/cc -I /usr/local/lib/coq/plugins/dp -I /usr/local/lib/coq/plugins/extraction -I /usr/local/lib/coq/plugins/field -I /usr/local/lib/coq/plugins/firstorder -I /usr/local/lib/coq/plugins/fourier -I /usr/local/lib/coq/plugins/funind -I /usr/local/lib/coq/plugins/groebner -I /usr/local/lib/coq/plugins/interface -I /usr/local/lib/coq/plugins/micromega -I /usr/local/lib/coq/plugins/nsatz -I /usr/local/lib/coq/plugins/omega -I /usr/local/lib/coq/plugins/quote -I /usr/local/lib/coq/plugins/ring -I /usr/local/lib/coq/plugins/romega -I /usr/local/lib/coq/plugins/rtauto -I /usr/local/lib/coq/plugins/setoid_ring -I /usr/local/lib/coq/plugins/subtac -I /usr/local/lib/coq/plugins/subtac/test -I /usr/local/lib/coq/plugins/syntax -I /usr/local/lib/coq/plugins/xml -I /usr/local/lib/ocaml/camlp5 -pp ""camlp5"o -I /usr/local/lib/ocaml -I . -I /usr/local/lib/coq/kernel -I /usr/local/lib/coq/lib -I /usr/local/lib/coq/library -I /usr/local/lib/coq/parsing -I /usr/local/lib/coq/pretyping -I /usr/local/lib/coq/interp -I /usr/local/lib/coq/proofs -I /usr/local/lib/coq/tactics -I /usr/local/lib/coq/toplevel -I /usr/local/lib/coq/plugins/cc -I /usr/local/lib/coq/plugins/dp -I /usr/local/lib/coq/plugins/extraction -I /usr/local/lib/coq/plugins/field -I /usr/local/lib/coq/plugins/firstorder -I /usr/local/lib/coq/plugins/fourier -I /usr/local/lib/coq/plugins/funind -I /usr/local/lib/coq/plugins/groebner -I /usr/local/lib/coq/plugins/interface -I /usr/local/lib/coq/plugins/micromega -I /usr/local/lib/coq/plugins/nsatz -I /usr/local/lib/coq/plugins/omega -I /usr/local/lib/coq/plugins/quote -I /usr/local/lib/coq/plugins/ring -I /usr/local/lib/coq/plugins/romega -I /usr/local/lib/coq/plugins/rtauto -I /usr/local/lib/coq/plugins/setoid_ring -I /usr/local/lib/coq/plugins/subtac -I /usr/local/lib/coq/plugins/subtac/test -I /usr/local/lib/coq/plugins/syntax -I /usr/local/lib/coq/plugins/xml pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl" src/ssreflect.ml
Error while loading "/usr/local/lib/coq/parsing/grammar.cma": interface mismatch on Plexing.
File "src/ssreflect.ml", line 1, characters 0-1:
Error: Preprocessor error
make[1]: *** [src/ssreflect.cmo] Error 2
make: *** [all] Error 2

Any help is much appreciated.

Thank you,
Lucian