Ssreflect Users Discussion List

[Derek Dreyer <>]

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