diff options
Diffstat (limited to 'TODO.developer')
| -rw-r--r-- | TODO.developer | 699 |
1 files changed, 0 insertions, 699 deletions
diff --git a/TODO.developer b/TODO.developer deleted file mode 100644 index a0067a90..00000000 --- a/TODO.developer +++ /dev/null @@ -1,699 +0,0 @@ --*- 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 <prover>/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. |