Opened 12 years ago
Closed 12 years ago
#447 closed defect (duplicate)
Proof General stalls on long Ltac (Coq)
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.2 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
Proof general seems to stall when trying to evaluate very long (textually long) ltac declarations. See example at the end. If you remove a line or two of the "let x := match ... in" then there is no problem. Is there a limit to the size of expressions that are fed to Coq?
Ltac bar k := k tt. Ltac foo x := bar ltac:(fun a => bar ltac:(fun b => bar ltac:(fun c => bar ltac:(fun d => bar ltac:(fun e => bar ltac:(fun f => bar ltac:(fun g => bar ltac:(fun h => let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in let x := match tt with | tt => constr:(1) end in idtac)))))))).
Attachments (1)
Change History (5)
comment:1 Changed 12 years ago by
Status: | new → accepted |
---|
comment:2 Changed 12 years ago by
Another example reported: 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.
It works fine in coqide, or as coqtop -emacs < bug.v.
comment:3 Changed 12 years ago by
Please try with proof-shell-process-connection-type set to nil, see #453 for more info.
Hendrik
I can repeat this problem on Ubuntu. I'm not sure where the problem is. PG seems to send the input as usual, but doesn't see a response. It seems to have something to do with the line length as even if the input text is commented rather than deleted, the problem still happens.
Perhaps the input or output is getting lost in the C-level buffering somehow (we saw issues like this years ago with UTF-8 prefix characters being inadvertently used in the output stream and low-level C libraries blocking while they waited for following chars).