* Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop
2016-03-04 19:59 ` bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop 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; 7+ 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] 7+ 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; 7+ 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] 7+ 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; 7+ 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] 7+ 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 ` bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop 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; 7+ 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] 7+ 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 ` bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop 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
2 siblings, 1 reply; 7+ 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] 7+ 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
0 siblings, 0 replies; 7+ 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] 7+ messages in thread