Ssreflect Users Discussion List

[Patrick Hulin <>]

Hi everyone,

I'm having trouble building ssreflect on Mac (10.6).
 I'm getting an interface mismatch error (below), which should mean that
 I'm using the wrong version of something. However, I can't figure out 
what that is - I'm using version 8.3pl2 of Coq with 1.3pl2 of SSReflect.


Iodine-Tablet:ssreflect-1.3pl2 phulin$ make
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
Iodine-Tablet:ssreflect-1.3pl2 phulin$ coqtop -v
The Coq Proof Assistant, version 8.3pl2 (April 2011)
compiled on avr 19 2011 12:29:05 with OCaml 3.12.0
Iodine-Tablet:ssreflect-1.3pl2 phulin$ ocaml -version
The Objective Caml toplevel, version 3.12.0
Iodine-Tablet:ssreflect-1.3pl2 phulin$ camlp5o -v
Camlp5 version 6.02.3 (ocaml 3.12.0)


Thanks,
-Patrick