[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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'.
--------------------