coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
That must be it. The real problem is that machine that make failed on is woefully defficient in libraries.
I suspect something went wrong in your ./configure process, so
seeing the output of that might help diagnose the error.
Yes.
Also, is this coq-8.4pl3.tar.gz exactly as downloaded from the website
No.
did you try to apply Vladimir's patches (necessary for his
foundations library)?
--
Best,
Bill
- [Coq-Club] Compilation of CoQ on Linux, michael.ganem, 01/04/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Stéphane Glondu, 01/05/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/05/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Vladimir Voevodsky, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/10/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/10/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/11/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/06/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Jason Gross, 01/06/2014
- Message not available
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Compilation of CoQ on Linux, Michael Ganem, 01/13/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/14/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Ben Horsfall, 01/14/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Vladimir Voevodsky, 01/14/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Michael Ganem, 01/13/2014
- Message not available
- Message not available
- Message not available
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/05/2014
- Re: [Coq-Club] Compilation of CoQ on Linux, Stéphane Glondu, 01/05/2014
Archive powered by MHonArc 2.6.18.