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: Jason Gross <jasongross9 AT gmail.com>
  • To: Bill Richter <richter AT math.northwestern.edu>
  • Cc: Stéphane Glondu <steph AT glondu.net>, "michael.ganem" <michael.ganem AT gmail.com>, coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Compilation of CoQ on Linux
  • Date: Sun, 5 Jan 2014 22:34:28 -0500

If you don't need CoqIDE (and instead use emacs), ocaml-4.01 or ocaml-3.12 and camlp5 (or camlp4) and findlib/ocamlfind should be sufficient.  (Then run "./configure -nodoc -coqide no")  If you also want CoqIDE, you'll need lablgtk2 and it's dependencies (much of Gtk+ 2).  If you also want documentation, you'll need LaTeX and hevea.  On a fresh debian ubuntu machine, I can get all the dependencies (except LaTeX/hevea) with "sudo apt-get install ocaml camlp5 liblablgtk2-ocaml ocaml-findlib".

-Jason


On Sun, Jan 5, 2014 at 9:58 PM, Bill Richter <richter AT math.northwestern.edu> wrote:
Thanks, Jason.  It's supposed to get down to -45 degrees windchill here in Chicago, so it will take me a while to get most of your data.

   I suspect something went wrong in your ./configure process, so
   seeing the output of that might help diagnose the error.

That must be it.  The real problem is that machine that make failed on is woefully defficient in libraries.

   Also, is this coq-8.4pl3.tar.gz exactly as downloaded from the website

Yes.

   did you try to apply Vladimir's patches (necessary for his
   foundations library)?

No.

--
Best,
Bill




Archive powered by MHonArc 2.6.18.

Top of Page