From: Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>
To: caml-list@yquem.inria.fr
Subject: Coq 8.1 and Ocaml 3.10
Date: Wed, 12 Dec 2007 18:21:24 +0100 [thread overview]
Message-ID: <47601894.1080105@fmf.uni-lj.si> (raw)
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'.
--------------------
next reply other threads:[~2007-12-12 17:20 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2007-12-12 17:21 Andrej Bauer [this message]
2007-12-12 17:28 ` [Caml-list] " Daniel de Rauglaudre
2007-12-12 17:32 ` Arnaud Spiwack
2007-12-12 21:57 ` Andrej Bauer
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=47601894.1080105@fmf.uni-lj.si \
--to=andrej.bauer@fmf.uni-lj.si \
--cc=Andrej.Bauer@andrej.com \
--cc=caml-list@yquem.inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox