coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bill Richter <richter AT math.northwestern.edu>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: steph AT glondu.net, michael.ganem AT gmail.com, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Compilation of CoQ on Linux
- Date: Fri, 10 Jan 2014 07:18:42 -0600
Thanks, Jason. I'll try passing -no-native-compiler to ./configure. Your
last configure idea didn't work for me:
(localhost)coq-8.4pl3> make clean
(localhost)coq-8.4pl3> ./configure --prefix /home/richter/Coq -with-doc no
-coq
ide no
You have GNU Make 3.81. Good!
You have Objective-Caml 3.12.1. Good!
You have native-code compilation. Good!
CoqIde disabled as requested.
Coq top directory : /home/richter/coq-8.4pl3
Architecture : Linux
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath
'/home/richter/Co
q/lib/coq'
Coq tools bytecode link flags :
OS dependent libraries : -cclib -lunix
Objective-Caml/Camlp4 version : 3.12.1
Objective-Caml/Camlp4 binaries in : /home/richter/HOL-Light/bin
Objective-Caml library in : /home/richter/HOL-Light/lib/ocaml
Camlp4 library in : /home/richter/HOL-Light/lib/ocaml/camlp5
Native dynamic link support : true
Documentation : None
CoqIde : no
Web browser : firefox -remote "OpenURL(%s,new-tab)"
|| f
irefox %s &
Coq web site : http://coq.inria.fr/
Paths for true installation:
binaries will be copied in /home/richter/Coq/bin
library will be copied in /home/richter/Coq/lib/coq
config files will be copied in /home/richter/Coq/etc/xdg/coq
data files will be copied in /home/richter/Coq/share/coq
man pages will be copied in /home/richter/Coq/share/man
documentation will be copied in /home/richter/Coq/share/doc/coq
emacs mode will be copied in /home/richter/Coq/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'.
(localhost)coq-8.4pl3> make VERBOSE=1
[...]
"ocamlopt" -rectypes -I config -I lib -I kernel -I kernel/byterun -I
library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I
tools -I tools/coqdoc -I scripts -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -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
plugins/decl_mode -I "/home/richter/HOL-Light/lib/ocaml/camlp5"
-intf-suffix .cmi -c plugins/syntax/nat_syntax.ml
"ocamlopt" -rectypes -I config -I lib -I kernel -I kernel/byterun -I
library -I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I
tools -I tools/coqdoc -I scripts -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -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
plugins/decl_mode -I "/home/richter/HOL-Light/lib/ocaml/camlp5"
-intf-suffix .cmi -c plugins/syntax/nat_syntax_plugin_mod.ml
"ocamlopt" -rectypes -I config -I lib -I kernel -I kernel/byterun -I library
-I proofs -I tactics -I pretyping -I interp -I toplevel -I parsing -I tools
-I tools/coqdoc -I scripts -I ide/utils -I ide -I plugins/omega -I
plugins/romega -I plugins/micromega -I plugins/quote -I plugins/ring -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
plugins/decl_mode -I "/home/richter/HOL-Light/lib/ocaml/camlp5" -a -o
plugins/syntax/nat_syntax_plugin.cmxa plugins/syntax/nat_syntax.cmx
plugins/syntax/nat_syntax_plugin_mod.cmx
"ocamlopt" -rectypes -linkall -shared -o
plugins/syntax/nat_syntax_plugin.cmxs plugins/syntax/nat_syntax_plugin.cmxa
rm -f theories/Init/Datatypes.glob
bin/coqtop.opt -boot -compile theories/Init/Datatypes -nois
File "/home/richter/coq-8.4pl3/theories/Init/Datatypes.v", line 13,
characters 0-38:
Error: error loading shared library:
/home/richter/coq-8.4pl3/plugins/syntax/nat_syntax_plugin.cmxs: cannot
restore segment prot after reloc: Permission denied
make[1]: *** [theories/Init/Datatypes.vo] Error 1
make[1]: Leaving directory `/home/richter/coq-8.4pl3'
make: *** [world] Error 2
(localhost)coq-8.4pl3>
- [Coq-Club] Compilation of CoQ on Linux, michael.ganem, 01/04/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Stéphane Glondu, 01/05/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/05/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
- 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
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 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
- Re: [Coq-Club] Compilation of CoQ on Linux, Michael Ganem, 01/13/2014
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/05/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Stéphane Glondu, 01/05/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/20/2014
Archive powered by MHonArc 2.6.18.