Opened 8 years ago

Closed 8 years ago

#453 closed defect (upstream)

Sending too-large definitions gets stuck

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.2
Component: 2:pg-emacs Keywords:


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.

Attachments (1)

bug.v (5.9 KB) - added by coquser 8 years ago.
A long inductive defintion.

Download all attachments as: .zip

Change History (6)

Changed 8 years ago by coquser

Attachment: bug.v added

A long inductive defintion.

comment:1 Changed 8 years ago by 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.


comment:2 Changed 8 years ago by coquser

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

comment:3 Changed 8 years ago by 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.



comment:4 Changed 8 years ago by coquser

The emacs bug is at

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


comment:5 Changed 8 years ago by David Aspinall

Resolution: upstream
Status: newclosed

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

Note: See TracTickets for help on using tickets.