Emacs 24 and long inputs

[David Aspinall]

Hello, I tried proofgeneral on the newly released emacs and it works at first sight but seems to have some problems with long input, like the one produced by this bash script:

function mk { echo "Check fun n, match n with "; s=O; for ((i=0;i<$1;i++)); do 
echo "  | $s => n"; s="(S $s)"; done; echo "  | _ => n end."; } > x.v

Processing x.v for small arguments like $ mk 10 works but for bigger ones like $ mk 100 it blocks without consuming cpu. Weirdly for me the threshold seems to be 42...

[David Aspinall]

Note, problem is reported with PG 4.1.

[David Aspinall]

Seems not to be Emacs 24 specific. See #447, probably the same problem.

[coquser]

Seems not to be Emacs 24 specific. See #447, probably the same problem.

But #447 is Emacs 24 specific, isn't it? And this problem as well: I can only reproduce it with Emacs 24.

The treshhold is 42, because for 42 it is just below 4K.

Try with proof-shell-process-connection-type set to nil.

Hendrik