Ssreflect Users Discussion List

[Beta Ziliani <>]

Hi, Patrick,

I compiled ssreflect 1.3pl1 in a MacOS 10.6 with camlp5 version 5.15,
transitional mode. Try using that version.

Good luck!
Beta

On Fri, Dec 2, 2011 at 4:16 PM, Patrick Hulin <> wrote:
> 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