diff options
| -rw-r--r-- | BUGS | 6 | ||||
| -rw-r--r-- | doc/NewDoc.texi | 43 | ||||
| -rw-r--r-- | todo | 22 |
3 files changed, 57 insertions, 14 deletions
@@ -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 @@ -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) |