Opened 6 years ago

Closed 6 years ago

Last modified 6 years ago

#442 closed defect (duplicate)

Emacs 24 and long inputs

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

Description

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

Change History (3)

comment:1 Changed 6 years ago by David Aspinall

Note, problem is reported with PG 4.1.

comment:2 Changed 6 years ago by David Aspinall

Resolution: duplicate
Status: newclosed

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

comment:3 in reply to:  2 Changed 6 years ago by 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

Note: See TracTickets for help on using tickets.