Opened 9 years ago
Last modified 9 years ago
#499 new defect
delays between coq messages can cause PG to duplicate some
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | duplicate messages |
| Cc: | jonikelee@… |
Description
Long delays between messages issued from tactics can confuse PG into duplicating some of them. Here's an example:
Goal True. idtac 1; idtac 2; idtac 3; idtac 4; do 1000000 idtac; idtac 5.
prints (on separate lines): 1 2 3 4 4 5 5
The amount of delay in the do loop might need to be altered to reproduce this.
Note: See
TracTickets for help on using
tickets.
I confirm this bug, but I have no idea where it comes from. Maybe David when he has some time...