GNU bug report logs - #22865
25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

Previous Next

Full log

View this message in rfc822 format

From: help-debbugs <at> gnu.org (GNU bug Tracking System)
To: Paul Eggert <eggert <at> cs.ucla.edu>
Cc: tracker <at> debbugs.gnu.org
Subject: bug#22865: closed (25.0.91; Use Proof General with emacs-25 on OS
 X frequent hangs coqtop)
Date: Sat, 05 Mar 2016 17:23:02 +0000

[Message part 1 (text/plain, inline)]

Your message dated Sat, 5 Mar 2016 09:22:28 -0800
with message-id <56DB15D4.8050509 <at> cs.ucla.edu>
and subject line Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
has caused the debbugs.gnu.org bug report #22865,
regarding 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
to be marked as done.

(If you believe you have received this mail in error, please contact
help-debbugs <at> gnu.org.)


-- 
22865: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=22865
GNU Bug Tracking System
Contact help-debbugs <at> gnu.org with problems

[Message part 2 (message/rfc822, inline)]

From: John Wiegley <jwiegley <at> gmail.com>
To: bug-gnu-emacs <at> gnu.org
Subject: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
Date: Mon, 29 Feb 2016 18:02:35 -0800

I'm afraid this could be difficult to debug, but here is my scenario:

 1. Open a .v (Coq) file within my project.

 2. Ask Proof General to evaluate the file to the end.

 3. Before a certain definition, PG will hang waiting on a response from
    "coqtop", the evaluator. Checking the process list shows that this
    process is not doing anything.

 4. Once this happens, C-g or C-c C-c to abort the evaluation leaves me
    in a broken state where nothing can evaluate anymore. The only
    recourse is to "killall coqtop", and then attempt the evaluation
    again. However, the same definition always causes it to hang. There
    is no common factor about the definitions that I can see, but it
    happens reliably every time for each file where it does occur.

if I switch to 24.5, everything evaluates fine. It happens quite
frequently with emacs-25, but never with 24.5.

Now, this could be 25.1, or it could be Mac port vs. NeXTstep, or it
could be some other subtle interaction with my environment.

Unfortunately this will take time to narrow down, and I have to get the
Coq code written, so for now this is a placeholder and I must revert to
using 24.5. I hope to come back to this later, especially if others have
ideas on where to look.

John

[Message part 3 (message/rfc822, inline)]

From: Paul Eggert <eggert <at> cs.ucla.edu>
To: YAMAMOTO Mitsuharu <mituharu <at> math.s.chiba-u.ac.jp>
Cc: John Wiegley <jwiegley <at> gmail.com>,
 Clément Pit--Claudel <cpitcla <at> csail.mit.edu>,
 22865-done <at> debbugs.gnu.org
Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X
 frequent hangs coqtop
Date: Sat, 5 Mar 2016 09:22:28 -0800

In <http://lists.gnu.org/archive/html/emacs-devel/2016-03/msg00087.html> 
YAMAMOTO Mitsuharu wrote:

> This part has been changed to the following one in
> https://github.com/ProofGeneral/PG/blob/master/generic/proof-config.el,
> ...
> and it seems to work for 25.0.92.

Thanks for checking this. As it appears that the bug has been fixed on the Proof 
General side, I'm closing the bug report.

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.