coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vladimir Voevodsky <vladimir AT ias.edu>
- To: Bill Richter <richter AT math.northwestern.edu>
- Cc: Jason Gross <jasongross9 AT gmail.com>, steph AT glondu.net, michael.ganem AT gmail.com, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Compilation of CoQ on Linux
- Date: Mon, 6 Jan 2014 10:55:39 -0500
Bill, please read the first page of the cover paper for the library before
trying things. The library won't compile with Coq8.4pl3. You need to get
Coq8.3pl2 (how to get it is explained in the main README file of the
library), patch it (how to do it is explained in the README file for the
subdirectory Coq_patches of the library) and then compile and install it.
After that the library itself should compile with the "make" command from the
directory Foundations/
V.
On 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
- [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
- Re: [Coq-Club] Compilation of CoQ on Linux, Bill Richter, 01/20/2014
Archive powered by MHonArc 2.6.18.