diff options
| -rw-r--r-- | TODO.defunct | 263 | ||||
| -rw-r--r-- | TODO.developer | 699 | ||||
| -rw-r--r-- | coq/todo | 60 | ||||
| -rw-r--r-- | hol98/todo | 25 | ||||
| -rw-r--r-- | isar/todo | 43 | ||||
| -rw-r--r-- | lego/todo | 44 | ||||
| -rw-r--r-- | plastic/todo | 10 |
7 files changed, 0 insertions, 1144 deletions
diff --git a/TODO.defunct b/TODO.defunct deleted file mode 100644 index 4943e3d8..00000000 --- a/TODO.defunct +++ /dev/null @@ -1,263 +0,0 @@ --*- mode:outline -*- - -* Proof General Defunct List of Things to Do - -This is a list of things that fell out of todo. They'll -probably never be read again, let alone done... - - - -** Things to do in the generic interface - -*** X X-Symbol improvements: see if we can get support for - proof-xsym-extra-modes outside PG (just by loading proof-site). - Will be handy for Isabelle's .itex Isabelle-LaTeX files. - Then we can parameterise more of the xsym support, and - remove spurious settings of calculated stuff from - x-symbol-isa.el (see FIXME comments in v3.1 there). - -*** X X-Symbol improvement: turning it on/off seems to move point. - -*** X Why does dired get loaded when PG loads? (Can we speed - loading by avoiding a particular function?) - -*** X 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. - -*** X Internal improvements for marking up proof assistant output. - We need a better mechanism for allowing "invisible" mark up - of assistant output based on annotations. Present code - allows proof-shell-leave-annotations-in-output=t to work - together with font-lock to do mark up. - Instead we need something more like what enriched-mode does - (although I've just tried it and I foound that copying with - the mouse ignores the text properties, but copying with the - keyboard copies them!). It uses a general library - format.el for reading and writing files in multiple formats. - This is not quite what we want for our purpose, but it might be a - closer approximation than using font-lock-fontify and - deleting the special characters. It would allow sgml-like - markupo in the future, too. - Or maybe w3's code for HTML mark up could be borrowed. - -*** X Idea: introduce a dynamic follow mode which follows - proof-locked-end rather than proof-queue-or-locked-end. - Would be annoying for interactive use though, point would - jump from under fingers (although no typing anyway, hardly - matters). Alternative is dynamic recenter mode to - keep end of locked region in buffer. - -*** X Improve goto button image [suggestion from Markus] - Is it possible to avoid the arrows to touch in the middle, - emphasizing the 'point' a bit more. The arrows look a bit outwards - bent, too. - -*** X Check compilation okay, check on use of eval-and-compile. - -*** X Difference in menubar appearance depending on whether X-Symbol - is loaded before Proof General or not. - -*** X Update logo to include new "???" prover badge - from graphics file elsewhere (da) - -*** X bug: outline mode when proof-strict-read-only is nil ought to - work, but there may be problems. - -*** X CVS repository issues. - Where are obsolete 'fileattr' files generated from/maintained? - Should junk these (which appear to say that tms is watching everything). - -*** X 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? - [da: can't repeat this now, presume it has gone away?] - -*** X Add other image sources to images/ directory. - Add target to html/images to remove images generated from - the image directory. - -*** X splash screen: report XEmacs problem of not displaying transparent - gif properly. - -*** X Allow bib-cite style clicking on Load/Import commands to go - to file. - -*** 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. - -*** X 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. - Wait until it's a problem for somebody. - [Trouble with this is that terminators are used for active - terminator mode, among several other things] - -*** X Functions for next,previous input a la shell mode, but in proof - script buffer (5h, da). - -*** (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. - (1 day's gimp hacking) - -*** X Proof General customization: how should it work? - Presently we have a bunch of variables in proof.el which are - set from a bunch of similarly named variables in <engine>-syntax.el. - Seems a bit daft: why not just have the customization in - one place, and settings hardwired in <engine>-syntax.el. - That way we can see which settings are part of instantiation of - proof.el, and which are part of cusomization for <engine>. - -*** X Moreover, 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 GNU 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! - [see proof-easy-config.el] - -*** X Support a history of proof commands, with a "redo" command to - redo undo-to-point or sequences of toolbar undo's. - -*** X Provers with sophisticated/configurable syntax should tell Emacs - about their syntax somehow, rather than trying to duplicate - specifications inside Emacs. - Maybe some particular ATerm format would help with this? - -*** 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 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(?). [2 days] - -*** X The narrowing issue - Code uses (point-min) and (point-max) everywhere. - Most primitive functions give error if given arguments outside - a restriction. However, most places these are used in PG we really - mean the start or end of the buffer (e.g. when parsing). - The only way to fix this seems to be with messy - (save-restriction (widen) ... sequences. - -*** X Solaris bugs: font locking and button enabling. - - [Markus]: I can only produce this problem on Solaris, where we have - both a mule and non-mule version of xemacs-21.1.8. On my Linux box - at home there is no problem present (using xemacs-21.1.7-mule). - - Note that on the Solaris boxes the problem is already exhibited by - visiting a new/empty thy file: buttons are off and are not enabled - by typing new stuff. - - Moved down the list now, instead we disable button enablers on - Solaris. - -*** X Multiple session architecture (difficult) - - With some major re-engineering, PG could be made to work with multiple - provers at once, and multiple instances of the same prover. - - Ideas: - introduce "session" notion - - have list of current sessions in progress, - values of active scripting buffer and other per-session vars - for each one - - proof shell filter and other functions must automatically - switch context to correct session - - force everybody to use proof-easy-config macro, and set - <prover>-var automatically from <proof>-var there, - to get defaults for new sessions. - - - -** Things to do for Web Pages, Distribution - -*** X Convert to SSI only plus a meta-generation phase? - -*** X Add status bar messages to navigation bar - -*** X Get rid of footer() function. - 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. diff --git a/coq/todo b/coq/todo deleted file mode 100644 index eea4427c..00000000 --- a/coq/todo +++ /dev/null @@ -1,60 +0,0 @@ --*- mode:outline -*- - -* Things to do for Coq - -See also ../todo for generic things to do, priority codes. - -** A Submit some minor patches to coqdev to improve things: - -- no printing of summary proof script, user can see it - -- information output when requiring/undoing requires - -- more robust markup of errors/responses, eager annotations - -- eventually... PGIP - -** B Adjust pretty printer line width automatically as others do - -** D Coq pbp focussing, would be helpful if this part works at least - -** C Auto-compile-vos - Would be nice to ressurect this: interaction between PG - and make system is tricky and tedious. - - -** D Loss of synchronisation with silent mode - Apocryphal story, no test cases. - - -** B Proof-by-Pointing [1 month+] (2002) - da: Yves Bertot told me that his CtCoq proof-by-pointing code - is in the Coq kernel now, so would be useful for PG. - We need a Coq hacker to do this. - Perhaps for new version of Coq. - da: I have old version of code sent to my by Healf. - Pierre: Since the code is to be changed, I suggest that we - wait for V7. - da: V7 is here now... - -** C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? - pierre: Yes, the greatest would be to allow users to easily declare - new tokens/symbols and add new grammar rules (Coq allows this) - including the declared tokens. Indeed when I define the type set, - and its element emptyset, and predicate In, I want to be able to say - that emptyset and In are new tokens and asociate them with the right - symbols. I want to be able of that on the fly (maybe we can use the - 'File Variables' feature of Emacs). Another thing is that we may ask - Coq developers to be unicode compliant or something like that. - - -** 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) - (maybe not if they're orthogonal to PG, but might help users - da) - -** D Add coq-add-tactic with a tactic name, which adds that tactic to the - undoable tactics and to the font-lock. (2h) - Pierre: I fixed this I think, by making a non-undoable regexp - instead. This solves the problem of tactics that have been defined - in another file. - -** 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] diff --git a/hol98/todo b/hol98/todo deleted file mode 100644 index d65df204..00000000 --- a/hol98/todo +++ /dev/null @@ -1,25 +0,0 @@ --*- mode:outline -*- - -* Things to do for HOL - -See also ../todo for generic things to do, priority codes. - -** A Problem with process filtering. - - Process (sometimes?) doesn't recover after interrupt, and no output - is seen. Why? - - Also problem with some input texts: try interactive version of - clScript.sml, inductive defn of CL terms breaks things. - -** B Improve display to strip ugly val it and spurious >'s. - -** B Add special markup to improve robustness - -** B Add support for multiple files - -** B Add support for proof by pointing. - -** B Output highlighting doesn't seem to work properly. - - diff --git a/isar/todo b/isar/todo deleted file mode 100644 index cfb5578e..00000000 --- a/isar/todo +++ /dev/null @@ -1,43 +0,0 @@ --*- mode:outline -*- - -* Things to do for Isabelle/Isar [maintainers' list] - -See also ../todo for generic things to do, priority codes. - -** C Improve handling of multiple files - We should recognize error messages from theory loader, in this form: - - \<^sync>ProofGeneral.inform_file_processed "/home/da/projects/proofgen/cvs/ProofGeneral/etc/isar/multiple/A.thy"; \<^sync>; -### Unknown theory "A" -### Theory loader: undefined theory entry for "A" -### Failed to register theory "A" - - (Although actually this case represents a bug elsewhere: - PG should not ask Isabelle to register some theory it doesn't know) - [Idea: maybe we need a sync-loaded-files possibility] - - NB: Multiple file handling has been repaired compared with PG 3.4, - by adding the setting `proof-cannot-reopen-processed-files'. - -** C Adjust imenu/fume to get sections/chapters usefully in tags - Need to grab a prefix of text from the markup section {* Foo *} - -** C Electric terminator for non-terminator provers would be nice. - -** B Proof nesting depth calculation not right: see debug messages - -** B Isabelle tweaks - -- theorem dependencies on spoils ordinary response buffer output - (dependency info *after* response display loses) - -** B visualise dependencies: sometimes not applicable. - Also, does not work at the moment. - -** C func-menu: - observe proof-syntactic-context (general problem of func-menu setup?); - -** C undo 'use' command: unlock corresponding ML file; - -** C provide template for empty theory (or even just for Scratch.thy); - -** C proper proof-by-pointing support (very hard); diff --git a/lego/todo b/lego/todo deleted file mode 100644 index dc0b1f28..00000000 --- a/lego/todo +++ /dev/null @@ -1,44 +0,0 @@ --*- mode:outline -*- - -* Things to do for LEGO - -See also ../todo for generic things to do, priority codes. - -** C Improve X-Symbol support. - -** D Fix Pbp implementation in LEGO itself (10h) - -** D 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) - -** D 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) - -** D Even with the more flexible region model, with - proof-nested-goals-behaviour=closequick, Proof General doesn't - do quite the right thing. Forget for a definition when inside - a proofstate kills off the whole proofstate. Effectively, - the definition is *global* rather than local to the proofstate, - and could perhaps be lifted to before the goal - (with the lift-global nonsense not so daft after all? Editing - behind the user's back is still objectionable though). - Another alternative fix would be to trigger some retraction action - on seeing the "Abort" regexp, rather than assuming it is the result of - some retraction action. More generally this could be used for error - handling. - -** 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 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] diff --git a/plastic/todo b/plastic/todo deleted file mode 100644 index 5ea74023..00000000 --- a/plastic/todo +++ /dev/null @@ -1,10 +0,0 @@ --*- mode:outline -*- - -* Things to do for Plastic - -See also ../todo for generic things to do, priority codes. - -** Add as part of main distribution when Plastic ready - - Edit Makefile.devel - |