The Coq mailing list

[Haoxi Zhan <hz12 AT hampshire.edu>]

Hi Bill,
> 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
Unfortunately, Coq is not available for Scientific Linux. So you have to 
compile on your own. However, ocaml-lablgtk is available in Fedora EPEL 6 
repo, which is supposed to be compabile with RHEL6/ CentOS6 and Scientific 
Linux 6.
> LablGtk2 not found: CoqIde will not be available.
CoqIde depends on LablGtk, if you don't have LablGtk, you would compile Coq 
without CoqIde. You can get LablGtk by EPEL 6 if you are using Scientific 
Linux 6.*. Otherwise, you may need to download it and compile it manually.
> hevea was not found; documentation will not be available
The lack of hevea would make it impossible to compile the documentation. 
Hevea 
is available here: http://hevea.inria.fr/
> 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:
I don't know what error is this.
> /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
This error might be caused by SELinux. You can disable SELinux temporarily to 
see what will happen.
> make[1]: Leaving directory `/home/richter/Desktop/coq-8.4pl3'
> make: *** [world] Error 2

It's really a hard job to compile something on your own. If you have a choice 
of distributions, you might want to try some other distributions which come 
with Coq in the repo.

- Haoxi