* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
@ 2016-03-01 2:02 John Wiegley
2016-03-04 19:55 ` John Wiegley
0 siblings, 1 reply; 16+ messages in thread
From: John Wiegley @ 2016-03-01 2:02 UTC (permalink / raw)
To: 22865
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
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-01 2:02 bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop John Wiegley
@ 2016-03-04 19:55 ` John Wiegley
2016-03-04 19:59 ` John Wiegley
2016-03-04 20:25 ` Clément Pit--Claudel
0 siblings, 2 replies; 16+ messages in thread
From: John Wiegley @ 2016-03-04 19:55 UTC (permalink / raw)
To: 22865; +Cc: Clément Pit--Claudel
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
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 19:55 ` John Wiegley
@ 2016-03-04 19:59 ` John Wiegley
2016-03-04 20:23 ` Anders Lindgren
` (2 more replies)
2016-03-04 20:25 ` Clément Pit--Claudel
1 sibling, 3 replies; 16+ messages in thread
From: John Wiegley @ 2016-03-04 19:59 UTC (permalink / raw)
To: Emacs developers; +Cc: Clément Pit--Claudel
[-- Attachment #1: Type: text/plain, Size: 773 bytes --]
I just wanted to put out a general call to other developers for some eyes on
this bug, since it occurs in the 25.1 release candidate, and I will not be
able to upgrade to Emacs 25 until it is fixed (it prevents me from getting
actual work done).
I'm not sure how many other Coq/Proof General users we have here, and who also
use OS X, but maybe someone would be willing to pair debug with me? From the
outside, it looks like a process communication issue, because the same
versions of PG and Coq work just fine with Emacs 24.5 (the Mac port variant).
But at this point I fear it could be anything.
Thanks,
--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2
[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 629 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 19:59 ` John Wiegley
@ 2016-03-04 20:23 ` Anders Lindgren
2016-03-04 21:03 ` John Wiegley
2016-03-04 20:24 ` Clément Pit--Claudel
2016-03-05 0:33 ` YAMAMOTO Mitsuharu
2 siblings, 1 reply; 16+ messages in thread
From: Anders Lindgren @ 2016-03-04 20:23 UTC (permalink / raw)
To: John Wiegley, Emacs developers, Clément Pit--Claudel
[-- Attachment #1: Type: text/plain, Size: 1166 bytes --]
HI!
I'm not a Coq/Proof General user but I'm interested in taking a look at
this (even if I can't promise a fast response).
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.
-- Anders
On Fri, Mar 4, 2016 at 8:59 PM, John Wiegley <jwiegley@gmail.com> wrote:
> I just wanted to put out a general call to other developers for some eyes
> on
> this bug, since it occurs in the 25.1 release candidate, and I will not be
> able to upgrade to Emacs 25 until it is fixed (it prevents me from getting
> actual work done).
>
> I'm not sure how many other Coq/Proof General users we have here, and who
> also
> use OS X, but maybe someone would be willing to pair debug with me? From
> the
> outside, it looks like a process communication issue, because the same
> versions of PG and Coq work just fine with Emacs 24.5 (the Mac port
> variant).
> But at this point I fear it could be anything.
>
> Thanks,
> --
> John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2
>
[-- Attachment #2: Type: text/html, Size: 1739 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 19:59 ` John Wiegley
2016-03-04 20:23 ` Anders Lindgren
@ 2016-03-04 20:24 ` Clément Pit--Claudel
2016-03-05 0:33 ` YAMAMOTO Mitsuharu
2 siblings, 0 replies; 16+ messages in thread
From: Clément Pit--Claudel @ 2016-03-04 20:24 UTC (permalink / raw)
To: emacs-devel
[-- Attachment #1.1: Type: text/plain, Size: 815 bytes --]
On 03/04/2016 02:59 PM, John Wiegley wrote:
> I just wanted to put out a general call to other developers for some eyes on
> this bug, since it occurs in the 25.1 release candidate, and I will not be
> able to upgrade to Emacs 25 until it is fixed (it prevents me from getting
> actual work done).
>
> I'm not sure how many other Coq/Proof General users we have here, and who also
> use OS X, but maybe someone would be willing to pair debug with me? From the
> outside, it looks like a process communication issue, because the same
> versions of PG and Coq work just fine with Emacs 24.5 (the Mac port variant).
> But at this point I fear it could be anything.
Happy to help. Can you clarify which combination of Emacs/PG/Coq you're using? I can probably borrow a Mac laptop to do some debugging.
[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 19:55 ` John Wiegley
2016-03-04 19:59 ` John Wiegley
@ 2016-03-04 20:25 ` Clément Pit--Claudel
2016-03-04 21:04 ` John Wiegley
1 sibling, 1 reply; 16+ messages in thread
From: Clément Pit--Claudel @ 2016-03-04 20:25 UTC (permalink / raw)
To: John Wiegley, 22865
[-- Attachment #1.1: Type: text/plain, Size: 241 bytes --]
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.
[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 836 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 20:23 ` Anders Lindgren
@ 2016-03-04 21:03 ` John Wiegley
2016-03-04 21:54 ` Anders Lindgren
0 siblings, 1 reply; 16+ messages in thread
From: John Wiegley @ 2016-03-04 21:03 UTC (permalink / raw)
To: Anders Lindgren; +Cc: Clément Pit--Claudel, Emacs developers
>>>>> Anders Lindgren <andlind@gmail.com> 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
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 20:25 ` Clément Pit--Claudel
@ 2016-03-04 21:04 ` John Wiegley
0 siblings, 0 replies; 16+ messages in thread
From: John Wiegley @ 2016-03-04 21:04 UTC (permalink / raw)
To: Clément Pit--Claudel; +Cc: 22865
>>>>> 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
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 21:03 ` John Wiegley
@ 2016-03-04 21:54 ` Anders Lindgren
0 siblings, 0 replies; 16+ messages in thread
From: Anders Lindgren @ 2016-03-04 21:54 UTC (permalink / raw)
To: John Wiegley, Anders Lindgren, Emacs developers,
Clément Pit--Claudel
[-- Attachment #1: Type: text/plain, Size: 1371 bytes --]
Hi!
I think you will need to "dumb it down" for me (as I have no experience
with Coq). Are there any external Emacs packages used? (When I open the
file in a stock Emacs, verilog-mode is used, which doesn't sound right.)
How do I evaluate a definition etc.
If possible, I would prefer a step by step description from "emacs -Q".
-- Anders
On Fri, Mar 4, 2016 at 10:03 PM, John Wiegley <jwiegley@gmail.com> wrote:
> >>>>> Anders Lindgren <andlind@gmail.com> 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
>
[-- Attachment #2: Type: text/html, Size: 2155 bytes --]
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 19:59 ` John Wiegley
2016-03-04 20:23 ` Anders Lindgren
2016-03-04 20:24 ` Clément Pit--Claudel
@ 2016-03-05 0:33 ` YAMAMOTO Mitsuharu
2016-03-05 17:12 ` Wolfgang Jenkner
2016-03-05 17:22 ` Paul Eggert
2 siblings, 2 replies; 16+ messages in thread
From: YAMAMOTO Mitsuharu @ 2016-03-05 0:33 UTC (permalink / raw)
To: Emacs developers, Clément Pit--Claudel
>>>>> On Fri, 04 Mar 2016 11:59:27 -0800, John Wiegley <jwiegley@gmail.com> said:
> I just wanted to put out a general call to other developers for some
> eyes on this bug, since it occurs in the 25.1 release candidate, and
> I will not be able to upgrade to Emacs 25 until it is fixed (it
> prevents me from getting actual work done).
> I'm not sure how many other Coq/Proof General users we have here,
> and who also use OS X, but maybe someone would be willing to pair
> debug with me? From the outside, it looks like a process
> communication issue, because the same versions of PG and Coq work
> just fine with Emacs 24.5 (the Mac port variant). But at this point
> I fear it could be anything.
I could reproduce the problem with 25.0.92, both on X11 and the Mac
port (the `work' branch in
https://bitbucket.org/mituharu/emacs-mac.git). But the behavior of
these variants were slightly different from that of the NS port: the
former allowed me to move the cursor while waiting for the process
output, but the latter needed C-g to move the cursor.
Anyway, the difference between 24 and 25 comes from the following
part in generic/proof-config.el in ProofGeneral-4.3pre150313:
(defcustom proof-shell-process-connection-type (if (= emacs-major-version 24) nil t)
"The value of `process-connection-type' for the proof shell.
Set non-nil for ptys, nil for pipes."
:type 'boolean
:group 'proof-shell)
This part has been changed to the following one in
https://github.com/ProofGeneral/PG/blob/master/generic/proof-config.el,
(defcustom proof-shell-process-connection-type (if (>= emacs-major-version 24) nil t)
"The value of `process-connection-type' for the proof shell.
Set non-nil for ptys, nil for pipes.
NOTE: In emacs >= 24 (checked for 24 and 25.0.50.1), t is not a
good choice: input is cut after 4095 chars, which hangs pg."
:type 'boolean
:group 'proof-shell)
and it seems to work for 25.0.92.
YAMAMOTO Mitsuharu
mituharu@math.s.chiba-u.ac.jp
^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-05 0:33 ` YAMAMOTO Mitsuharu
@ 2016-03-05 17:12 ` Wolfgang Jenkner
2016-03-05 17:22 ` Paul Eggert
1 sibling, 0 replies; 16+ messages in thread
From: Wolfgang Jenkner @ 2016-03-05 17:12 UTC (permalink / raw)
To: YAMAMOTO Mitsuharu; +Cc: Clément Pit--Claudel, Emacs developers
On Sat, Mar 05 2016, YAMAMOTO Mitsuharu wrote:
> Anyway, the difference between 24 and 25 comes from the following
> part in generic/proof-config.el in ProofGeneral-4.3pre150313:
>
> (defcustom proof-shell-process-connection-type (if (= emacs-major-version 24) nil t)
> "The value of `process-connection-type' for the proof shell.
> Set non-nil for ptys, nil for pipes."
I guess the discussion in bug#6771 explains the issue.
Wolfgang
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-05 0:33 ` YAMAMOTO Mitsuharu
2016-03-05 17:12 ` Wolfgang Jenkner
@ 2016-03-05 17:22 ` Paul Eggert
2016-03-05 17:41 ` Clément Pit--Claudel
1 sibling, 1 reply; 16+ messages in thread
From: Paul Eggert @ 2016-03-05 17:22 UTC (permalink / raw)
To: YAMAMOTO Mitsuharu; +Cc: John Wiegley, Clément Pit--Claudel, 22865-done
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.
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-05 17:22 ` Paul Eggert
@ 2016-03-05 17:41 ` Clément Pit--Claudel
2016-03-05 19:49 ` Paul Eggert
2016-03-06 13:03 ` Wolfgang Jenkner
0 siblings, 2 replies; 16+ messages in thread
From: Clément Pit--Claudel @ 2016-03-05 17:41 UTC (permalink / raw)
To: Paul Eggert, YAMAMOTO Mitsuharu; +Cc: John Wiegley, 22865-done
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?
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-05 17:41 ` Clément Pit--Claudel
@ 2016-03-05 19:49 ` Paul Eggert
2016-03-06 4:53 ` John Wiegley
2016-03-06 13:03 ` Wolfgang Jenkner
1 sibling, 1 reply; 16+ messages in thread
From: Paul Eggert @ 2016-03-05 19:49 UTC (permalink / raw)
To: Clément Pit--Claudel, YAMAMOTO Mitsuharu; +Cc: John Wiegley, 22865-done
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.
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-05 19:49 ` Paul Eggert
@ 2016-03-06 4:53 ` John Wiegley
0 siblings, 0 replies; 16+ messages in thread
From: John Wiegley @ 2016-03-06 4:53 UTC (permalink / raw)
To: Paul Eggert; +Cc: Clément Pit--Claudel, 22865-done
>>>>> Paul Eggert <eggert@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
^ permalink raw reply [flat|nested] 16+ messages in thread
* bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-05 17:41 ` Clément Pit--Claudel
2016-03-05 19:49 ` Paul Eggert
@ 2016-03-06 13:03 ` Wolfgang Jenkner
1 sibling, 0 replies; 16+ messages in thread
From: Wolfgang Jenkner @ 2016-03-06 13:03 UTC (permalink / raw)
To: Clément Pit--Claudel; +Cc: John Wiegley, Paul Eggert, 22865-done
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.
^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2016-03-06 13:03 UTC | newest]
Thread overview: 16+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2016-03-01 2:02 bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop John Wiegley
2016-03-04 19:55 ` John Wiegley
2016-03-04 19:59 ` John Wiegley
2016-03-04 20:23 ` Anders Lindgren
2016-03-04 21:03 ` John Wiegley
2016-03-04 21:54 ` Anders Lindgren
2016-03-04 20:24 ` Clément Pit--Claudel
2016-03-05 0:33 ` YAMAMOTO Mitsuharu
2016-03-05 17:12 ` Wolfgang Jenkner
2016-03-05 17:22 ` Paul Eggert
2016-03-05 17:41 ` Clément Pit--Claudel
2016-03-05 19:49 ` Paul Eggert
2016-03-06 4:53 ` John Wiegley
2016-03-06 13:03 ` Wolfgang Jenkner
2016-03-04 20:25 ` Clément Pit--Claudel
2016-03-04 21:04 ` John Wiegley
Code repositories for project(s) associated with this external index
https://git.savannah.gnu.org/cgit/emacs.git
https://git.savannah.gnu.org/cgit/emacs/org-mode.git
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.