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 <address@hidden> 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
                                address@hidden