New/updated information files

3 files changed, 70 insertions, 12 deletions

diff --git a/lego/BUGS b/lego/BUGS
new file mode 100644
index 00000000..bfe39752
--- /dev/null
+++ b/lego/BUGS
@@ -0,0 +1,53 @@
+-*- mode:outline -*-
+
+* LEGO Proof General Bugs
+
+See also ../BUGS for generic bugs.
+
+
+** PBP doesn't work on FSF, reason mentioned in generic bugs.
+
+** [FSF specific] `proof-zap-commas-region' does not work for Emacs
+  
+  On lego/example.l . On *initially* fontifying the buffer,
+  commas are not zapped [unfontified]. However, when entering text,
+  commata are zapped correctly. Workaround: don't stare too much at commata
+
+** If LEGO attempts to write a (object) file in a non-writable directory
+
+  It forgets the protocol mechanism on how to interact with 
+  Proof General and gets stuck. Workaround: Directly enter "Configure
+  AnnotateOn" in the Proof Shell to recover.
+
+** 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 issue is 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 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.
+ 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.
+
+
diff --git a/lego/README b/lego/README
index a8fa6850..2ddd6fd1 100644
--- a/lego/README
+++ b/lego/README
@@ -5,11 +5,17 @@ Later maintainance by David Aspinall and Paul Callaghan.
 
 $Id$
 
+Status:		supported
+Maintainer:	Paul Callaghan / David Aspinall
+LEGO version:	1.3.1
+LEGO homepage:	http://www.lfcs.informatics.ed.ac.uk/lego
+
+========================================
+
 LEGO Proof General has full support for multiple file scripting, and
 experimental support for proof by pointing.
 
-There is support for x-symbols, but not using a proper token
-language.  Try writing "philosophy" !
+There is support for X Symbol, but not using a proper token language.
 
 There is a tags program, legotags.
 
diff --git a/lego/todo b/lego/todo
index 99a8154e..dc0b1f28 100644
--- a/lego/todo
+++ b/lego/todo
@@ -1,27 +1,26 @@
 -*- mode:outline -*-
 
-* See also ../todo for generic things to do, priority codes.
+* Things to do for LEGO
 
-* Things to do for Lego
-=======================
+See also ../todo for generic things to do, priority codes.
 
-C Improve X-Symbol support.
+** C Improve X-Symbol support.
 
-D Fix Pbp implementation in LEGO itself (10h)
+** D Fix Pbp implementation in LEGO itself (10h)
 
-D In LEGO, apart from Goal...Save pairs, we have
+** D 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)
 
-D Inoking an "Expand" command produces a new proof state. But this is
+** D Inoking an "Expand" command produces a new proof state. But this is
   incorrectly displayed in the response buffer and not the goals
   buffer because special annotations are missing. Presumably, one
   ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the
   definition of "Expand" (see file newtop.sml [Version 1.4]). (30min)
 
-D Even with the more flexible region model, with 
+** D Even with the more flexible region model, with 
   proof-nested-goals-behaviour=closequick, Proof General doesn't
   do quite the right thing.  Forget for a definition when inside
   a proofstate kills off the whole proofstate.  Effectively,
@@ -34,11 +33,11 @@ D Even with the more flexible region model, with
   some retraction action.  More generally this could be used for error
   handling.
 
-D Improve legotags. It cannot handle lists e.g., with 	
+** D Improve legotags. It cannot handle lists e.g., with 	
     [x,y:nat];
   it only tags x but not y. [The same problem exists for coqtags]
 
-X Mechanism to save object file. Specifically, after having processed
+** X Mechanism to save object file. Specifically, after having processed
   a script (interactively), it would be nice if one could now save the
   buffer in object format. At the moment, it only gets converted
   (automatically) when it is read in indirectly at a later stage.