-*- mode:outline -*- $Id$ * Priorities ============ A (High) to be fixed before release (Version 2.0) B would be nice to fix before release of 2.0; but not crucial D (Medium) desirable to fix at some point X (Low) probably not worth wasting time on * This is a list of things which need doing in the generic interface ==================================================================== A proof-toolbar: Add support for entering a goal and saving a theorem at the generic level. These functions should also be accessible from menus. Fixup movement of point (choice of up and down functions). Add toolbar to pbp mode too. (1hr, da) A Add xbm bitmap images for toolbar. Probably important to support non-colour displays. (30mins, da) X Improve toolbar icons. Automatically generate reduced and pressed/greyed-out versions from gimp xcf files. Keep the xcf files under CVS rather than xpm files. (5h or more to design nice ones) A Documentation for proof-mode and its derived modes. (5min) A Clean up proof-assert-until-point behaviour. At the moment we get an odd error if it is run in the locked region. If point is on the start of a command it says "nothing to do", but if it is one character into the command, it asserts the whole command! I propose the new function proof-assert-next-command as a possible alternative/additional behaviour, bound to C-c C-RET. Another question is whether the point is moved afterwards or not. I suspect it is useful to leave point where it is, so we can easily edit one step in a proof, try the next few steps, then undo them, try a variation, etc. As an experiment, proof-assert-next-command does not advance point. (da, tms/others to assess) A A less drastic version of proof-restart-script would be useful: one that doesn't involve killing off the proof assistant process and restarting that -- it can take ages! (da, 20mins) D Code in proof.el assumes all characters with top bit set are special instructions to Emacs. This is rather arrogant, and precludes proof systems which utilize 8-bit character sets! Needs repair. (3h) A Add a small script "example.l" etc to each of the prover subdirectories, for testing/example purposes. (Perhaps proving the same thing? commutativity of conjunction?) Only needed for Coq now. (10min, hhg) D Prune dead code. (1h) D Add support to proof.el for *not* setting variables for commands which aren't supported by a prover. For example, in Isabelle there is no such thing as killing a goal. For the minimum set of variables to cover, see FIXME's in isa.el (da, 1.5hrs) D Outsource script management features from proof.el to proof-script.el (1h) A Write function proof-retract-file. (30min tms) Currently, the command ForgetMark (for LEGO) is hardwired in proof-steal-process. D Improve documentation in proof.el to help porting/understanding Also add notes into proof.texinfo. (ongoing, da). B Fixup sources to follow Elisp conventions better. The first line of documentation of functions and variables should be a whole sentence. Subsequent lines should *not* be indented. See output of hyper-apropos and poor formatting of current comments. (1hr, tms) A Update source documentation and manual, in particular document bugs and workarounds (4h hhg & tms & da) D Technical documentation to record expertise and allow users of other proof systems to adopt generic package (40h 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? A Multiple files are sometimes handled incorrectly, because the function `proof-steal-process' cannot figure out that some files have already been processed. This is most likely caused by the ad-hoc equality test on file names. Instead, one could employ the built-in `file-truename' to trigger *canonical* file names. (1h tms) D Implement proof-find-previous-terminator and bind it to C-c C-a (45min tms) D Support for x-symbols package. Provers with sophisticated/configurable syntax should tell Emacs about their syntax somehow, rather than trying to duplicate specifications inside Emacs. A 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). This could be achieved with a hook which is not set by default. [Remember to add user documentation] (30min tms) A replace (current-buffer) by proof-shell-buffer/proof-script-buffer where ever possible (30 min tms) A Replace "You are not authorised for this information." by a proper documentation (2h, da) A Reengineer *-count-undos and *-find-and-forget at generic level (3h) D Allow bib-cite style clicking on Load/Import commands to go to file. D support font-lock in goal buffer X 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. Document this problem so that it can be tested for future versions. [Currently the problem is documented in Email messages sent to lego] B Introduce keybinding to save the proof e.g., in LEGO, this should insert "Save id" or "$Save id" depending on the name of the theorem. Do the same thing for Goal, to add as a toolbar function. B Unify toolbar and menu functions. A use proof buffer instead of response buffer and leave non-proof state output in the process buffer (2h tms) D Remove duplication of variables e.g., proof-prog-name and lego-prog-name for Coq and Lego. (1h) D Fixup implementation of "spans": Add documentation! (30 mins) X Comment support is not very generic: we don't support end-of-line terminated comments. Is there any case where this might be worthwhile? (2h to add it). * Proof-by-Pointing =================== A Fixing up errors caused by pbp-generated commands; currently, script management unwisely assumes that pbp commands cannot fail (2h tms) A Rename pbp-mode to response-mode or goals-mode (which doesn't support any actual proof-by-pointing) (30min) A Outsource actual pbp/goals functionality (30min) (separate pbp annotations from other annotations). Make a file proof-goals.el. X 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. * Here are things to be done to Lego mode ========================================= A fix Pbp implementation (10h; 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) A release new version of the LEGO proof engine (4h tms) B 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) B LEGO should not issue warning messages triggered by the interactive use of the Module command when invoked by the interface e.g., Lego> Module nstderror Import stderror; Including module nstderror Warning: module name "nstderror" does not equal filename ""! Warning: Interactive use of Module command. X Mechanism to save object file * Here are things to be done to Coq mode ======================================== D set proof-commands-regexp to support indentation for commands (10min hhg) D Add Patrick Loiseleur's commands to search for vernac or ml files. X Sections and files are handled incorrectly. 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) [ This seems to have corrected itself... hhg ] D Proof-by-Pointing (10h hhg) A Add coq-add-tactic with a tactic name, which adds that tactic to the undoable tactics and to the font-lock. (2h hhg) * Here are things to be done to Isabelle Mode ============================================= A Get basic features working: proof state extraction -- okay. undo -- needs work (undoes to much). error detection -- seems okay. what else? Check these things: abort-goal-regexp D Write perl scripts to generate TAGS file for ML and thy files. (6h, I've completely forgotten perl) D Add useful specific commands for Isabelle. Many could be added. Would be better to merge in Isamode's menus. (probably a week's work to bring together Isamode and proof.el, making some of Isamode generic) D Add ability to choose logic. Maybe not necessary: can use default set in Isabelle settings nowadays, in the premise that most people stick to a particular logic? But then no support for loading user-saved databases. (ponder this) X New features ideas: 1. Manage multiple proofs (markers in possibly different buffers) * Emacs19 ========= D The proof-locked-span isn't set to read-only, because overlays don't have that capability. This needs to be done with text-regions. (2hr hhg) * Release ========= A remove CVS history in all files (replace with idents $Id) A extend Copyright to 1998 A fix INSTALL file, add COPYING note A fix branches after renames A write Makefile targets to build documentation formats and generate distributable tar.gz file, tag sources, compile .elc, web page (?), with release version.