Re: [Caml-list] Coq 8.1 and Ocaml 3.10

From: Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr>
To: Andrej.Bauer@andrej.com
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Coq 8.1 and Ocaml 3.10
Date: Wed, 12 Dec 2007 18:32:53 +0100	[thread overview]
Message-ID: <47601B45.5090503@lix.polytechnique.fr> (raw)
In-Reply-To: <47601894.1080105@fmf.uni-lj.si>

Hi,

This bug seems to have nothing to do with camlp4/5. I've seen this bug 
twice before, with two different version of OCaml (3.09.3 and 3.09.2 
namely), but always Coq 8.1pl2. It's rare, and I have no clue why they 
occur.

One solution is to move to the trunk version of Coq (whose Makefile has 
been reengineered, and is far less surprising).

If you insist on keeping 8.1pl2, then here is a way to work around it :
First do a :
  make world
when it stops, do :
  make parsing/q_constr.cmo
to build the missing file, then do :
  make worldnodep

Which should build everything but not clean the installation (as make 
world do before building the dependencies).

Arnaud Spiwack

Andrej Bauer a écrit :
> The Coq homepage seems to indicate that Coq 8.1pl2 can be compiled with
> Ocaml 3.10 and camlp5. I have those (installed through Godi), the
> configuration script for Coq is happy, see below, yet the compilation is
> getting stuck on
>
> OCAMLOPT4 tactics/hipattern.ml4
> Error while loading "parsing/q_constr.cmo": file not found in path.
> Preprocessor error
> make[1]: *** [tactics/hipattern.cmx] Error 2
> make[1]: Leaving directory `/home/andrej/compile/coq-8.1pl2'
>
> There is a parsing/q_constr.ml4 file which does not seem to be compiled.
>
> This happens with Godi version of Coq as well as one that I compiled "by
> hand".
>
> I am blaming myself and Ocaml 3.10 which is why I am posting on this
> list, as opposed to coq-club. Any help is appreciated.
>
> Andrej
>
> P.S.
> This is the result of ./configure prefix /usr/local:
>
> --------------------
> $ ./configure --prefix /usr/local
> You have Objective-Caml 3.10.0. Good!
> You have native-code compilation. Good!
> LablGtk2 found, native threads: native CoqIde will be available.
> Should I compile the complete theory of real analysis [Y/N, default is Y] ?
> y
>
>   Coq top directory                 : /home/andrej/compile/coq-8.1pl2
>   Architecture                      : i686
>   OS dependent libraries            : -cclib -lunix
>   Objective-Caml/Camlp4 version     : 3.10.0
>   Objective-Caml/Camlp4 binaries in : /usr/local/godi/bin
>   Objective-Caml library in         : /usr/local/godi/lib/ocaml/std-lib
>   Camlp4 library in                 : +camlp5
>   Lablgtk2 library in               : +lablgtk2
>   FSets theory                      : All
>   Reals theory                      : All
>   CoqIde                            : opt
>
>   Paths for true installation:
>     binaries   will be copied in /usr/local/bin
>     library    will be copied in /usr/local/lib/coq
>     man pages  will be copied in /usr/local/man
>     emacs mode will be copied in /usr/local/share/emacs/site-lisp
>
> /home/andrej/compile/coq-8.1pl2/theories
> /home/andrej/compile/coq-8.1pl2/contrib
> If anything in the above is wrong, please restart './configure'
>
> *Warning* To compile the system for a new architecture
>           don't forget to do a 'make archclean' before './configure'.
> --------------------
>
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>   