documented problem with Discharge in LEGO

3 files changed, 57 insertions, 14 deletions

diff --git a/BUGS b/BUGS
index 8bfb6856..be0f5e1b 100644
--- a/BUGS
+++ b/BUGS
@@ -59,6 +59,12 @@ FSF Emacs specific bugs
 LEGO Proof General Bugs
 =======================
 
+* After a `Discharge', retraction ought to only be possible back to the
+first declaration/definition which is discharged. However, LEGO Proof
+General does not know that Discharge has such a non-local effect.
+Workaround: retract back to the first declaration/definition which is
+discharged.
+
 * A thorny issues are local definitions in a proof state. LEGO cannot
 undo them explicitly. Workaround: retract back to a command before a
 definition.
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi
index 9c04543d..cdbab281 100644
--- a/doc/NewDoc.texi
+++ b/doc/NewDoc.texi
@@ -128,7 +128,7 @@ Isabelle.
 * Index::                       
 @end menu
 
-@detailmenu --- The Detailed Node Listing ---
+@detailmenu  --- The Detailed Node Listing ---
 
 Introducing Proof General
 
@@ -166,17 +166,18 @@ Advanced Script Management
 Support for other Packages
 
 * Support for function menus::  
+* Support for tags::            
 
 Customizing Proof General
 
 * Easy customization::          
 * Setting the user options::        
-* Running on another machine::  
 * Tweaking configuration settings::  
 
 LEGO Proof General
 
 * LEGO specific commands::      
+* LEGO tags::                   
 * LEGO customizations::         
 
 Coq Proof General
@@ -216,11 +217,25 @@ Obtaining and Installing Proof General
 * Installing Proof General from tarball::  
 * Installing Proof General from RPM package::  
 * Notes for syssies::           
-@end detailmenu
 
-@end ifinfo
+Known bugs and workarounds
+
+* Bugs at the generic level::   
+* Bugs specific to LEGO Proof General::  
+* Bugs specific to Coq Proof General::  
+* Bugs specific to Isabelle Proof General::  
 
+Bugs specific to LEGO Proof General
 
+* Retraction and @code{Discharge}::  
+* Retraction and proving::      
+
+Plans and ideas
+
+* Granularity of Atomic Command Sequences::  
+* Browser mode for script files and theories::  
+@end detailmenu
+@end ifinfo
 
 @node Introducing Proof General
 @chapter Introducing Proof General
@@ -256,7 +271,6 @@ features at the generic level wherever possible.  See
 for more details, and send ideas, comments, patches,
 and code to @code{proofgen@@dcs.ed.ac.uk}.
 
-
 @menu
 * Quick start guide::           
 * Features of Proof General::   
@@ -1653,6 +1667,25 @@ provers you need.
 @node Bugs specific to LEGO Proof General
 @section Bugs specific to LEGO Proof General
 
+@menu
+* Retraction and Discharge::    
+* Retraction and proving::      
+@end menu
+
+@node Retraction and Discharge
+@subsection Retraction and Discharge
+
+After a @code{Discharge}, retraction ought to only be possible back to
+the first declaration/definition which is discharged. However, LEGO
+Proof General does not know that Discharge has such a non-local effect.
+
+@strong{Workaround:} retract back to the first declaration/definition
+which is discharged.
+
+@node Retraction and proving
+@subsection Retraction and proving
+@cindex Retraction
+
 Getting retracting right is tricky when working on proofs. 
 
 @unnumberedsubsec Definitions in a proof state 
diff --git a/todo b/todo
index 8bf9ff1c..c7b55385 100644
--- a/todo
+++ b/todo
@@ -175,14 +175,6 @@ C Clean up proof-assert-until-point behaviour.  Discussion results:
     when new commands are added to the buffer needs careful
     thought! (1h)
 
-B Implement more generic mechanism for large undos (4h tms)
-
-    COQ: C-c u inside a Section should reset the whole section, then
-         redo defns 
-
-    LEGO: consider Discharge; perhaps unrol to the beginning of the
-          module?
-
 D Provide a sensible default frame/buffer layout (4h)
 
 C A less drastic version of proof-restart-script would be useful:
@@ -387,7 +379,11 @@ X pbp code doesn't quite accord with the tech report; in particular it
 * Here are things to be done to Lego mode
 =========================================
 
-C fix Pbp implementation (10h)
+C In LEGO, apart from Goal...Save pairs, we have
+  declaration...discharge pairs. See the section "Granularity of
+  Atomic Commands" for a proposal on how to generalise the current
+  implementation so that it can also deal with "Discharge".
+  [See also the Coq problem with Sections] (6h)
 
 C Inoking an "Expand" command produces a new proof state. But this is
   incorrectly displayed in the response buffer and not the goals
@@ -395,6 +391,8 @@ C Inoking an "Expand" command produces a new proof state. But this is
   ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the
   definition of "Expand" (see file newtop.sml [Version 1.4]). (30min)
 
+C fix Pbp implementation (10h)
+
 B release new version of the LEGO proof engine (4h tms)
 
 X Mechanism to save object file
@@ -408,6 +406,12 @@ D Improve legotags. It cannot handle lists e.g., with
 * Here are things to be done to Coq mode
 ========================================
 
+C Retraction in a Section should retract to the beginning of the whole 
+  section. See the section "Granularity of
+  Atomic Commands" for a proposal on how to generalise the current
+  implementation so that it can also deal with sections.
+  [See also the LEGO problem with Discharge] (6h)
+
 A* Implement multiple file handling.
 
 C derive a coq-response-mode from proof-response-mode; see lego.el (10min)