The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi,

I'm trying to compile Coq 8.2pl1 on Mac OS X (10.5.7) and am getting  
an error during compilation. I've configured it using

> ./configure -local -fsets basic -reals basic -coqide no -with-doc no  
> -debug

(Also tried with -opt option, with same result). Running make world  
stops with

> CAMLP4DEPS test.ml4
> Testing parsing/grammar.cma
> Error while loading "config/coq_config.cmo": config/coq_config.cmo  
> is not a bytecode object file.
> File "test.ml4", line 1, characters 0-1:
> Error: Preprocessor error
> make[1]: *** [parsing/grammar.cma] Error 2
> make: *** [stage1] Error 2

(The corresponding verbose output is at the end of this mail). The  
file config/coq_config.cmo does exist, and 'file' returns:

> # file config/coq_config.cmo
> config/coq_config.cmo: Objective caml object file (.cmo) (Version  
> 007).

Interestingly, simply removing this file gives the exact same error (?).

Ocaml itself is installed through macports:

> # ocaml -version
> The Objective Caml toplevel, version 3.11.1
>
> # camlp5 -v
> Camlp5 version 5.11 (ocaml 3.11.0)

I thought that maybe the camlp5 version was the problem (although I  
managed to compile Coq on a different machine, also running Mac OS X,  
with the same versions of ocamlc and camlp5 -- not sure what the  
differences between the two machines are, except that the machine on  
which it worked is an old PowerPC PowerBook and the machine on which  
it breaks is a much newer Intel iBook :-/ ), so I installed the latest  
version of 5.12 manually:

> # camlp5 -v
> Camlp5 version 5.12 (ocaml 3.11.1)

Compilation (starting from a clean slate) now gives a different error  
message:

> CAMLP4DEPS test.ml4
> Testing parsing/grammar.cma
> Error while loading "parsing/argextend.cmo": interface mismatch on  
> Pcaml.
> File "test.ml4", line 1, characters 0-1:
> Error: Preprocessor error

I'm not Ocaml user so I'm stuck here. Any hints?

Thanks,

Edsko

PS. Verbose output: with campl5 version 5.11:

> # make VERBOSE=1 world
> *****************************************************
> *****************************************************
> ****************** Entering stage1 ******************
> *****************************************************
> *****************************************************
> make -f Makefile.stage1 "stage1"
> "ocamlc" -rectypes  -I config -I tools -I tools/coqdoc -I scripts -I  
> lib -I kernel -I kernel/byterun -I library -I proofs -I tactics -I  
> pretyping -I interp -I toplevel -I parsing -I ide/utils -I ide -I  
> contrib/omega -I contrib/romega -I contrib/micromega -I contrib/ring  
> -I contrib/dp -I contrib/setoid_ring -I contrib/xml -I contrib/ 
> extraction -I contrib/interface -I contrib/fourier -I contrib/cc -I  
> contrib/funind -I contrib/firstorder -I contrib/field -I contrib/ 
> subtac -I contrib/rtauto  -I "+camlp5" -g  -pp "camlp5o -I .  config/ 
> coq_config.cmo lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/ 
> flags.cmo lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/hashcons.cmo  
> lib/predicate.cmo lib/rtree.cmo lib/option.cmo kernel/names.cmo  
> kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo kernel/ 
> mod_subst.cmo kernel/sign.cmo kernel/cbytecodes.cmo kernel/ 
> copcodes.cmo kernel/cemitcodes.cmo kernel/declarations.cmo kernel/ 
> retroknowledge.cmo kernel/pre_env.cmo kernel/cbytegen.cmo kernel/ 
> conv_oracle.cmo kernel/environ.cmo kernel/closure.cmo kernel/ 
> reduction.cmo kernel/type_errors.cmo kernel/entries.cmo kernel/ 
> modops.cmo kernel/inductive.cmo kernel/typeops.cmo kernel/ 
> indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo kernel/ 
> subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo library/ 
> nameops.cmo library/libnames.cmo library/summary.cmo library/ 
> nametab.cmo library/libobject.cmo library/lib.cmo library/ 
> goptions.cmo library/decl_kinds.cmo library/global.cmo pretyping/ 
> termops.cmo pretyping/evd.cmo pretyping/reductionops.cmo pretyping/ 
> inductiveops.cmo pretyping/rawterm.cmo pretyping/detyping.cmo  
> pretyping/pattern.cmo interp/topconstr.cmo interp/genarg.cmo interp/ 
> ppextend.cmo proofs/tacexpr.cmo parsing/lexer.cmo parsing/extend.cmo  
> toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_util.cmo parsing/ 
> q_coqast.cmo  parsing/argextend.cmo parsing/tacextend.cmo parsing/ 
> vernacextend.cmo  parsing/g_prim.cmo parsing/g_tactic.cmo parsing/ 
> g_ltac.cmo parsing/g_constr.cmo -impl" -impl test.ml4 -o test-grammar
> Error while loading "config/coq_config.cmo": config/coq_config.cmo  
> is not a bytecode object file.
> File "test.ml4", line 1, characters 0-1:
> Error: Preprocessor error
> make[1]: *** [parsing/grammar.cma] Error 2
> make: *** [stage1] Error 2

and with version 5.12:

> "ocamlc.opt" -rectypes  -I config -I tools -I tools/coqdoc -I  
> scripts -I lib -I kernel -I kernel/byterun -I library -I proofs -I  
> tactics -I pretyping -I interp -I toplevel -I parsing -I ide/utils - 
> I ide -I contrib/omega -I contrib/romega -I contrib/micromega -I  
> contrib/ring -I contrib/dp -I contrib/setoid_ring -I contrib/xml -I  
> contrib/extraction -I contrib/interface -I contrib/fourier -I  
> contrib/cc -I contrib/funind -I contrib/firstorder -I contrib/field - 
> I contrib/subtac -I contrib/rtauto  -I "+camlp5" -g  -pp "camlp5o - 
> I .  config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo lib/ 
> compat.cmo lib/flags.cmo lib/util.cmo lib/bigint.cmo lib/dyn.cmo lib/ 
> hashcons.cmo lib/predicate.cmo lib/rtree.cmo lib/option.cmo kernel/ 
> names.cmo kernel/univ.cmo kernel/esubst.cmo kernel/term.cmo kernel/ 
> mod_subst.cmo kernel/sign.cmo kernel/cbytecodes.cmo kernel/ 
> copcodes.cmo kernel/cemitcodes.cmo kernel/declarations.cmo kernel/ 
> retroknowledge.cmo kernel/pre_env.cmo kernel/cbytegen.cmo kernel/ 
> conv_oracle.cmo kernel/environ.cmo kernel/closure.cmo kernel/ 
> reduction.cmo kernel/type_errors.cmo kernel/entries.cmo kernel/ 
> modops.cmo kernel/inductive.cmo kernel/typeops.cmo kernel/ 
> indtypes.cmo kernel/cooking.cmo kernel/term_typing.cmo kernel/ 
> subtyping.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo library/ 
> nameops.cmo library/libnames.cmo library/summary.cmo library/ 
> nametab.cmo library/libobject.cmo library/lib.cmo library/ 
> goptions.cmo library/decl_kinds.cmo library/global.cmo pretyping/ 
> termops.cmo pretyping/evd.cmo pretyping/reductionops.cmo pretyping/ 
> inductiveops.cmo pretyping/rawterm.cmo pretyping/detyping.cmo  
> pretyping/pattern.cmo interp/topconstr.cmo interp/genarg.cmo interp/ 
> ppextend.cmo proofs/tacexpr.cmo parsing/lexer.cmo parsing/extend.cmo  
> toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_util.cmo parsing/ 
> q_coqast.cmo  parsing/argextend.cmo parsing/tacextend.cmo parsing/ 
> vernacextend.cmo  parsing/g_prim.cmo parsing/g_tactic.cmo parsing/ 
> g_ltac.cmo parsing/g_constr.cmo -impl" -impl test.ml4 -o test-grammar
> Error while loading "parsing/argextend.cmo": interface mismatch on  
> Pcaml.
> File "test.ml4", line 1, characters 0-1:
> Error: Preprocessor error
> make[1]: *** [parsing/grammar.cma] Error 2
> make: *** [stage1] Error 2