Version française
Home     About     Download     Resources     Contact us    
Browse thread
Coq 8.1 and Ocaml 3.10
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Andrej Bauer <Andrej.Bauer@f...>
Subject: Coq 8.1 and Ocaml 3.10
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'.
--------------------