Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi Derek,

I'm afraid your problems are due to a faulty (well, incomplete) binary 
distribution of Coq.
The grammar.cma library is used by the camlp4 preprocessor to compile plugins 
which, like ssreflect, define extensions to the input language of Coq (i.e., 
extending that language can only be done in an extension of the Caml 
language). If it's not included in your binary distribution, then you won't 
be able to compile the ssreflect plugin. You'll have to get hold of the Coq 
source distribution, and recompile all of it so you get a consistent set of 
binaries (you might perhaps also want to file a Coq bug report). 
Alternatively, someone on this list might offer an already-made binary...

   Georges

-----Original Message-----
From:  [] On Behalf Of 
Derek Dreyer
Sent: 11 November 2009 13:34
To: 
Subject: trouble installing ssreflect v1.2 on Mac 10.5

I'm trying to install ssreflect v1.2 on Mac 10.5.  I have Coq v8.2p0,
installed from the Mac binary off the Coq website, which put coq into
/opt/local/bin and /opt/local/lib/coq.  (OCaml is also in
/opt/local/bin.)

I followed the ssreflect installation instructions, setting the
environment variables COQTOP and COQLIB to /opt/local/lib/coq/, and
COQBIN to /opt/local/bin/.

On running coq_makefile, followed by make, I get the error below,
which claims that /opt/local/lib/coq/parsing/grammar.cma is not a
bytecode object file.  Any suggestions would be appreciated.

Thanks,
Derek

valchek:ssreflect-1.2 dreyer$ coq_makefile -f Make -o Makefile
Warning: install target will copy files at the first level of the coq
contributions installation directory; option -R is recommended
valchek:ssreflect-1.2 dreyer$ 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
-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"
Error while loading "/opt/local/lib/coq/parsing/grammar.cma":
/opt/local/lib/coq/parsing/grammar.cma is not a bytecode object file.
Preprocessing error on file src/ssreflect.ml
/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 -rectypes  -I /opt/local/lib/ocaml/camlp5
-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 -c -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
Error while loading "/opt/local/lib/coq/parsing/grammar.cma":
/opt/local/lib/coq/parsing/grammar.cma is not a bytecode object file.
File "src/ssreflect.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [src/ssreflect.cmx] Error 2