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)

bug.v (5.9 KB) - added by David Aspinall 12 years ago.
Another example of long input causing a bug

Download all attachments as: .zip

Change History (5)

comment:1 Changed 12 years ago by David Aspinall

Status: newaccepted

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

comment:2 Changed 12 years ago by David Aspinall

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.

Changed 12 years ago by David Aspinall

Attachment: bug.v added

Another example of long input causing a bug

comment:3 Changed 12 years ago by coquser

Please try with proof-shell-process-connection-type set to nil, see #453 for more info.

Hendrik

comment:4 Changed 12 years ago by David Aspinall

Resolution: duplicate
Status: acceptedclosed

See #453

Note: See TracTickets for help on using tickets.