The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You can download the Gtk+ stack from http://www.gtk.org/download/index.php (make sure you get 2.*, not 3.*), and lablgtk from http://lablgtk.forge.ocamlcore.org/.  I've not had much trouble building lablgtk, but building gtk+ is a pain, especially if you don't have all the dependencies already lying around.  If you have a package manager for your system, I suggest you use it to get gtk+ (if you don't already have it; you can check with `pkg-config --list-all | sort`; if you don't have gtk, or gtk+-2.0 doesn't show up on the list, then you don't have it).

That's a different error message than the one you got before.  Did the other one magically disappear?  Or is this a different computer?  Anyway, try passing -no-native-compiler to ./configure.  (I can't recall whether that's an option just for trunk, or also for 8.4, and I don't know if it fixes things only for trunk, or also for 8.4.)  Alternatively/additionally, try googling for "cannot restore segment prot after reloc: Permission denied" and see if you can find anything to fix it.

-Jason

On Sun, Jan 5, 2014 at 11:54 PM, Bill Richter <richter AT math.northwestern.edu> wrote:

Jason, I'll try
./configure -nodoc -coqide no
I wish I knew how to install lablgtk2 etc.  I don't know if I have findlib/ocamlfind, but I know that I made Coq on a machine with much the same ocaml stuff (i.e. I installed it myself on both machines) as the machine that failed.  Here's my data for the make failure:


(localhost)coq-8.4pl3> pwd
/home/richter/coq-8.4pl3

(localhost)coq-8.4pl3> 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

(localhost)coq-8.4pl3> ocaml -version
The Objective Caml toplevel, version 3.12.1

(localhost)coq-8.4pl3>  ./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

  Coq top directory                 : /home/richter/coq-8.4pl3
  Architecture                      : Linux
  Coq VM bytecode link flags        : -dllib -lcoqrun -dllpath '/home/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 : /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)" || firefox %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'.

*Warning* To compile the system for a new architecture
          don't forget to do a 'make archclean' before './configure'.

(localhost)coq-8.4pl3> make clean

(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_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>

--
Best,
Bill