-*- mode:outline -*- * Proof General Low-level List of Things to Do $Id$ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. ** 0. Contents 1. Priorities 2. Things to do in the generic interface 3. Things to do for the documentation 4. GNU Emacs issues 5. Things to do for Proof-by-Pointing 6. Things to do for Web Pages, Distribution 7. Future improvements to take advantage of newer Emacsen 8. Bugs in other software beyond our control 9. Stable version release checklist 10. Things to do for Proof General Project See /todo for things to do for each prover. ** 1. Priorities A (High) e.g. to be fixed ASAP for next pre-release B e.g. to be fixed before next release C (Medium) e.g. would be nice to fix before next release; not crucial D e.g. desirable to fix at some point X (Low) e.g. probably not worth spending time on ** 2. Things to do in the generic interface *** D Make code robust against accidental buffer kills by regenerating auxiliary buffers automatically. *** D Bugs with extents: Sometimes probs if try to assert a whole file while one is being processed: (proof-set-queue-start end) call in proof-done-advancing finds that queue span is detached. Code is now robust for this. But why detach anyway? *** C Extensions with semantic tokens Look at the Semantic Navigator package. Implements persistent database of tokens. *** B Documentation: Check new doc for hiding; add doc for dependencies, tracing. Moving spans; navigating through locked region. Favourite menu. *** C Fix byte compilation Problem with proof-ass macro mechanism -- gets expanded during compilation. *** B generalize from Isabelle's "atomic scripting" theory file mode to allow other instances which do not allow incremental processing of files in major or auxiliary file types. E.g. twelf, ACL2, LambdaCLAM. Also, add the atomic scripting handling for Isabelle/Isar. *** B Move over to new better designed parsing function mechanism. *** D ChangeLog generation still not right. Probs: duplicated entries when runs several times in same day. Suggested fix: use rcs2log to generate the entire log, just take a sensible number of lines from it. (Ideal would be to get until a given date) *** C Fix the doc makefiles to adapt the image flag in PG-adapting.tex properly, for dvi/ps targets *** B Generalize electric terminator mode for other parsing mechanisms. *** B Add parameter for help function so HOL help works nicely *** D Make tags support in lego.el and coq.el a bit more generic. Use customization option proof-tags-support. *** D Display functions: does auto-delete-windows work with window-dedicated as it should? (I thought it would switch between 2/3 bufs as appropriate?). *** C Clean up assert-until-point stuff: should have just one function, as a subroutine of assert-next-command; and no bizarre never-used arguments! *** B proof-shell-restart should clear response buffer (only noticed with proof-tidy-response=nil) *** D Continue programme of making adaptation easier. *** D Fix up sources to conform to library header conventions see (lispref)Library Headers. *** D Proof shell exit function -- could try sending an interrupt first if the process is busy, just to be polite (and avoid the 10 second wait before it gets killed). *** C make pretty printer line width altering generic. Make a generic hook (or hook-constructing macro) to adjust pretty printer line widths, a la LEGO. Maybe find a better place to do this that in the proof-shell-insert-hook (should be triggered by resize events). *** D X-Symbol: is there a function to input in the minibuffer using a token language? *** D Investigate possible toolbar refresh problems. Sometimes extra clicks *are* needed. Why? *** C Consider supporting imenu instead, or as well as, func-menu. *** C Improved configurability of command settings, etc. We should let command settings, etc, be a special type which can be one of three things: 'string -- send this as a command to assistant 'function -- call this interactively to return either 'string -- send this as a command nil -- do nothing (function does work). This way we cover commands which need prompting for extra args, as well as elisp functions which do whatever's necessary. Then use a generic function "proof-invoke-function" or similar. *** C Usability enhancement: 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? *** C Usability enhancement: - Fix proof-script-command-separator and proof-one-command-per-line flag, document them. *** C Support an extended version of dynamic abbreviations, to work for commands rather than words. Should behave a bit like a history mechanism in shell buffer: use M-n M-p to scroll up and down through previous and forthcoming (matching) commands. *** B TESTING. - Add automatic testing mechanism to test user-level functions PG - Test schedule for things to try with a new instantiation *** D Is there a way to make colours defined for x work in mswindows too? defface specs with (type x) seem to work fine with (type mswindows) too. Hassle to duplicate, is there an easy way to cover both? *** C Improve proof-easy-config mechanism. Let it be redoable by initializing some of the variables to default values to begin with(?). e.g. proof-script-next-entity-regexps. Convention is that everything must be set in proof-easy-config body. Use custom to set everything to its default value from proof-config, before invoking the body. *** B Add a new configuration setting for matching proof commands which have no undo effect --- should be treated like comments for undo. Perhaps would be useful for Isabelle, HOL, at least, although it's tricky to see how it would be completely *safe*. [ See discussion with Pierre re Coq undo command categories ] *** C Implement proof-generic-find-and-forget <...>-count-undos, to simplify prover-specific code. Complete reengineering of *-count-undos and *-find-and-forget at generic level *** D Display buffer clearing: response buffer is cleared too often/eagerly, perhaps? The output find-theorems or similar doesn't last beyond a single proof step. The problem is that we want to erase irrelevant output from the response buffer for the previous proof step. Consider making output from invisible command persistent. See attempted patch in etc/patches/fix-attempt-for-eager-cleaning.txt *** C Add to proof-config those variables created in proof-easy-config for font lock and syntax entries. Use these instead of primitive elisp in the other configs, too. *** C Improvements to customization mechanism: watch the use of customize-set-variable, odd for users who think it means they've changed a setting! (currently: next-entity-regexps, proof-splash-settings for Isabelle). *** C Add improvements to script movement in electric terminator mode. Some commented regions in code. E.g. automatic newline/space after C-c C-BS. *** C Make proof-{script,shell,goals,resp}-font-lock-keywords the default way of setting font-lock-keywords, removing from proof-easy-config and changing each supported prover instance. *** D Settings mechanism could be generalised for non-persistent settings local settings: E.g. Coq has some settings which are local: "Focus" which it doesn't make sense to save between sessions or issue at the start of the session. Ideal would be to specify context when local settings are relevant, as a predicate. *** D Modify response display routine a bit to center around recent output, or display top, for long output. Makes better sense for big screen-fulls, perhaps? Or maybe display top with an itimer to move to the bottom after a couple of seconds delay, would be a nice effect. *** D Scheme to detect type of buffer and choose between possible modes. Help select Isar over Isa, maybe sml over HOL etc? *** D Fix the sentinel infinite loop bug which occurs in some cases when proof shell startup fails. Same message is printed over and over. Infinite in GNU Emacs. Why? See note at end of proof-shell. [2hrs] *** D See if there is a way of postponing func-menu loading. *** D Quit timeout enhancement: instead of killing immediately after timeout, could give a message "not responding, kill immediately?" *** D Consider proof-generic-goal-hyp function, for proof by pointing support. Based on `proof-shell-goal-regexp' which I accidently introduced at one point. *** D Make code robust against accidental deletion of response/goals buffer. Add functions proof-get-or-create-{response,goals}-buffer. [30 mins] *** D proof-script-next-entity-regexps: "However, it does not parse strings, comments, or parentheses." Actually we could improve the generic code to ignore headings which buffer-syntactic-context suggests are inside comments or strings. *** D Change the name of "automatic multiple files" to something more comprehensible. *** D Strange problem when running in tty mode: c-c c-RET seems to be impossible to type. Consider binding C-c RET instead when running on a console. *** D Tidy up library-loading and dependencies. (Probably do this at the same time as organizing for the XEmacs packaging mechanism) *** D Make compile should give error if any elisp compile fails. *** D Check support for proof-guess-command-line, new generic setting added by Patrick. Don't know if anyone can use it, actually. *** D Usability enhancement: - Fix asymmetry between "doing" and "undoing": doing will skip comments, undoing will not. e.g. test case: (* tester *) intros; *** D Robustify and cleanup code by allowing functions in place of regexps for proof-goal-command-regexp and proof-save-command-regexp. New names: proof-goal-command-match, proof-save-command-match. Then we can remove duplicity and simplify code. *** D BUGLETS: - Response buffer doesn't scroll to display o/p (it does for debug msgs, oddly). This might have been a 1998 design decision. Maybe it should be a user option? - XEmacs pg forces on font-lock, should it? *** D SMALL DELTAS: - Consider setting proof-mode-for-script automatically? Is it ever needed in the shell before the script mode has been entered? - In case active terminator leads to an error, delete it again? (problem synchronizing) - Improvements to script navigation commands. Would like some uniformity with proof-find-next-terminator, and a better implementation. Maybe we have four commands: find command start, command end, and move to next command/previous command. *** D 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. *** D outline configuration should be generic (or else documented for each prover separately, since not guaranteed to work for all). *** D 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] *** D Implement proof-auto-retract idea. [4hrs] *** D 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) *** D 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) *** D 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). Or via a new generic mechanism for matching or invoking a fn. *** D 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 [2hr] *** D 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;" Probably by using a generic Emacs package. [2hr] *** D Review and prune "FIXME notes" which are notes about ongoing fixes or sometimes things to do. [6hr] *** D Write proof-define-derived-mode which automatically adds a call back hook somehow corresponding to our "proof-config-done" mess. Propose this to maintainer of derived.el. (1.5hrs) *** D 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;")) *** 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 More flexible help configuration is needed. HOL has some nice on-line help but no way in PG to help by library. Perhaps a help browser is needed? At least, optional arg to help command. [patch ready and waiting to go in] *** X 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. *** X 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. *** X Making undoing better. Rather than calculating an undo command each time an undo command is needed, another idea would be to keep the undo command in the span. Then when we amalgamate spans we can construct new undo commands. When we come to issue an undo, we either need to do each undo step in turn in reverse, just the final one, or perhaps some proof-assistant dependent filtering/modification of the set. At the moment, though, PG is rather keen on issuing just one command to forget to some specific place in the script. [Maybe a design principle is that spans should coincide with undoable regions] ** 3. Things to do for the documentation *** A Doc new bits: proof-next-error *** A Doc new bits: font lock keywords, filename %e, %r. Added proof-{script,shell,goals,resp}-font-lock-keywords. Presently used only in proof-easy-config, will put into other mechanism *** A Doc new bits: win32 support *** A Doc new bits: settings mechanism via defpacustom *** C Update front page image - Should include ??? logo to represent other provers *** B Manual improvements before techreport publishing (see notes at end also): - Mention configuring function menus, outline. - Consider splitting up chapter 9? - document mouse functions, proof-cd, process quit timeout, X-Symbol, prog-name-guess, new menu functions for display. - general tips on what to do when things go wrong: try interrupt, restart, finally exit proof assistant. - improvements after feedback from users. - add screenshots? - add more index entries *** B Add something to better document two-buffer versus three-buffer interaction modes, and the use of proof-window-dedicated to trigger three buffer mode. *** C Documentation in pdf format: need to fix inclusion of image problem. *** D Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. *** D texi-docstring-magic: first time deffn's, etc, are added, whitespace after magic comment is left. *** B Doc enhancement: explain conditions for switching buffers and auto switching of scripting buffers. (See doc of proof-auto-action-when-switching-scripting) ** 4. GNU Emacs issues *** B Improve support for Emacs 21. X-symbol fixup in other provers. *** B Consider replacing buffer-substring -> buffer-substring-no-properties Text properties are passed around in spans, probably needlessly. (not the same in XEmacs?) *** C Changed implementation of overlays inside Emacs itself. We seem to need 'priority property of overlays for queue and locked to make sure the colours show through. Even then highlighting is strange, and background face spoils the others. Transparent? Same priority: we get mouse highlighting but no face property. Higher priority: we get blanking as mouse highlighting. Yuk. ACTION: check Emacs Lispref for hints. Maybe ask on newsgroup. *** X `proof-zap-commas-region' does not work for Emacs 20.4 on lego/example.l . On *initially* fontifying the buffer, commas are not zapped. However, when entering text (on a particular line), commata are zapped correctly. (4h) ** 5. Things to do for subterm markup / proof-by-pointing *** B Unify proof-insert-pbp-command and proof-shell-insert-loopback-cmd. Add some debugging messages in proof-done-advancing to indicate Maybe pbp should be a new class of "'pbpadvancing" since we don't want to allow the flexible queue manipulation here? Think on it. *** B Change proof by pointing (pbp) stuff into proofstate buffer stuff. Outsource actual pbp/goals functionality (separate pbp annotations from other annotations). Rename pbp-mode to response-mode or goals-mode (which doesn't support any actual proof-by-pointing), Make a file proof-goals.el. [4 hrs] *** C Extend balloon-help (e.g. show pbp command) *** C Fixing up errors caused by pbp-generated commands; currently, script management unwisely assumes that pbp commands cannot fail. da: Is this still true? It looks fine to me. I think "failure" should mean generates an error. With LEGO pbp, it uses "Try" tactic which always succeeds, whether or not something gets done. *** C In case of pbp failure (real failure), we might keep a flag to indicate that the next pbp command should delete the previous pbp command's insertion into the buffer, to replace it with another one. *** 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. ** 6. Things to do for Web Pages, Distribution *** C simplify editing of web pages by instead including files with version numbers in them, at least for development version. Can also use the link "-latest". *** C Remove fileshow urls in html *** D Add an animation, showing proof replay. *** C Wanted for links: something to UITP. Are there any pages? *** C Validate pages. Current failures for HTML 4.0 to do with CGI-style arguments with "&", this is a problem with PHP3 really. *** X Restructure so that page titles are different to help browsing. (Move links_arr from header.html somewhere new, and set $pg_title appropriately before head.html is included). *** X Add some one-stop-shop pages. Ask permission to redistribute packages for PAs. Maybe do Windows and Linux versions. ** 7. Future improvements to take advantage of newer Emacsen *** X XEmacs 21.2 compatibility/improvements **** Accelerators for PG menus? (how to customize?) **** Use one-shot-hook for splash display *** X GNU and XEmacs improvements **** Indirect Buffers Maybe a cunning way to implement the response buffer and goals buffer, since they're basically variants on displaying fragments of the shell buffer output. Appears in XEmacs 21.2, GNU 20.5 ** 8. Bugs in other software beyond our control *** A Nasty bug in Emacs 21.{1,2} triggered by proof-shell-dont-show-annotations. Report this. *** X Code for find-alternate-file has annoying habit of nullifying buffer-file-name before kill functions are called, on a buffer named ** lose **. This means PG has to keep a copy of the buffer file name to handle proof-included-files-list nicely. Would be better if (X)Emacs code didn't do this. *** X useful if call-process would keep last error state (primarily for exec-to-string, in case of errors) *** X Odd behaviour of font-lock in script buffers when long strings contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)" *** X 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) *** X spurious byte comp warning in XEmacs 21.1.4: While compiling proof-x-symbol-encode-shell-input: ** buffer-substring called with 3 args, but requires 0-3 for this code: (prog1 (buffer-substring) (kill-buffer (current-buffer)) *** X Error with pdftexinfo (hacked version of teTeX pre-release, 1.0.6). Gives problem with @value{blah} inside @pdfurl. May be absent from pdftexinfo.tex, but that version doesn't seem to generate web links? *** (/usr/share/texmf.local/pdftex/texinfo/pdftexinfo.tex Loading texinfo [version 1999-09-25.10]: Basics, pdf, (/usr/share/texmf/pdftex/plain/misc/pdfcolor.tex) fonts, page headings, tables, conditionals, indexing, sectioning, toc, environments, defuns, macros, cross references, (/usr/share/texmf/tex/plain/dvips/epsf.tex) localization, and turning on texinfo input format.)) (ProofGeneral.aux) [1[/usr/share/texmf/d vips/config/pdftex.map][/usr/share/texmf.local/dvips/config/dalucida.map][/usr/ share/texmf.local/dvips/adobe/agaramon/pad.map][/usr/share/texmf.local/dvips/co nfig/wp1.map][/usr/share/texmf.local/dvips/config/mscore.map][/usr/share/texmf. local/dvips/config/barbedor-ttf.map][/usr/share/texmf.local/dvips/config/goodtt .map]] [2] (Preface) ! Undefined control sequence. @indexbreaks ->@catcode `@-=@active @let - @realdash @value ...ode `@-=12 @catcode `@_=12 @indexbreaks @let _@normalunderscore @v... @value {URLpghome} @pdfurl ...r{/Subtype /Link /A << /S /URI /URI (#1 ) >>}@endgroup @douref ...->@begingroup @unsepspaces @pdfurl {#1} @setbox 0 = @hbox {@ignore... l.264 @uref{@value{URLpghome}} . Visit this page for ? x <8r.enc> Output written on ProofGeneral.pdf (2 pages, 54702 bytes). ** 9. New Stable Version Release checklist *** 0. Make all files have same CVS branch with cvs commit -f *** 1. Tests: multiple file test suites for LEGO, Isabelle; other egs *** 2. Check case with GNU Emacs *** 3. Check case with compiled code, for XEmacs only. (Wait for error reports for GNU Emacs) Even if the code is faulty afterwards, compiling is worthwhile just because it shows up bugs in unbound variables, etc. *** 4. Dates and versions updated. Check README, doc/ProofGeneral.texi, html/download.html, others. *** 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. *** 9. Update and distribute etc/announce. *** 10. Message to PG mailing list. ** 10. Things to do for Proof General Project *** A Journal paper on design and development of Proof General. *** A Grant proposal for Proof General Kit. *** A Make informatics research reports from latest docs. *** A Small project grant from LFCS for summer student (2003) *** C PG CDROM: CDROM with PG and other theorem provers Complete read-to-go distributions. Could make up from TYPES summer school systems to make sure of a consistent set of progs? *** B Find new people to help advance and develop Proof General. Getting more instances is a good way. Also encouraging feedback. Hear stories of bugs by word-of-mouth, they don't get reported often enough. *** A Add more PG projects, publicise them. *** B PG auxiliary contributions - span library *** A PG research directions: - protocols for interactive proof - configuration management / dependency organization - ideas about proof engineering cf software engineering - research on ways of conducting a formalization, cf ways of writing a program. Common idioms that PG could help with. ================================================================= LIST OF THINGS FOR PG 3.4 ========================= ** LATEST -- Coq pbp focussing --- does this part work at least? Test case. -- Pierre's changes -- Christophe's changes -- Win32 prob noted by N.V. ** X-SYMBOL PROBLEMS -- GNU emacs probs with Coq and friends. -- Isabelle probs (electric token, latin1, sub/sup). ** Check all instantiations. ** Nested idiom spans: - check nested 'idiom spans are removed in all cases. (Maybe they should have type annotation after all?) ** GNU Emacs probs: Another miscellaneous hang: on "Exit Isabelle" after doing retraction because of part-way through processing a file. ** Announce mailing list move, new test version. ** Does proof-follow-mode have any effect??? ** Add glyphs for hidden proofs. ** Fix-up show/hide for nested proofs. (Wierdness with cursor jumping as well) ** Show/hide in FSF Emacs. ** Context menu for FSF Emacs. ** Cleanup undo behaviour to cope with new Coq mechanism. Is the simplified mechanism better for other provers too, or does the split still apply? Probably best to leave Isar as-is and have proof-nesting-depth left as experimental. (Branch?) ** Cleanup Coq undo: discussion with Pierre clarified. Docs, variable names need improvement. ** proof-shell-proof-completed Doesn't behave right for Isabelle/Isar?? ** proof-nesting-depth: This needs to be fixed up in count undos, find-and-forget. ** Would be good to make count undos and find-and-forget generic. [ Perhaps too tricky/temperamental to get this right ]