coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bill Richter <richter AT math.northwestern.edu>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: 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: Fri, 10 Jan 2014 07:28:50 -0600
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/
Thanks, Vladimir. I've been a poor correspondent due to the crazy weather in
Chicago (-45 F on Monday), but it's getting warmer. Your advice is great for
compiling on the NWU math dept machines, where the standard Coq installation
worked. But for the machine I normally work on, I haven't been able to
compile any version of Coq.
--
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.