From ee9fbb707100dd2e05132c75dc0f8bee26e666bf Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 1 Dec 2004 22:38:34 +0000 Subject: Renamed file --- BUGS.developer | 18 ++ TODO.defunct | 263 +++++++++++++++++++++ TODO.developer | 709 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ bugs | 18 -- todo | 709 --------------------------------------------------------- todo.defunct | 263 --------------------- 6 files changed, 990 insertions(+), 990 deletions(-) create mode 100644 BUGS.developer create mode 100644 TODO.defunct create mode 100644 TODO.developer delete mode 100644 bugs delete mode 100644 todo delete mode 100644 todo.defunct diff --git a/BUGS.developer b/BUGS.developer new file mode 100644 index 00000000..840bd8da --- /dev/null +++ b/BUGS.developer @@ -0,0 +1,18 @@ +-*- outline -*- + +* Developer's list of bugs. + +These are obscure/minor issues which are known about and +could be investigated fixed as low priority. + +** GNU Emacs oddity via menus + +Toggle scripting in incomplete buffer: Emacs hangs after +clicking on "yes". + + + + + + + diff --git a/TODO.defunct b/TODO.defunct new file mode 100644 index 00000000..4943e3d8 --- /dev/null +++ b/TODO.defunct @@ -0,0 +1,263 @@ +-*- 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 -syntax.el. + Seems a bit daft: why not just have the customization in + one place, and settings hardwired in -syntax.el. + That way we can see which settings are part of instantiation of + proof.el, and which are part of cusomization for . + +*** 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 + -var automatically from -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 new file mode 100644 index 00000000..ced35e65 --- /dev/null +++ b/TODO.developer @@ -0,0 +1,709 @@ +-*- mode:outline -*- +$Id$ + +This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. + +================================================================= + +3.6 TODOs +========= + +* 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 + + +================================================================= + +* 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 +10. Things to do for Proof General Project + + See /todo for things to do for each prover. + +** 1. Priorities + +A (High) e.g. to be fixed ASAP for next pre-release +B e.g. to be fixed before next release +C (Medium) e.g. would be nice to fix before next release; not crucial +D e.g. desirable to fix at some point +X (Low) e.g. probably not worth spending time on + + +** 2. 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. + + + + + + +** 10. Things to do for Proof General Project + + +*** A Journal paper on design and development of Proof General. +*** A Grant proposal for Proof General Kit. +*** A Informatics research reports from latest docs. +*** A Small project grants for summer students +*** A Small project grant from LFCS for summer student + +*** B "Spam-protect" (ho, ho) email addresses on web pages +*** B Fixup HTML on mailing list pages (image address) + +*** B Find new people to help advance and develop Proof General. + Getting more instances is a good way. Also encouraging feedback. + Hear stories of bugs always by word-of-mouth, they don't get + reported often enough by email. +*** A PG student projects +*** B PG auxiliary contributions +*** C PG CDROM: CDROM with PG and other theorem provers. Useful? + diff --git a/bugs b/bugs deleted file mode 100644 index 840bd8da..00000000 --- a/bugs +++ /dev/null @@ -1,18 +0,0 @@ --*- outline -*- - -* Developer's list of bugs. - -These are obscure/minor issues which are known about and -could be investigated fixed as low priority. - -** GNU Emacs oddity via menus - -Toggle scripting in incomplete buffer: Emacs hangs after -clicking on "yes". - - - - - - - diff --git a/todo b/todo deleted file mode 100644 index ced35e65..00000000 --- a/todo +++ /dev/null @@ -1,709 +0,0 @@ --*- mode:outline -*- -$Id$ - -This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. - -================================================================= - -3.6 TODOs -========= - -* 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 - - -================================================================= - -* 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 -10. Things to do for Proof General Project - - See /todo for things to do for each prover. - -** 1. Priorities - -A (High) e.g. to be fixed ASAP for next pre-release -B e.g. to be fixed before next release -C (Medium) e.g. would be nice to fix before next release; not crucial -D e.g. desirable to fix at some point -X (Low) e.g. probably not worth spending time on - - -** 2. 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. - - - - - - -** 10. Things to do for Proof General Project - - -*** A Journal paper on design and development of Proof General. -*** A Grant proposal for Proof General Kit. -*** A Informatics research reports from latest docs. -*** A Small project grants for summer students -*** A Small project grant from LFCS for summer student - -*** B "Spam-protect" (ho, ho) email addresses on web pages -*** B Fixup HTML on mailing list pages (image address) - -*** B Find new people to help advance and develop Proof General. - Getting more instances is a good way. Also encouraging feedback. - Hear stories of bugs always by word-of-mouth, they don't get - reported often enough by email. -*** A PG student projects -*** B PG auxiliary contributions -*** C PG CDROM: CDROM with PG and other theorem provers. Useful? - 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 -syntax.el. - Seems a bit daft: why not just have the customization in - one place, and settings hardwired in -syntax.el. - That way we can see which settings are part of instantiation of - proof.el, and which are part of cusomization for . - -*** 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 - -var automatically from -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. - -- cgit v1.2.3