Ssreflect Users Discussion List

["Lucian M. Patcas" <>]

Hi Beta,

Thanks for your response. The Camlp5 that I used was version 6.02.3. I've just tried with version 5.15 as you suggested, but I'm still getting errors:

src/ssreflect.ml

ld: warning: directory '/usr/local/lib/coq/plugins/groebner' following -L not found
ld: warning: directory '/usr/local/lib/coq/plugins/interface' following -L not found
ld: warning: directory '/usr/local/lib/coq/plugins/subtac/test' following -L not found

ld: absolute addressing (perhaps -mdynamic-no-pic) used in _caml_curry11 from src/ssreflect.cmxs.startup.o not allowed in slidable image. Use '-read_only_relocs suppress' to enable text relocs
collect2: ld returned 1 exit status

File "caml_startup", line 1, characters 0-1:
Error: Error during linking
make[1]: *** [src/ssreflect.cmxs] Error 2
make: *** [all] Error 2

Lucian

On Mon, Sep 19, 2011 at 02:27, Beta Ziliani <> wrote:

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