Sending too-large definitions gets stuck

[coquser]

With a sufficiently large definition, as attached, Proof General never finishes advancing past it, and also can't retract until I send an interrupt or kill the Coq process.

I'm using Coq 8.4, emacs 24.1.1, and have tried both the stable and development releases of Proof General.

It works fine in coqide, or as coqtop -emacs < bug.v.

[coquser]

A long inductive defintion.

[coquser]

I can reproduce this in a vanilla emacs 24.2. I believe this is an emacs problem. process-send-region inside scomint-send-input is called with the right parameters. However, the external process only receives the first 4096 characters.

Hendrik

[coquser]

I see the same truncation of long lines with shell mode in emacs 24.1.1, so it's not just ProofGeneral.

[coquser]

Emacs 24 only sends the first 4K when sending large strings to processes. Try

(let* ((process-connection-type t)
       (process (start-process "cat" (current-buffer) "cat")))
  (process-send-string process (format "%s\n" (make-string 6000 ?a))))

in emacs 23, this inserts all 6000 characters in the current buffer. In 24 you only get 4K.

However, if process-connection-type is nil, everything works fine. Therefore, please try setting proof-shell-process-connection-type to nil.

I reported this as emacs bug already.

Bye,

Hendrik

[coquser]

The emacs bug is at ​http://debbugs.gnu.org/cgi/bugreport.cgi?bug=12440

BTW, why is Proof General using PTY's for running the proof assistant?

Hendrik

[David Aspinall]

Thanks for doing the detective work Hendrik!

I'm closing this as upstream, although we could change the default for process-connection-type to avoid it (sigh).

At one point PTYs became the better choice over pipes, I don't recall exactly why, maybe pipes were getting tired after some 64k limit or something. It is all back in the midst of time...