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

Previous Next

To add a comment to this bug, you must first unarchive it, by sending
a message to control AT debbugs.gnu.org, with unarchive 22865 in the body.
You can then email your comments to 22865 AT debbugs.gnu.org in the normal way.

Toggle the display of automated, internal messages from the tracker.

Message #5 received at submit <at> debbugs.gnu.org (full text, mbox):

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 #8 received at 22865 <at> debbugs.gnu.org (full text, mbox):

From: John Wiegley <jwiegley <at> gmail.com>
To: 22865 <at> debbugs.gnu.org
Cc: Clément Pit--Claudel <cpitcla <at> csail.mit.edu>
Subject: Re: bug#22865: 25.0.91;
 Use Proof General with emacs-25 on OS X frequent hangs coqtop
Date: Fri, 04 Mar 2016 11:55:41 -0800

Clément, have you seen this bug on your side?  Is it possible that this only
happens on OS X?

-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2

Message #11 received at 22865 <at> debbugs.gnu.org (full text, mbox):

From: Clément Pit--Claudel <clement.pitclaudel <at> live.com>
To: John Wiegley <johnw <at> gnu.org>, 22865 <at> debbugs.gnu.org
Subject: Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X
 frequent hangs coqtop
Date: Fri, 4 Mar 2016 15:25:27 -0500

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

On 03/04/2016 02:55 PM, John Wiegley wrote:
> Clément, have you seen this bug on your side?  Is it possible that this only
> happens on OS X?

Definitely OS X only; I haven't seen it in over 6 months using of Emacs 25 w/ PG and Coq.

[signature.asc (application/pgp-signature, attachment)]

Message #14 received at 22865 <at> debbugs.gnu.org (full text, mbox):

From: John Wiegley <jwiegley <at> gmail.com>
To: Clément Pit--Claudel <clement.pitclaudel <at> live.com>
Cc: 22865 <at> debbugs.gnu.org
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:04:34 -0800

>>>>> Clément Pit--Claudel <clement.pitclaudel <at> 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

Message #19 received at 22865-done <at> debbugs.gnu.org (full text, mbox):

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.

Message #22 received at 22865-done <at> debbugs.gnu.org (full text, mbox):

From: Clément Pit--Claudel <cpitcla <at> csail.mit.edu>
To: Paul Eggert <eggert <at> cs.ucla.edu>,
 YAMAMOTO Mitsuharu <mituharu <at> math.s.chiba-u.ac.jp>
Cc: John Wiegley <jwiegley <at> gmail.com>, 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 12:41:59 -0500

On 03/05/2016 12:22 PM, Paul Eggert wrote:
> 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.

Proof General includes a workaround, but isn't this still a bug?

Message #25 received at 22865-done <at> debbugs.gnu.org (full text, mbox):

From: Paul Eggert <eggert <at> cs.ucla.edu>
To: Clément Pit--Claudel <cpitcla <at> csail.mit.edu>,
 YAMAMOTO Mitsuharu <mituharu <at> math.s.chiba-u.ac.jp>
Cc: John Wiegley <jwiegley <at> gmail.com>, 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 11:49:49 -0800

Clément Pit--Claudel wrote:
> Proof General includes a workaround, but isn't this still a bug?

Hmm, I suppose it is, though it's no longer a blocker for the release. I'll 
reopen the bug report.

Message #32 received at 22865-done <at> debbugs.gnu.org (full text, mbox):

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

>>>>> Paul Eggert <eggert <at> cs.ucla.edu> writes:

> Hmm, I suppose it is, though it's no longer a blocker for the release. I'll
> reopen the bug report.

Thank you, Paul.

-- 
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2

Message #35 received at 22865-done <at> debbugs.gnu.org (full text, mbox):

From: Wolfgang Jenkner <wjenkner <at> inode.at>
To: Clément Pit--Claudel <cpitcla <at> csail.mit.edu>
Cc: John Wiegley <jwiegley <at> gmail.com>, Paul Eggert <eggert <at> cs.ucla.edu>,
 22865-done <at> debbugs.gnu.org, YAMAMOTO Mitsuharu <mituharu <at> math.s.chiba-u.ac.jp>
Subject: Re: bug#22865: 25.0.91;
 Use Proof General with emacs-25 on OS X frequent hangs coqtop
Date: Sun, 06 Mar 2016 14:03:41 +0100

On Sat, Mar 05 2016, Clément Pit--Claudel wrote:

> Proof General includes a workaround, but isn't this still a bug?

The same as bug#6771, I guess.

Previous Next

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