-*- mode:outline -*- $Id$ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. ================================================================= 3.7 TODOs ========= Things to do for 3.7: -- move real todos onto Trac -- nuisance fix needed for docstring magic because of pruning of spaces from empty lines in all docstrings by Stefan Monnier (argh!) -- merge/fix of patch by Claire Quigley (check status with Larry/Tom/whoever) -- Coq updates check: symbols, linewidth, file handling -- Complete generification of adjust-line-width function (currently separately in lego, isar,plastic) ================================================================= * PGIP support ** Remove need for decorated output around PGIP responses. ** Support simplified (flat, non context-sensitive) completion for idtables ** URL parse: library from w3 is incomplete, also may clash with Emacs version. * X-Symbol ** Unify versions with distributed XEmacs version ** Integrate large demo font * Coq-8 fixup ** Fix display of sub/super scripts in Coq output ** Multiple file handling ** Automatic adjustment of line width * Docstring magic fixups ** Some missing files ** Isabelle classic remove? ================================================================= * Developers' Infeasibly Long Low-Level List of Things to Do ** 0. Contents 1. Priorities 2. Things to do in the generic interface 3. Things to do for the documentation 4. 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 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. Long list of things to do in the generic interface *** B Fix-up show/hide for nested proofs. (Wierdness with cursor jumping as well) *** B 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. *** B proof-nesting-depth: This needs to be fixed up in count undos, find-and-forget. *** C Add MMM for other provers where relevant/useful *** C Further display management improvement (it's a nightmare) Glitches to resolve: -- suggestion to cache window height: could implement this by resize change functions (also doing the pretty-print hack?) which set a symbol property for associated buffer symbol -- longer term improvements: allow window preferences per associated buffer. Either separate frame or merged into switching mode. Very messy to implement. -- Stuck-withs: XEmacs frames always have minibuffer. GNU Emacs frames always have modelines. Other older comments: - 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. - check: does auto-delete-windows work with window-dedicated as it should? (I thought it would switch between 2/3 bufs as appropriate?). - 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 Menu layout Would be good to try to make this uniform between version: PG menu frist, then prover-specific menu. Similarly for Imenu. *** A PGIP SUPPORT (minimal for Isabelle patch): -- settings with categories *** A Oddity: Weirdness with regions turning blue even though they haven't been processed. Noticed with HOL/CCC experimental setups. Send a few regions queueing, no result from interpreter, yet sometimes turns blue. Why??? *** C Allow empty retract action that doesn't produce new prompt (Noticed with HOL4). *** unify format for syntax table entries with imenu (make alist); use config setting for syntax table entries everywhere rather than modify-syntax-entry. *** C Implement optional arg to next/undo which doesn't update display (so user can retain something else on screen) *** X Cleanup display during settings processing. *** C Generic adjusting of pretty-printer line width 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). *** C document and simplify proof-script-span-context-menu-extensions *** C 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. *** B Generalize electric terminator mode for other parsing mechanisms. *** B Add parameter for help function so HOL help works nicely *** C Add output highlighting to minibuffer in proof-shell-message. (Quite tricky to get text properties onto text in minibuffer...) *** B Extensions with semantic tokens Look at the Semantic Navigator package. Implements persistent database of tokens. *** 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? *** 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) *** B proof-shell-restart should clear response buffer (only noticed with proof-tidy-response=nil) *** B TESTING. - Add automatic testing mechanism to test user-level functions PG - Test schedule for things to try with a new instantiation *** 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 ] *** X Fix the doc makefiles to adapt the image flag in PG-adapting.tex properly, for dvi/ps targets *** 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! *** 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. Used e.g. 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. *** 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. *** C Consider supporting imenu instead, or as well as, func-menu. *** 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. *** D Make tags support in lego.el and coq.el a bit more generic. Use customization option proof-tags-support. *** 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). *** D X-Symbol: is there a function to input in the minibuffer using a token language? *** X Investigate possible toolbar refresh problems. Sometimes extra clicks *are* needed. Why? (Gone in recent Emacsen?) *** 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 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 *** 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 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. [1hr] *** 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. *** X 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 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). *** X 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) *** X Add support to filter out unwanted noise from the prover by setting up a regular expression proof-shell-noise-regexp [2hr] (any useful examples of noise?) *** 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. [6hr] *** 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 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] *** X A more flexible way of choosing which instance of PG we want, allowing matches on the buffer before choosing the mode function. ** 3. Things to do for the documentation *** B New screenshots for web page, also would be nice for manual. *** B Documentation: Check new doc for hiding; add doc for dependencies, tracing. Moving spans; navigating through locked region. Favourite menu. *** 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: difference between GNU Emacs and XEmacs regexps GNU Emacs gives buggy behaviour with "@lisp" regions. *** B Doc enhancement: explain conditions for switching buffers and auto switching of scripting buffers. (See doc of proof-auto-action-when-switching-scripting) ** 4. Emacs issues *** GNU Emacs issues **** A Improve support for Emacs 21. To do: PBP highlighting (?) **** 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 mouse 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) *** XEmacs issues **** C Ask for easy-menu to support :visible keyword Very useful option of GNU Emacs easy menu to remove items from menu altogether, dynamically. (Or at least, fairly dynamically. Fully dynamically would be guitrocity). [NB: this is there now, perhaps, as :configured] *** A Undo in "read-only" regions *** A Support for nested comments ** 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. *** 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 Error with pdftexinfo (still there?) Gives problem with @value{blah} inside @pdfurl. May be absent from pdftexinfo.tex, but that version doesn't seem to generate web links? ** 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 for compiler warnings running "make", on XEmacs & Emacs *** 3. Test cases using compiled code on Emacs and XEmacs. *** 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.