Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[John Wiegley]

[-- 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 --]

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[Anders Lindgren]

[-- 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 --]

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[Clément Pit--Claudel]

[-- 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 --]

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[John Wiegley]

>>>>> 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

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[Anders Lindgren]

[-- 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 --]

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[YAMAMOTO Mitsuharu]

>>>>> 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

Re: bug#22865: 25.0.91; Use Proof General with emacs-25 on OS X frequent hangs coqtop

[Wolfgang Jenkner]

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