diff options
| -rw-r--r-- | BUGS | 43 | ||||
| -rw-r--r-- | doc/NewDoc.texi | 7 | ||||
| -rw-r--r-- | doc/notes.txt | 2 | ||||
| -rw-r--r-- | todo | 8 |
4 files changed, 53 insertions, 7 deletions
@@ -36,3 +36,46 @@ allocation. Maybe some of the spans aren't removed properly. Setting a limit on the size of the process buffer doesn't seem to help. (1998/10/06: Is this bug still present? Test examples?) +*`proof-zap-commas-region' does not work for Emacs 20.2 on + lego/example.l . On *initially* fontifying the buffer, + commas are not zapped. However, when entering text, commata are + zapped correctly. Workaround: don't stare too much at commata + +*`proof-find-next-terminator' (bound to C-c C-e) doesn't work +properly. Workaround: use other means to navigate in a proof scipt +buffer. + + +LEGO Proof General Bugs +======================= + +* A thorny issues are local definitions in a proof state. LEGO cannot +undo them explicitly. Workaround: retract back to a command before a +definition. + +* Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone +in a proof state by the Proof General. Workaround: retract back to the +start of the proof. + +* After LEGO has issued a `*** QED ***' you may undo steps in the proof +as long as you don't issue a `Save' command or start a new proof. The +LEGO Proof General assumes that all proofs are terminated with a +proper `Save' command. Workaround: Always issue a `Save' command after +completing a proof. If you forget one, you should retract to a point +before the offending proof development. + +*legotags doesn't find all declarations. It cannot handle lists e.g., +with [x,y:nat]; it only tags x but not y. [The same problem exists for +coqtags] Workaround: don't rely too much on the etags mechanism. + +Coq Proof General Bugs +====================== + +*coqtags doesn't find all declarations. It cannot handle lists e.g., +with "Parameter x,y:nat" it only tags x but not y. [The same problem +exists for legotags] Workaround: don't rely too much on the etags +mechanism. + +*user defined tactics cannot be retracted. Workaround: you may need to +retract to the beginning of the proof. + diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index 157bc477..1af8d002 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -1311,6 +1311,7 @@ let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. @menu * Bugs at the generic level:: * Bugs specific to LEGO Proof General:: +* Bugs specific to Coq Proof General:: @end menu @node Bugs at the generic level @@ -1370,8 +1371,12 @@ that all proofs are terminated with a proper @samp{Save} command. a proof. If you forget one, you should retract to a point before the offending proof development. +@node Bugs specific to Coq Proof General +@section Bugs specific to Coq Proof General - +The collection of tactics which Proof General is aware of is hard-wired. +Thus, user-defined tactics cannot be retracted. +@strong{Workaround:} You may need to retract to the start of the proof. @node Plans and ideas @appendix Plans and ideas diff --git a/doc/notes.txt b/doc/notes.txt index fd32d00b..dfc585d9 100644 --- a/doc/notes.txt +++ b/doc/notes.txt @@ -75,7 +75,7 @@ Suggestion for outline of improved documentation. APPENDIX A. Obtaining and installing the software [da] - B. Known bugs [tms] + B. Known bugs [done] C. Future ideas and plans [da] @@ -273,8 +273,6 @@ C Reengineer *-count-undos and *-find-and-forget at generic level D Allow bib-cite style clicking on Load/Import commands to go to file. -D support font-lock in goal buffer - C Unify toolbar and menu functions. (1h) D Remove duplication of variables e.g., proof-prog-name and @@ -414,7 +412,7 @@ B release new version of the LEGO proof engine (4h tms) X Mechanism to save object file -D Improve legotags. I cannot handle lists e.g., with +D Improve legotags. It cannot handle lists e.g., with [x,y:nat]; @@ -435,12 +433,12 @@ D Add Patrick Loiseleur's commands to search for vernac or ml files. X Sections and files are handled incorrectly. -D Proof-by-Pointing (10h hhg) +D Proof-by-Pointing (10h) D Add coq-add-tactic with a tactic name, which adds that tactic to the undoable tactics and to the font-lock. (2h) -D Improve coqtags. I cannot handle lists e.g., with +D Improve coqtags. It cannot handle lists e.g., with Parameter x,y:nat |