diff options
Diffstat (limited to 'todo')
| -rw-r--r-- | todo | 106 |
1 files changed, 106 insertions, 0 deletions
@@ -0,0 +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 +==================================================================== + +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) + +B Port packages to XEmacs 20 + +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. + +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. One should check regularly if extents become + available in emacs19 + +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) (30min tms) + +C LEGO and Coq modes overwrite each other. + +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 + +C Outline-mode does not work due to read-only restrictions of + protected region + +* Here are things to be done to Lego mode +========================================= + +A LEGO mode might incorporate changes to Coq mode menu, in particular + making help refer to the info file (30min tms) + +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. (initially 2h tms) + +C Mechanism to save object file + +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 (2h tms) + +A Error messages need to be revised e.g., if an import fails, LEGO + outputs + + 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 +======================================== + +A Restart if going back to beginning of proof. (30min hhg) + +? There's a bug so the goal buffer isn't displaying everything that + happens. + +C Sections and files are handled incorrectly. + +A Update documentation to include C-c C-s. (10min hhg) + +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. (45min hhg) + +B Proof-by-Pointing (10h hhg) |