Custom Query (361 matches)
Results (28 - 30 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #445 | worksforme | Proof General (or coqtop?) barfs on "Arguments foo / ..." | ||
| Description |
When I make a new file containing the two (literal) line Definition foo a : Type := a. Arguments foo / ... and try to evaluate it when running Coq 8.4beta2, PG accepts the first line fine (highlights it blue), highlights the second line pink, marks it as read-only, and refuses to do anything more with Coq; it refuses to stop coq with ctrl+c, ctrl+c, it gives me the following error when I try to retract the buffer and start over: proof-add-to-queue: Assertion failed: (eq proof-shell-busy queuemode) and it never finishes evaluating the line (where never >= 15 seconds). Given that coqtop sits there using 0% CPU and 8 MB of RAM, and coqc errors and quits after 2s, I'm inclined to think that this is either a PG problem, or a communication problem. |
|||
| #460 | worksforme | proof general hanging on Coq Definition in file generated by Why3 | ||
| Description |
When I try to process the attached Coq file using ProofGeneral, it gets hung up on the Definition of IB6_IB7_QueryTags_First. In contrast, coqtop file works on this file. The file was generated by Why3's Coq driver, so maybe it's doing something that's syntactically unusual. I'm running PG 4.1 on GNU Emacs 24.2.1. The Coq version is 8.3pl4. |
|||
| #92 | duplicate | Attempt recovery from XML parse errors in PGIP main loop | ||
| Description |
Isabelle exits in case of erroneous XML input. It could be made more robust, which, e.g., helps debugging in case of editing XML by hand.
One suggestion is to attempt recovery by scanning for the next
See proof_general_pgip.ML, function |
|||
