Ssreflect Users Discussion List

[Derek Dreyer <>]

Thanks.  Indeed, the binary and theories were all there, so I'm just
ignoring the error...

Derek

On Wed, Nov 11, 2009 at 5:59 PM, Georges Gonthier
<> wrote:
>  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
>
>