Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Compilation of CoQ on Linux

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Compilation of CoQ on Linux


Chronological Thread 
  • 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 21:31:19 -0600

> Anyway, try passing -no-native-compiler to ./configure.

Thanks, Jason! I couldn't find your flag, but maybe this is what you meant,
and it worked:

make clean
./configure --prefix /home/richter/Coq -natdynlink no
make world
umask 022
make install

> That's a different error message than the one you got before. Did
> the other one magically disappear? Or is this a different computer?

It's the same computer, and I didn't notice the difference in error messages,
other than
make VERBOSE=1
making more noise. Here's the common error message:

"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

Any ideas about why "dynamic loading of native code" would give me this
error? Let me remind you that I had no such error on another machine running
SL, a machine with this configure info:

(poisson)coq-8.4pl3> ./configure --prefix /rhome/2/richter/Coq
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.4pl3
Architecture : Linux
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath
'/rhome/2/richter/Coq/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 :
/rhome/2/richter/HOL-Light/lib/ocaml/camlp5
Native dynamic link support : true
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/Coq/bin
library will be copied in /rhome/2/richter/Coq/lib/coq
config files will be copied in /rhome/2/richter/Coq/etc/xdg/coq
data files will be copied in /rhome/2/richter/Coq/share/coq
man pages will be copied in /rhome/2/richter/Coq/share/man
documentation will be copied in /rhome/2/richter/Coq/share/doc/coq
emacs mode will be copied in /rhome/2/richter/Coq/share/emacs/site-lisp

--
Best,
Bill



Archive powered by MHonArc 2.6.18.

Top of Page