completed chapter on Known bugs. However section on Isabelle Proof

General specific bugs is still missing.

1 files changed, 43 insertions, 0 deletions

diff --git a/BUGS b/BUGS
index d50971a1..9dc47716 100644
--- a/BUGS
+++ b/BUGS
@@ -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.
+