|
From: | Anders Lindgren |
Subject: | Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop |
Date: | Fri, 4 Mar 2016 22:54:44 +0100 |
>>>>> Anders Lindgren <address@hidden> writes:
> However, I would need a recipe, including where to get and how to install the
> external programs, and the steps you take in Emacs to reproduce the problem.
Hi Anders, Clément,
I am using ProofGeneral-4.3pre150313, and Coq 8.4pl6. I've tried setting
coq-prog-name to both "coqtop" and "coqtop.opt", with no change in behavior.
If you download Software Foundations from:
https://www.cis.upenn.edu/~bcpierce/sf/current/index.html
And open the file ImpParser.v, it hangs for me while attempting to evaluate
the definition parsePrimaryExp.
Note that I build and install all of this through Nix, so if you're interested
in those details, let me know.
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2
[Prev in Thread] | Current Thread | [Next in Thread] |