The Coq mailing list

[Bill Richter <richter AT math.northwestern.edu>]

I successfully installed Coq on a Scientific Linux which presumably had all 
the libraries, with 
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

But I failed to make Coq an a similar machine missing libraries, with
 uname -a
Linux localhost.localdomain 2.6.18-194.11.4.el5 #1 SMP Tue Sep 21 06:57:06 
EDT 2010 i686 i686 i386 GNU/Linux

Here's my report: 

./configure --prefix /home/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

Native dynamic link support       : true
  Documentation                     : None
  CoqIde                            : no

 make world

OCAMLC    plugins/syntax/nat_syntax.ml
OCAMLC    plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLC -a -o plugins/syntax/nat_syntax_plugin.cma
OCAMLOPT  plugins/syntax/nat_syntax.ml
OCAMLOPT  plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLOPT -a -o plugins/syntax/nat_syntax_plugin.cmxa
OCAMLOPT -shared -o plugins/syntax/nat_syntax_plugin.cmxs
COQC -nois theories/Init/Datatypes.v
File "/home/richter/Desktop/coq-8.4pl3/theories/Init/Datatypes.v", line 13, 
characters 0-38:
Error: error loading shared library: 
/home/richter/Desktop/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/Desktop/coq-8.4pl3'
make: *** [world] Error 2

-- 
Best,
Bill