prioritised

1 files changed, 61 insertions, 30 deletions

diff --git a/todo b/todo
index 9545d6ea..f916e77e 100644
--- a/todo
+++ b/todo
@@ -1,75 +1,106 @@
 -*- mode:outline -*-
+
+* Priorities
+============
+A (High)   to be fixed before release
+B (Medium) desirable to fix at some point
+C (Low)    probably not worth wasting time on
+
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
-o Implement proof-find-previous-terminator and bind it to C-c C-a
+A Structured review of complete system (2h hhg & tms)
+
+A Update documentation, in particular document bugs and workarounds
+  (4h hhg & tms) 
+
+A Implement more generic mechanism for large undos (2h)
+
+    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?
+    
+B Implement proof-find-previous-terminator and bind it to C-c C-a
+  (45min tms)
+
+B Technical documentation to record expertise and allow users of other
+  proof systems to adopt generic package (40h hhg & tms)
 
-o Fixing up errors caused by pbp-generated commands.
+B Port packages to XEmacs 20
 
-o pbp code doesn't quite accord with the tech report; in particular it
+A Fixing up errors caused by pbp-generated commands; currently, script
+  management unwisely assumes that pbp commands cannot fail (2h tms)
+
+C pbp code doesn't quite accord with the tech report; in particular it
   decodes annotations eagerly. Lazily would be faster, and it's what
   the tech report claims
   --- djs: probably not much faster, actually.
 
-o It would be nice to have a version ported to emacs19 (or
+C It would be nice to have a version ported to emacs19 (or
   20). Unfortunately, it's currently impossible to port the pbp code,
   since emacs19 doesn't properly handle highlighting of nested
   overlays. The bulk of the stuff dependent on which version of emacs
   is running has been moved to proof-dependencies.el, but there are
   doubtless differences in font-locking and menu code which will
-  require some work.
+  require some work. One should check regularly if extents become
+  available in emacs19
 
-o file handling could be more robust; perhaps one should always cd to
+B file handling could be more robust; perhaps one should always cd to
   the directory corresponding to the script buffer (currently only
-  done for the buffer which starts up the proof system)
+  done for the buffer which starts up the proof system) (30min tms)
 
-o LEGO and Coq modes overwrite each other.
+C LEGO and Coq modes overwrite each other.
 
-o We need to go over to piped communication rather than ptys to fix
+C We need to go over to piped communication rather than ptys to fix
   the (Solaris) ^G bug. In this circumstance there's a bug in the
   eager annotation code
 
-o Outline-mode does not work due to read-only restrictions of
+C Outline-mode does not work due to read-only restrictions of
   protected region
 
 * Here are things to be done to Lego mode
 =========================================
 
-o undo support for LEGO needs to consider Discharge; perhaps unrol to
-  the beginning of the module?
-
-o LEGO mode might incorporate changes to Coq mode menu, in particular
-  making help refer to the info file.
+A LEGO mode might incorporate changes to Coq mode menu, in particular
+  making help refer to the info file (30min tms)
 
-o Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
+A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
   annotations are recorded in the object file. This needs to be
-  changed in the SML code.
+  changed in the SML code. (initially 2h tms)
 
-o Mechanism to save object file (does this apply to Coq as well?)
+C Mechanism to save object file
 
-o Equiv, Next,... aren't handled properly, because LEGO does not
+A Equiv, Next,... aren't handled properly, because LEGO does not
   refresh the proof state. Perhaps it would be easiest to get LEGO to
-  output more information in proof script mode
+  output more information in proof script mode (2h tms)
+
+A Error messages need to be revised e.g., if an import fails, LEGO
+  outputs
 
-o due to bugs in the LEGO system, object files may fail.
-  Script-management needs to be aware of this problem.
+    Error in file: search: undefined or out of context: should
+   (* closing file ./blah.l; time= 0.010000  gc= 0.0  sys= 0.0 *)
+   Error: Unwinding to top-level
+
+  but script management only prints the last line. (5h tms)
 
 * Here are things to be done to Coq mode
 ========================================
 
-o Restart if going back to beginning of proof.
-
-o C-c u inside a Section should reset the whole section, then redo defns
+A Restart if going back to beginning of proof. (30min hhg)
 
-o There's a bug so the goal buffer isn't displaying everything that
+? There's a bug so the goal buffer isn't displaying everything that
   happens.
 
-o Sections and files are handled incorrectly.
+C Sections and files are handled incorrectly.
 
-o Update documentation to include C-c C-s.
+A Update documentation to include C-c C-s. (10min hhg)
  
-o Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
+A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
   correct command if I undo up to the lower lemma, but the buffer
   undoes to the upper lemma.  I.e., if I start Lemma x, then prove
   Lemma y, then finish x, and undo lemma x, then lemma y gets undone
-  in the buffer as well.
+  in the buffer as well. (45min hhg)
+
+B Proof-by-Pointing (10h hhg)