[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent
|
From: |
John Wiegley |
|
Subject: |
Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop |
|
Date: |
Fri, 04 Mar 2016 13:03:49 -0800 |
|
User-agent: |
Gnus/5.130014 (Ma Gnus v0.14) Emacs/24.5 (darwin) |
>>>>> 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