Ticket #442 (closed defect: duplicate)

Opened 22 months ago

Last modified 19 months ago

Emacs 24 and long inputs

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


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

comment:1 Changed 22 months ago by da

Note, problem is reported with PG 4.1.

comment:2 follow-up: ↓ 3 Changed 20 months ago by da

  • Status changed from new to closed
  • Resolution set to duplicate

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

comment:3 in reply to: ↑ 2 Changed 19 months 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.


Note: See TracTickets for help on using tickets.