-*- mode:outline -*- Proof General Low-level List of Things to Do ============================================ $Id$ * Contents ========== * Priorities * Things to do in the generic interface * Things to do for Proof-by-Pointing * Things to do for Lego * Things to do for Coq * Things to do for Isabelle * FSF Emacs issues * Stable version release checklist * Things to do for Proof General Project * Priorities ============ A (URGENT) to be fixed immediately for next pre-release B to be fixed before next release (Version 2.1) C would be nice to fix before release of 2.1; but not crucial D (Medium) desirable to fix at some point X (Low) probably not worth spending time on * Things to in the generic interface ==================================== A Usability enhancements: 1. Movement of point after assert/retract commands - configure by default for one command/line. - Add option for many commands per line. - Maybe shell like behaviour with pressing return? 2. Optional argument to delete region removed from C-c C-u 3. Extra toolbar and menu commands - Toolbar button to display current proof state D bug: outline mode when proof-strict-read-only is nil ought to work, but there may be problems. D bug: mentioned by Martin H. with Lego: "don't know what I should be doing..." error when it shouldn't happen. C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting ELISP_DIRS somehow. D Update logo to include new "???" prover badge (maybe it should be "...") from graphics file elsewhere (da) D Add etc/announce to web pages somewhere. B Improve relocatability of RPM package, and produce package for XEmacs which installs directly under ~/.xemacs/packages. C Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. C Check compilation okay, check on use of eval-and-compile. C Support for proof-guess-command-line, new generic setting added by Patrick. D Key binding and interface issues - Consider change for prefix argument for C-c C-u and C-c u, it's quite easy to accidently delete by pressing C-c C-u repeatedly. D CVS repository issues. Where are obsolete 'fileattr' files generated from/maintained? Should junk these (which appear to say that tms is watching everything). B QUESTION: why do we have proof-shell-proof-completed-regexp's perhaps objectionable behaviour of forcing the response buffer? Would it be safe just to set the proof-shell-proof-completed flag and output as usual? (The effect would be to allow Isabelle's completed proof message to appear in the goals buffer since it's marked up as a proof state output) C proof-shell-exit has a time delay of 10 secs built-in, before which the process is killed off. This should be configurable to allow for proof assistants which really want to do some work before exiting, for example writing persistent databases out or the like. Also this fact should be documented. C Add support for XEmacs 21 packaging. Make suitable updates available on web page, and make RPM put things in the right place so no .emacs file may need editing(?). [4 hours] B Fixup display problems. The window dedicated stuff is a real pain and I've spent ages inserting workarounds. Why do we want it?? The latest problem is that with (setq special-display-regexps (cons "\\*Inferior .*-\\(goals\\|response\\)\\*" special-display-regexps)) I get the script buffer made into a dedicated buffer, presumably because the wrong window is selected in proof-display-and-keep-buffer? B Make completion more generic. For Isabelle and Lego, we can build a completion table by querying the process, which is better than messing with tags. B outline configuration should be generic (or else documented for each prover separately, since not guaranteed to work for all). B Improve behaviour when switching active scripting buffer. Now kill buffer function retracts partially-processed files and removes them from proof-included-files-list, we could allow switching between scripting buffers automatically, (perhaps with an option akin to the old "steal scripting?" idea). B Check matching code carefully, in view of bug reported (now fixed) for Isabelle. Examine syntax tables for all instances, and whether word matching is based on whitespace constituents or non-word constituents. [6 hrs] C Reorganize menus in a better way. Have generic scripting commands for keyboard or menu/toolbar use. (2hrs) C Implement proof-auto-retract idea. (4hrs) C Make and test generic versions of <..>-goal-command-p, <...>-count-undos, to simplify prover-specific code. C Improve handling of process exiting early (see note at end of proof-shell-mode). (30mins) C da: Suggested improvement to interface for included files: Currently have two cases: processing a single file, and retracting which updates the included file list arbitrarily (but assumes that only removals are made). A simpler and more general interface would be to just have the second case, and automatically find removed files and added files between two versions of proof-included-files-list and unlock or lock buffers appropriately. We could provide a useful default function based on three regexps: retract-file-regexp, add-file-regexp, clear-filelist-regexp. Master regexp process-file-regexp would match all of these cases. Could be multiple matches of the three above within a single process-file-regexp to avoid processing lots of urgent messages. (3h) C da: goal-hyp: this should be more generic. At the moment, there are generic variables which are only used in the specific code: proof-shell-goal-regexp and proof-shell-assumption-regexp. This is confusing. I suggest making lego-goal-hyp the default behaviour for proof-goal-hyp-fn a hook function. That will work for Isabelle too. (15 mins) C Process handling output. Handling mixtures of urgent and non-urgent messages: at the moment any non-urgent output *before* an urgent message will not be displayed in the response buffer. Accept this as a feature for now. C proof-goal-command-regexp: the syntax of Coq spoils the uniform use of a regexp to match a goal (since it allows goals to begin Definition ...). Nonetheless, it would be for this not to mean that everyone else needs to set proof-goal-command-p. Perhaps some crucial regexps can be used via proof-string-match-p which would allow a function to be invoked instead? (Cf font lock). C Improve indentation code and see why it's so slow (at least for Isabelle). Enable it for particular provers if it works okay (but must test in on large files). C Regions in script buffer have nice "name" property and configurers have to set regexps carefully so that it works, but is it actually used anywhere? What's it good for? C ROBUSTness: deal gracefully with possibility that goals buffer is killed during session. (2h) D Add support to filter out unwanted noise from the prover by setting up a regular expression proof-shell-noise-regexp (1h) C support for templates e.g., in LEGO it would be nice if, by default, fresh buffers corrsponding to file foo.l would automatically insert "Module foo;" (1h) C Remove "FIXME notes" which are just notes I've put in about old code in case something breaks (da, 10mins). C Check on all FIXME notes. C automise testing procedures in etc/ C Write proof-define-derived-mode which automatically adds a call back hook somehow. Propose this to maintainer of derived.el. (1.5hrs) C Toolbar icon for `proof-execute-minibuffer-cmd' (1.5hrs) C Improve web pages after suggestions in doc/notes.txt (da, 1.5hrs) C proof-issue-goal should refuse to work when a proof is in progress. Similarly proof-issue-save should refuse to work when a proof hasn't been completed! Algorithm: Search the last goal and check length of span. (45min) C Bug in proof-retract-until-point when called twice in succession: calls backward-char at beginning of buffer. (Should say no locked region, or "nothing to retract"). Problems is that there is a proof-locked-end, but it's at (point-min). (30min) C Clean up proof-assert-until-point behaviour. Discussion results: 1. At the moment we get an odd error if it is run in the locked region. This is a bug. Should behave same as proof-assert-next-command in this case (simpler) or give better error message. 2. At or before first character of proof command, "nothing to do" error message. This is a bug. Should behave same as proof-assert-next-command in this case. [1,2 have been "fixed" by rebinding C-c RET to proof-assert-next-command for now, eventually this may form a new version of proof-assert-until-point] 3. Movement and possible insertion of spaces/newlines for when new commands are added to the buffer needs careful thought! (1h) C Improve proof-goal-command and proof-save-command: `proof-goal-command' should be more flexible and support a placeholder for the name and the actual goal. In LEGO, we have Goal foo : absurd; ... Save foo; Perhaps functions at the generic level to make suitable values for the hook, e.g., (setq proof-goal-command (proof-prompt-named-goal "Goal %s :" "%s;")) C Cleanup handling of proof-terminal-string. At the moment some commands need to have the terminal string, some don't. da: I suggest removing proof-terminal-string altogether and adding back the semi-colons or fullstops at the specific level. It's not a big deal and would support other provers which may use a mixture of terminators, or no terminators at all. C Functions for next,previous input a la shell mode, but in proof script buffer (3h, da). C User-level functions: 1. add new version of undo-until-point which behaves analogously to proof-assert-next-command. 2. make version of proof-restart-script which will start or restart the proof assistant as appropriate. (It's handy to have a direct function to start the proof assistant). (1hr, da) C Write test schedule for things to try out with a new instantiation of Proof General. C Add skeleton instantiation files for a dummy prover "myassistant" to make it easier to add support for new assistants -- looking at any of the existing modes is confusing because of the prover-specific stuff. Ideally it should work for one of the default provers as an impoverished example mode. (2h, da will do for Isabelle) C 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) C Reengineer *-count-undos and *-find-and-forget at generic level (3h) C Unify toolbar and menu functions. (1h) C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's. Generic problem, really: maybe CRs should be stripped, and just first line of multiline urgent message displayed in minibuffer. D Perhaps goal..save sequences should be closed also by the appearance of a new goal, even though this may be a "broken" proof. At the moment, undoing past the new goal causes errors: ... .. Will ACS idea handle this? D Better support for adding a new prover: give error messages which hint at what variable to set (see proof-issue-goal for example). D Multiple files: handle failures in reading ancestors. D Provide a sensible default frame/buffer layout (4h) D Implement mouse drag-and-drop support for selecting subterms in the goals buffer and copying them in a script buffer. This could be implemented by defining button2 in the response buffer and setting button2up in script buffers. (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. D proof-find-next-terminator is too slow when it needs to parse a long buffer. Generally a performance problem with proof-segment-up-to. D Implement proof-find-previous-terminator and bind it to C-c C-a (45min) D Implement a function to undo to the previous goal. D Remove duplication of variables e.g., proof-prog-name and lego-prog-name for Coq and Lego. (1h) D Display management is much better than it was, but perhaps not quite as good as it could be. It might be nice to display both the goals and response buffer occasionally (even with window-dedicated disabled). e.g. when proof-shell-erase-response-flag is non-nil and the goals buffer is updated: might like to still see what was in the response buffer. Oddities: Response buffer doesn't get cleared after completion of a proof followed by retraction of whole file. On other cases of retraction, it does. Perhaps retraction should set the flag to ensure it's cleared. D Fixup display of urgent messages in minibuffer: split at newlines so we don't get ^J's in FSF Emacs. D Make wellclean target remove images in html/images which are generated from the image directory. Consider putting all the image sources in images/ X Web pages: - Check appearance in V3 browsers. - Make front page logo be an image map. - Reduce text size and front page image, for 1024x768 screens. - Validate pages. Current failures for HTML 4.0 to do with CGI-style arguments with "&", this is a problem with PHP3 really. - Restructure so that page titles are different to help browsing. (Move links_arr from header.phtml somewhere new, and set $pg_title appropriately before head.phtml is included). - Add pdf documentation as soon as DCS upgrades its ancient TeX installation, or as soon as making release from elsewhere works. Also need to fix inclusion of image in pdf. - Add status bar messages to navigation bar - Get rid of footer() function. - Convert to SSI only plus a meta-generation phase? X Is it possible to let C-c C-c (SIGINT) issue additional process input? Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or rather, to fail gracefully. [ This item reduced to X since Poly/ML is now obsolete. This may still be useful for future proof assistants, though. ] X splash screen: report XEmacs problem of not displaying transparent gif properly. X Consider filtering out special annotations from shell buffer rather than merely making them invisible. X Allow bib-cite style clicking on Load/Import commands to go to file. X w3 manages to do toolbar enablers that work. How? X Images for splash screen: could add xpm files for logos so that XEmacs displays transparent parts properly. (Probably not worth effort of distributing more files). X Customization mechanism: is there a way to make saved settings not be overwritten by setq's in the code? Need to think how to do this, something like customize-set-variable-if-unchanged Otherwise no so useful for people to use customize for prover config settings (we'd need to shadow them all again for each assistant for this to work smoothly). Sure sign saving will fail is when you see "this option has been changed outside customization buffer" At the moment even setting config variables in a hook is tricky, because proof-config-done is called before the hook variables for the new mode are. Our new version of define-derived-mode needs to address this. X Proofs in Isabelle scripts can be non-interactive. Non-interactive proofs have only one command, effectively. It might be useful to find a way to integrate these into Proof General nicely. X 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) X Span convenience functions for special 'type property. Could put these in proof.el or somewhere. (defsubst set-span-type-property (span val) "Set type property of SPAN to VAL" (set-span-property span 'type val)) (defsubst span-type-property (span) "Get type property of SPAN" (span-property span 'type)) etc. (1hr) X Read-only mode of extents sometimes gets in the way: for example, if file changes on disk, can't reload it via usual functions. Can this be improved? Always have to retract first, and that leaves stuff around. X toolbar icons: Automatically generate reduced and pressed/greyed-out versions from gimp xcf files. Keep the xcf files under CVS rather than xpm files. (2h, da) X Remove .gif, .jpg, .xpm, .xbm files from the CVS repository. Add .cvsignore's for them instead. Disadvantage: developers will need to have the Gimp installed to build them via 'make images' (or copy them from the latest download). (da, 1hr) X proof-site (da): I think it would be nice to change the architecture to make customization for new provers much easier. The standard use of 'define-derived-mode' could be invoked automatically in proof-site, and we could easily get away from the kludge of proof-config-done and friends. (Compare this to the way font-lock works automatically for XEmacs when the right variable name is set, but for FSF Emacs you have to write something special). The objection to doing this is based on the idea that we should use an object-like inheritance mechanism to define the new modes. But if this is forgone, it might even be possible to add support for new assistants entirely via the customize mechanism, without any knowledge of elisp apart from regular expressions! X Support a history of proof commands, with a "redo" command to redo undo-to-point or sequences of toolbar undo's. X 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. 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). X Make process handling smarter: because Emacs is single-threaded, no process output can be dealt with when we are running some command. This means that it would be safe to extend the red region, by putting more commands on the queue. Also it would be safe to implement a clever undo command which worked on the red region: if there are commands waiting to be processed, we could remove them from the queue. If there are no commands waiting, we have to wait until something becomes blue to undo it by sending a command to the process. X Ideas for efficiency improvements. Rather than repeatedly re-parsing the buffer, we could parse the whole buffer *once* and make adjustments after edits, like font-lock. We could make an extent for every command, and set it to "blue", "red" or "clear" as appropriate. (This would allow proofs to be sent out-of-order to the proof process too, although perhaps that's not so nice). The function proof-segment-up-to could be made to cache its result. X proof-mark-buffer-atomic marks the buffer as only containing comments if the first ACS is a goal-save span. This is however not a problem for LEGO and Isabelle. (30 min) X Idea for future re-engineering: Indirect Buffers seem to be a cunning way to implement the response buffer and goals buffer, since they're basically variants on displaying fragments of the shell buffer output. Unfortunately seems to be implemented only in FSFmacs at the moment. * Things to do for Proof-by-Pointing ==================================== B Change proof by pointing (pbp) stuff into proofstate buffer stuff. (1h tms) C Fixing up errors caused by pbp-generated commands; currently, script management unwisely assumes that pbp commands cannot fail (2h) B Rename pbp-mode to response-mode or goals-mode (which doesn't support any actual proof-by-pointing) (30min) B Outsource actual pbp/goals functionality (30min tmd) (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. * Things to do for Lego ======================= 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 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) C fix Pbp implementation (10h) 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 Add support for changing directory when scripting buffer changes (see proof-activate-scripting-hook). This would alleviate users from some messing with LEGOPATH. (Possibly contentious). 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. However, there is currently no LEGO command to do this. [4h] * Things to do for Coq ====================== A C-c C-c breaks the coherence with prover state 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) D Add Patrick Loiseleur's commands to search for vernac or ml files. (they are in a separate file that is part of Coq distrib. should I really integrate that in PG ? Patrick) D Proof-by-Pointing (10h) D Add coq-add-tactic with a tactic name, which adds that tactic to the undoable tactics and to the font-lock. (2h) D Improve coqtags. It cannot handle lists e.g., with Parameter x,y:nat it only tags x but not y. [The same problem exists for legotags] * Things to do for Isabelle =========================== A Multiple files needs careful testing. There are cases when retracting asks for files to be removed which were never loaded. This might be harmless, but might be better cleaned up. B auto-adjust Pretty.setmargin when window is resized C derive an isa-response-mode from proof-response-mode; see lego.el (10min) D Implement completion for Isabelle using tables generated by the running process. D Add useful specific commands for Isabelle. Many could be added. Would be better to merge in Isamode's menus. (however, probably a month's work to bring together Isamode and proof.el, making some of Isamode generic) D Switching to other file with C-c C-o could be more savy with file names and extensions (use some standard function?) X 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 Write perl scripts to generate TAGS file for ML and thy files. (6h, I've completely forgotten perl). Does anyone actually want this? X Manage multiple proofs (markers in possibly different buffers) * FSF Emacs issues ================== A bug: FSF Emacs problem (showstopper): highlighting of locked region and queue region seems faulty nowadays for me (da). Only tested on Linux. Going back to 2.0 does not fix problem, on 20.2 or 20.3 C `proof-zap-commas-region' does not work for Emacs 20.2 on lego/example.l . On *initially* fontifying the buffer, commas are not zapped. However, when entering text, commata are zapped correctly. (2h) C proof-shell-dont-show-annotations doesn't seem to work. X possible bug: Thomas had a bizarre .emacs file which causes Seg Faults with Proof General and FSF Emacs. Doesn't happen with "emacs -q". Investigate which package/setting he adds is to blame. * Bugs in other packages beyond our control =========================================== . Odd behaviour of font-lock in elisp buffers when long strings contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)" . oddity: startup delay when running XEmacs remotely and local display is 8 bit. Suspect an XEmacs issue to do with face allocations. Also huge delay in buffers for Isabelle mode which try to highlight binders (removed because they appear inside strings anyway) * New Stable Version Release checklist ====================================== 0. Make all files have same CVS branch with cvs commit -f (only seems to work locally, not via cvs server). Innessential convention. Could increment head number. 1. Test multiple file test suite for LEGO, Isabelle. Coq example. 2. Check case with FSF Emacs 3. Check case with compiled code, for XEmacs only. (Wait for error reports for FSF Emacs) 4. Dates and versions updated in: README, doc/ProofGeneral.texi, html/download.html 5. ProofGeneral.texi docstring magic is up-to-date: cd doc; make magic 6. Update Emacs and prover versions in texi, html/ 7. Check web page references from other places. 8. Validate web pages if they're changed much. * Things to do for Proof General Project ======================================== A Try to get small project grant from LFCS to help with development of Proof General A Find new person to help maintain Coq Proof General A Polish ProofGeneral.texi and publish LaTeX as an LFCS Technical Report. * Fix page rearrangement to insert a blank page * Fix typos/other stuff found by Dave. * Suggestions, typos, contributions by Healf. (Dave has email) * Improve trivial and uniformative docstrings. * Fixup markup mistakes by editing docstrings. * Update menus in texi [6 hours] A Write paper for system demonstration of Proof General for some conference. Write paper on design and development of Proof General.