Coq 8.1 and Ocaml 3.10

Coq 8.1 and Ocaml 3.10

[Andrej Bauer]

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'.
--------------------

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

[Daniel de Rauglaudre]

Hi,

On Wed, Dec 12, 2007 at 06:21:24PM +0100, Andrej Bauer wrote:

> OCAMLOPT4 tactics/hipattern.ml4
> Error while loading "parsing/q_constr.cmo": file not found in path.
> Preprocessor error

The file q_constr.cmo is not part of Camlp5, but of Coq. Write to
the Coq team, rather.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

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

[Arnaud Spiwack]

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
>
>   

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

[Andrej Bauer]

Arnaud Spiwack wrote:
> 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.

I don't insist, I just want a Coq which doesn't think that semirings
satisfy the cancelation law for addition (since I care about
distributive lattices, which are semirings without a cancelation law).

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

Will try an older version of Coq first. Thanks for the advice. I just
wanted to hear from someone that Coq was "Ocaml 3.10 ready".

Andrej