The Coq mailing list

[Bill Richter <richter AT math.northwestern.edu>]

I got Coq 8.3 to run on two SL machines (the 32-bit machine needed the 
configure flag -natdynlink no) using Dan Grayson's patches, and that includes 
Vladimir's Foundation patches.  In case someone else could benefit from this, 
or I didn't do it right, I want to explain what worked.  

I went to https://github.com/DanGrayson/coq in the Firefox browser and
clicked on the righthand black box Download ZIP.  You can easily get to Dan's 
link by going to 
https://github.com/DanGrayson
clicking on the box Repositories at the top, and then 
clicking on the blue link coq.
I unzipped the downloaded file with
unzip coq-8.3-recommended-patches.zip
This creates a perfectly good Coq directory 
coq-8.3-recommended-patches
in which I can run configure, make world and make install.  Using this coq, I 
succeeded in make in Vladimir's directory
Foundations-master.

So that's great, and now I need to learn about Coq, UF, Proof General etc. I 
won't post any dumb questions until I've tried to read the documentation. 

BTW I'm not happy that UF only runs on Coq 8.3.  If I was one of the Coq 
developers of Vladimir's UF programmers, I'd be working real hard to get the 
bugs reported and fixed so that UF runs smoothly in Coq 8.4.

-- 
Best,
Bill