[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent han
|
From: |
John Wiegley |
|
Subject: |
bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop |
|
Date: |
Fri, 04 Mar 2016 13:04:34 -0800 |
|
User-agent: |
Gnus/5.130014 (Ma Gnus v0.14) Emacs/24.5 (darwin) |
>>>>> Clément Pit--Claudel <clement.pitclaudel@live.com> writes:
> Definitely OS X only; I haven't seen it in over 6 months using of Emacs 25
> w/ PG and Coq.
That's good to hear, thanks for that data point. I've posted reproduction
instructions to emacs-devel, but they should be repeated here:
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.
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2