Ssreflect Users Discussion List

[Georges Gonthier <>]

  From the diagnostic, there is: a cma file should be a bytecode library. I 
guess your Caml/Camlp5 version disagrees with the one with which the binary 
distribution was made (though the install should have diagnosed this).

Georges

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

Hrm, it's hard to believe the only Mac binary file available on the
Coq website is broken, but perhaps you're right.

Btw, the file /opt/local/lib/coq/parsing/grammar.cma exists.  Is there
just something wrong with it?

Derek

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