coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bill Richter <richter AT math.northwestern.edu>
- To: Michael Ganem <michael.ganem AT gmail.com>
- Cc: steph AT glondu.net, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Compilation of CoQ on Linux
- Date: Mon, 13 Jan 2014 20:56:59 -0600
I have bad news: I can not compile coq-8.3pl2, the version needed for
Vladimir's Foundations, on either of my two SL machines. Here's a bug report
for the better of the two. BTW here's a dumb question. This is a 64-bit
machine. Doesn't the _64 in the uname output show this is a 64-bit machine?
I also failed to make with dynamic loading of native code turned off. On my
more primitive 32-bit home machine, I failed to make with Vladimir's
Foundations patches installed.
(poisson)coq-8.3pl2> pwd
/rhome/2/richter/coq-8.3pl2
(poisson)coq-8.3pl2> uname -a
Linux poisson.math.northwestern.edu 2.6.32-358.18.1.el6.x86_64 #1 SMP Tue Aug
27 14:23:09 CDT 2013 x86_64 x86_64 x86_64 GNU/Linux
(poisson)coq-8.3pl2> ocaml -version
The Objective Caml toplevel, version 3.12.1
(poisson)coq-8.3pl2> ./configure --prefix /rhome/2/richter/Coq83
(poisson)coq-8.3pl2> make VERBOSE=1
[...]
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I
kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I
interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I
plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I
plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I
plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I
plugins/syntax -I "+camlp5" -c pretyping/cbv.ml
"ocamlc" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I
kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I
interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I
plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I
plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I
plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I
plugins/syntax -I "+camlp5" -c pretyping/pretype_errors.mli
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I
kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I
interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I
plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I
plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I
plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I
plugins/syntax -I "+camlp5" -c pretyping/pretype_errors.ml
File "pretyping/pretype_errors.ml", line 48, characters 4-109:
Error: Unbound constructor Stdpp.Exc_located
make[1]: *** [pretyping/pretype_errors.cmx] Error 2
make[1]: Leaving directory `/tmp_mnt/rhome/2/richter/coq-8.3pl2'
make: *** [world] Error 2
(poisson)coq-8.3pl2> make clean
(poisson)coq-8.3pl2> ./configure --prefix /rhome/2/richter/Coq83 -natdynlink
no
You have GNU Make >= 3.81. Good!
You have Objective-Caml 3.12.1. Good!
You have native-code compilation. Good!
LablGtk2 not found: CoqIde will not be available.
hevea was not found; documentation will not be available
Coq top directory : /rhome/2/richter/coq-8.3pl2
Architecture : x86_64
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath
'/rhome/2/richter/Coq83/lib/coq'
Coq tools bytecode link flags :
OS dependent libraries : -cclib -lunix
Objective-Caml/Camlp4 version : 3.12.1
Objective-Caml/Camlp4 binaries in : /rhome/2/richter/HOL-Light/bin
Objective-Caml library in : /rhome/2/richter/HOL-Light/lib/ocaml
Camlp4 library in : +camlp5
Native dynamic link support : false
Documentation : None
CoqIde : no
Web browser : firefox -remote "OpenURL(%s,new-tab)"
|| firefox %s &
Coq web site : http://coq.inria.fr/
Paths for true installation:
binaries will be copied in /rhome/2/richter/Coq83/bin
library will be copied in /rhome/2/richter/Coq83/lib/coq
man pages will be copied in /rhome/2/richter/Coq83/man
documentation will be copied in /rhome/2/richter/Coq83/share/doc/coq
emacs mode will be copied in
/rhome/2/richter/Coq83/share/emacs/site-lisp
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'.
(poisson)coq-8.3pl2> make VERBOSE=1
[...]
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I
kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I
interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I
plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I
plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I
plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I
plugins/syntax -I "+camlp5" -c pretyping/cbv.ml
"ocamlc" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I
kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I
interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I
plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I
plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I
plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I
plugins/syntax -I "+camlp5" -c pretyping/pretype_errors.mli
"ocamlopt" -rectypes -I config -I tools -I tools/coqdoc -I scripts -I lib -I
kernel -I kernel/byterun -I library -I proofs -I tactics -I pretyping -I
interp -I toplevel -I parsing -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -I
plugins/dp -I plugins/setoid_ring -I plugins/xml -I plugins/extraction -I
plugins/fourier -I plugins/cc -I plugins/funind -I plugins/firstorder -I
plugins/field -I plugins/subtac -I plugins/rtauto -I plugins/nsatz -I
plugins/syntax -I "+camlp5" -c pretyping/pretype_errors.ml
File "pretyping/pretype_errors.ml", line 48, characters 4-109:
Error: Unbound constructor Stdpp.Exc_located
make[1]: *** [pretyping/pretype_errors.cmx] Error 2
make[1]: Leaving directory `/tmp_mnt/rhome/2/richter/coq-8.3pl2'
make: *** [world] Error 2
--
Best,
Bill
- Re: [Coq-Club] Compilation of CoQ on Linux, (continued)
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Vladimir Voevodsky, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/10/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/10/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/11/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/06/2014
- Message not available
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Compilation of CoQ on Linux, Michael Ganem, 01/13/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/14/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Ben Horsfall, 01/14/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Vladimir Voevodsky, 01/14/2014
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
Archive powered by MHonArc 2.6.18.