Ssreflect Users Discussion List

[Georges Gonthier <>]

  This is an error you can probably ignore: you successfully built the ssrcoq 
binary and compiled all the theories. For some curious reason, you could not 
manage to make a bytecode image of ssreflect: Coq attempted to load a 
statically linked library as a dynamically linked one. Since you probably 
don't want to be running a bytecode system anyway (Coq being already 
painfully slow at times), you can simply remove the corresponding entry in 
the Makefile.

Georges

-----Original Message-----
From:  [] On Behalf Of 
Derek Dreyer
Sent: 11 November 2009 16:38
To: Yves Bertot
Cc: Georges Gonthier; 
Subject: Re: trouble installing ssreflect v1.2 on Mac 10.5

I'm afraid I gave up on trying to make the binary version work.  I
went ahead and used macports to compile from source.  In the process,
it gave me a new version of ocaml (3.11.1) and ocamlp5 (5.12).  (This
turned out to be quite annoying, because the binary version of Coq had
installed itself in the Macports directories without informing
Macports of this, and Macports wouldn't let me install Coq 8.2p1 until
I manually cleaned out the 8.2p0 binaries, etc.)

Anyway, with Coq 8.2p1 in place, the ssreflect compilation got much
farther this time, but still resulted in an error (see below):

ld: absolute addressing (perhaps -mdynamic-no-pic) used in
_caml_curry11 from src/ssreflect.cmxs.startup.o not allowed in
slidable image
collect2: ld returned 1 exit status
File "caml_startup", line 1, characters 0-1:
Error: Error during linking

Again, any help would be appreciated.

Thanks,
Derek

lebowski:~/tmp/ssreflect-1.2 $ make
/opt/local/bin/ocamldep -slash -I /opt/local/lib/coq/kernel -I
/opt/local/lib/coq/lib -I /opt/local/lib/coq/library -I
/opt/local/lib/coq/parsing -I /opt/local/lib/coq/pretyping -I
/opt/local/lib/coq/interp -I /opt/local/lib/coq/proofs -I
/opt/local/lib/coq/tactics -I /opt/local/lib/coq/toplevel -I
/opt/local/lib/coq/contrib/cc -I /opt/local/lib/coq/contrib/dp -I
/opt/local/lib/coq/contrib/extraction -I
/opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml -I
theories -pp "/opt/local/bin/"camlp5"o -I . -I
/opt/local/lib/coq/kernel -I /opt/local/lib/coq/lib -I
/opt/local/lib/coq/library -I /opt/local/lib/coq/parsing -I
/opt/local/lib/coq/pretyping -I /opt/local/lib/coq/interp -I
/opt/local/lib/coq/proofs -I /opt/local/lib/coq/tactics -I
/opt/local/lib/coq/toplevel -I /opt/local/lib/coq/contrib/cc -I
/opt/local/lib/coq/contrib/dp -I /opt/local/lib/coq/contrib/extraction
-I /opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml
pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl"
"src/ssreflect.ml" > "src/ssreflect.ml.d"
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/zmodp.v"
> "theories/zmodp.v.d" || ( RV=$?; rm -f "theories/zmodp.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/tuple.v"
> "theories/tuple.v.d" || ( RV=$?; rm -f "theories/tuple.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/ssrnat.v"
> "theories/ssrnat.v.d" || ( RV=$?; rm -f "theories/ssrnat.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/ssrfun.v"
> "theories/ssrfun.v.d" || ( RV=$?; rm -f "theories/ssrfun.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/ssreflect.v" > "theories/ssreflect.v.d" || ( RV=$?; rm -f
"theories/ssreflect.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/ssrbool.v" > "theories/ssrbool.v.d" || ( RV=$?; rm -f
"theories/ssrbool.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/ssralg.v"
> "theories/ssralg.v.d" || ( RV=$?; rm -f "theories/ssralg.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/seq.v" >
"theories/seq.v.d" || ( RV=$?; rm -f "theories/seq.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/prime.v"
> "theories/prime.v.d" || ( RV=$?; rm -f "theories/prime.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/poly.v" >
"theories/poly.v.d" || ( RV=$?; rm -f "theories/poly.v.d"; exit ${RV}
)
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/perm.v" >
"theories/perm.v.d" || ( RV=$?; rm -f "theories/perm.v.d"; exit ${RV}
)
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/paths.v"
> "theories/paths.v.d" || ( RV=$?; rm -f "theories/paths.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/normal.v"
> "theories/normal.v.d" || ( RV=$?; rm -f "theories/normal.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/morphisms.v" > "theories/morphisms.v.d" || ( RV=$?; rm -f
"theories/morphisms.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/matrix.v"
> "theories/matrix.v.d" || ( RV=$?; rm -f "theories/matrix.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/groups.v"
> "theories/groups.v.d" || ( RV=$?; rm -f "theories/groups.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/fintype.v" > "theories/fintype.v.d" || ( RV=$?; rm -f
"theories/fintype.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/finset.v"
> "theories/finset.v.d" || ( RV=$?; rm -f "theories/finset.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/finfun.v"
> "theories/finfun.v.d" || ( RV=$?; rm -f "theories/finfun.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/eqtype.v"
> "theories/eqtype.v.d" || ( RV=$?; rm -f "theories/eqtype.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/div.v" >
"theories/div.v.d" || ( RV=$?; rm -f "theories/div.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/cyclic.v"
> "theories/cyclic.v.d" || ( RV=$?; rm -f "theories/cyclic.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/connect.v" > "theories/connect.v.d" || ( RV=$?; rm -f
"theories/connect.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/choice.v"
> "theories/choice.v.d" || ( RV=$?; rm -f "theories/choice.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/charpoly.v" > "theories/charpoly.v.d" || ( RV=$?; rm -f
"theories/charpoly.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/binomial.v" > "theories/binomial.v.d" || ( RV=$?; rm -f
"theories/binomial.v.d"; exit ${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories  "theories/bigops.v"
> "theories/bigops.v.d" || ( RV=$?; rm -f "theories/bigops.v.d"; exit
${RV} )
/opt/local/bin/coqdep -c -glob -slash -I theories
"theories/automorphism.v" > "theories/automorphism.v.d" || ( RV=$?; rm
-f "theories/automorphism.v.d"; exit ${RV} )
/opt/local/bin/ocamlopt.opt -c -rectypes  -I theories -I
/opt/local/lib/coq/kernel -I /opt/local/lib/coq/lib -I
/opt/local/lib/coq/library -I /opt/local/lib/coq/parsing -I
/opt/local/lib/coq/pretyping -I /opt/local/lib/coq/interp -I
/opt/local/lib/coq/proofs -I /opt/local/lib/coq/tactics -I
/opt/local/lib/coq/toplevel -I /opt/local/lib/coq/contrib/cc -I
/opt/local/lib/coq/contrib/dp -I /opt/local/lib/coq/contrib/extraction
-I /opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml -I
/opt/local/lib/ocaml/camlp5 -pp "/opt/local/bin/"camlp5"o -I . -I
/opt/local/lib/coq/kernel -I /opt/local/lib/coq/lib -I
/opt/local/lib/coq/library -I /opt/local/lib/coq/parsing -I
/opt/local/lib/coq/pretyping -I /opt/local/lib/coq/interp -I
/opt/local/lib/coq/proofs -I /opt/local/lib/coq/tactics -I
/opt/local/lib/coq/toplevel -I /opt/local/lib/coq/contrib/cc -I
/opt/local/lib/coq/contrib/dp -I /opt/local/lib/coq/contrib/extraction
-I /opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml
pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl"
src/ssreflect.ml
/opt/local/bin/coqmktop -opt -o bin/ssrcoq src/ssreflect.cmx
bin/ssrcoq -q  -I theories    -compile theories/ssreflect
Defining 'is' as keyword
Defining 'by' as keyword
Defining 'of' as keyword
Defining 'nosimpl' as keyword
bin/ssrcoq -q  -I theories    -compile theories/ssrfun
bin/ssrcoq -q  -I theories    -compile theories/ssrbool
bin/ssrcoq -q  -I theories    -compile theories/eqtype
bin/ssrcoq -q  -I theories    -compile theories/ssrnat
bin/ssrcoq -q  -I theories    -compile theories/seq
bin/ssrcoq -q  -I theories    -compile theories/choice
bin/ssrcoq -q  -I theories    -compile theories/fintype
Defining 'forallb' as keyword
Defining 'existsb' as keyword
bin/ssrcoq -q  -I theories    -compile theories/div
bin/ssrcoq -q  -I theories    -compile theories/tuple
bin/ssrcoq -q  -I theories    -compile theories/finfun
bin/ssrcoq -q  -I theories    -compile theories/paths
Defining 'fpath' as keyword
Defining 'fcycle' as keyword
Defining 'ufcycle' as keyword
bin/ssrcoq -q  -I theories    -compile theories/bigops
bin/ssrcoq -q  -I theories    -compile theories/finset
bin/ssrcoq -q  -I theories    -compile theories/groups
bin/ssrcoq -q  -I theories    -compile theories/perm
bin/ssrcoq -q  -I theories    -compile theories/morphisms
bin/ssrcoq -q  -I theories    -compile theories/automorphism
bin/ssrcoq -q  -I theories    -compile theories/prime
bin/ssrcoq -q  -I theories    -compile theories/binomial
bin/ssrcoq -q  -I theories    -compile theories/ssralg
bin/ssrcoq -q  -I theories    -compile theories/zmodp
bin/ssrcoq -q  -I theories    -compile theories/matrix
bin/ssrcoq -q  -I theories    -compile theories/poly
bin/ssrcoq -q  -I theories    -compile theories/charpoly
Defining 'R' as keyword
Defining 'M' as keyword
bin/ssrcoq -q  -I theories    -compile theories/connect
Defining 'fconnect' as keyword
Defining 'froot' as keyword
Defining 'froots' as keyword
Defining 'fcard' as keyword
Defining 'fclosed' as keyword
Defining 'fclosure' as keyword
bin/ssrcoq -q  -I theories    -compile theories/normal
bin/ssrcoq -q  -I theories    -compile theories/cyclic
/opt/local/bin/ocamlc.opt -c -rectypes  -I theories -I
/opt/local/lib/coq/kernel -I /opt/local/lib/coq/lib -I
/opt/local/lib/coq/library -I /opt/local/lib/coq/parsing -I
/opt/local/lib/coq/pretyping -I /opt/local/lib/coq/interp -I
/opt/local/lib/coq/proofs -I /opt/local/lib/coq/tactics -I
/opt/local/lib/coq/toplevel -I /opt/local/lib/coq/contrib/cc -I
/opt/local/lib/coq/contrib/dp -I /opt/local/lib/coq/contrib/extraction
-I /opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml -I
/opt/local/lib/ocaml/camlp5 -pp "/opt/local/bin/"camlp5"o -I . -I
/opt/local/lib/coq/kernel -I /opt/local/lib/coq/lib -I
/opt/local/lib/coq/library -I /opt/local/lib/coq/parsing -I
/opt/local/lib/coq/pretyping -I /opt/local/lib/coq/interp -I
/opt/local/lib/coq/proofs -I /opt/local/lib/coq/tactics -I
/opt/local/lib/coq/toplevel -I /opt/local/lib/coq/contrib/cc -I
/opt/local/lib/coq/contrib/dp -I /opt/local/lib/coq/contrib/extraction
-I /opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml
pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl"
src/ssreflect.ml
/opt/local/bin/ocamlopt.opt -rectypes  -I theories -I
/opt/local/lib/coq/kernel -I /opt/local/lib/coq/lib -I
/opt/local/lib/coq/library -I /opt/local/lib/coq/parsing -I
/opt/local/lib/coq/pretyping -I /opt/local/lib/coq/interp -I
/opt/local/lib/coq/proofs -I /opt/local/lib/coq/tactics -I
/opt/local/lib/coq/toplevel -I /opt/local/lib/coq/contrib/cc -I
/opt/local/lib/coq/contrib/dp -I /opt/local/lib/coq/contrib/extraction
-I /opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml -I
/opt/local/lib/ocaml/camlp5 -shared -o src/ssreflect.cmxs -pp
"/opt/local/bin/"camlp5"o -I . -I /opt/local/lib/coq/kernel -I
/opt/local/lib/coq/lib -I /opt/local/lib/coq/library -I
/opt/local/lib/coq/parsing -I /opt/local/lib/coq/pretyping -I
/opt/local/lib/coq/interp -I /opt/local/lib/coq/proofs -I
/opt/local/lib/coq/tactics -I /opt/local/lib/coq/toplevel -I
/opt/local/lib/coq/contrib/cc -I /opt/local/lib/coq/contrib/dp -I
/opt/local/lib/coq/contrib/extraction -I
/opt/local/lib/coq/contrib/field -I
/opt/local/lib/coq/contrib/firstorder -I
/opt/local/lib/coq/contrib/fourier -I
/opt/local/lib/coq/contrib/funind -I
/opt/local/lib/coq/contrib/interface -I
/opt/local/lib/coq/contrib/micromega -I
/opt/local/lib/coq/contrib/omega -I /opt/local/lib/coq/contrib/ring -I
/opt/local/lib/coq/contrib/romega -I /opt/local/lib/coq/contrib/rtauto
-I /opt/local/lib/coq/contrib/setoid_ring -I
/opt/local/lib/coq/contrib/subtac -I /opt/local/lib/coq/contrib/xml
pa_extend.cmo pa_macro.cmo q_MLast.cmo grammar.cma -loc loc -impl"
src/ssreflect.ml
ld: absolute addressing (perhaps -mdynamic-no-pic) used in
_caml_curry11 from src/ssreflect.cmxs.startup.o not allowed in
slidable image
collect2: ld returned 1 exit status
File "caml_startup", line 1, characters 0-1:
Error: Error during linking
make: *** [src/ssreflect.cmxs] Error 2