The Coq mailing list

[Andrej Bauer <Andrej.Bauer AT fmf.uni-lj.si>]

I am trying to compile Coq 8.1pl2 with Ocaml 3.10. The Coq web page
indicates that this is possible. I have ocaml 3.10 and camlp5 installed
through Godi. The problem with Coq happens both in Godi and "manual"
compilation.

The ./configure script is happy (see below) but the compilation gets
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
for some reason. Is this a known issue, or is my computer just very
special? Any help is appreciated (and I apologize if this is the wrong
mailing list).

Andrej

P.S. Here is the result of ./configure:
--------------------
$ ./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'.
--------------------