-*- mode:outline -*- Proof General Low-level List of Things to Do ============================================ $Id$ * Contents ========== * Priorities * Things to do in the generic interface * Things to do for Proof-by-Pointing * Things to do for Lego * Things to do for Coq * Things to do for Isabelle * FSF Emacs issues * Bugs in other packages beyond our control * Stable version release checklist * Things to do for Proof General Project * Priorities ============ A (URGENT) to be fixed immediately for next pre-release B to be fixed before next release C would be nice to fix before next release; but not crucial D (Medium) desirable to fix at some point X (Low) probably not worth spending time on * Things to in the generic interface ==================================== A Pending work, in progress [da]: - reorganization and improvement of menus, keybindings . use toolbar functions, but remove from proof-toolbar and reorganize. . update documentation - test support for x-symbol - document proof-mouse-track-insert (new name for proof-send-span, re-enabled), proof-toggle-scripting, new configuration options. proof-cd - more 3.0 issues: extending the queue region, being more lax about proof-shell-busy. - Fix sentinel infinite loop bug - noticeable delay when loading ML files for Isabelle (fontification?) A Isabelle (and perhaps other prover) multiple file problem: add configuration setting proof-shell-inform-file-processed-command, and send *retract* action when reactivating scripting in a previously full buffer, but don't actually unlock there. A Nested error problem: conceptually, activate scripting should fail if the hook function which causes loading of more files (for isabelle) fails. Maybe fix by adding a new piece of state: "proof-shell-error-flagged". D Usability for Isabelle QED message. Why does the 'no subgoals' proofstate+message appear in the response buffer? I'd say it should appear at least in the goals buffer, as this is the place where I expect the proofstate, and if it disappears, I always get the impression that something has gone wrong. I don't mind if it appears in the response buffer additionally. I think the conceptual argument is that it isn't any more a list of goals, so any special stuff (proof by pointing) is not applicable. The other assistants just say something trivial like "QED!" which is more justifiably a response. D Investigate possible toolbar refresh problems. Are extra clicks ever needed? Wait for some comments. D Improve efficiency for processing for large proofs. Currently worse case is about 75%/25% CPU to Prover/XEmacs when processing long output stretches on zermelo. (Example: time_use_thy in src/HOL/Real/ROOT.ML) Processing large scripts is likely to be worse, and needs work. B After interrupt, queue region is left intact. Seems odd. Let's remove it. Also interrupt needs other cleanups: position of proof-marker may be wrong. Even the message appears in the goals buffer rather than the response buffer! B bug: interrupting Isabelle process sometimes doesn't return, why? (see first half of interrupt error only: *** Interrupt. *** At command "time_use". uncaught exception ERROR raised at: library.ML:1100.35-1100.40 But not "uncaught exception" part. What is worse: prompt disappears! But process still seems to be there underneath. Not sure where this bug comes from. Moreover, killing process then hangs Emacs with message "cleaning up", and get error (1) (error/warning) Error in process sentinel: (no-catch exited t) To see if this is some SML/NJ or Isabelle weirdness, test in xterm: use "ROOT.ML", interrrupt, use "ROOT.ML" again. sig 11! (flaky hardware?) /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2ad09c43 Not reliably repeatable, but: ProofGeneral.isa_restart(); /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b C Add new test cases for closure of unfinished proofs in Lego, Isabelle. 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? Also: movement when queue region is active is odd. E.g.: press C-c C-n twice on lego/example.l. Point hops backwards! C Usability enhancement: Rationalize next and undo. Make same as toolbar commands and have different commands for power users to assert/retract until point. At the moment this is done by binding to the toolbar commands, we need to remove these from proof-toolbar now. C Usability enhancement: Have toolbar button/command to goto a point. Proof General itself should work out whether it's a retraction or advancement! C Unify toolbar and menu functions. (1h) B Web pages: improve screenshots section to include a slideshow, or at least, a series of pictures of PG in action. (3 hours) C Nicety enhancement: Add messages "retracting buffer ... done" "processing ... done". This needs some call backs or setting of variables examined by proof-done-{advancing,retracting} C Fix colouring of response buffer, may be broken. The idea was that the latest message would always be highlighted, I think. C Usability enhancement: remove stupid "I don't know what I should be doing" errors and replace with something more informative. C Doc enhancement: explain conditions for switching buffers and auto switching of scripting buffers. (See doc of proof-auto-action-when-switching-scripting) C Usability enhancement: - Fix proof-script-command-separator and proof-one-command-per-line flag, document them. C Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting ELISP_DIRS somehow. B Improve relocatability of RPM package, and produce package for XEmacs which installs directly under ~/.xemacs/packages. C Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. C Check compilation okay, check on use of eval-and-compile. C Support for proof-guess-command-line, new generic setting added by Patrick. D Update logo to include new "???" prover badge (maybe it should be "...") from graphics file elsewhere (da) D Add etc/announce to web pages somewhere. D Key binding and interface issues - Consider change for prefix argument for C-c C-u and C-c u, it's quite easy to accidently delete by pressing C-c C-u repeatedly. D Usability enhancement: - Fix asymmetry between "doing" and "undoing": doing will skip comments, undoing will not. e.g. test case: (* tester *) intros; D Robustify and cleanup code by allowing functions in place of regexps for proof-goal-command-regexp and proof-save-command-regexp. New names: proof-goal-command-match, proof-save-command-match. Then we can remove duplicity and simplify code. D 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 and hiding the special characters. Maybe using x-symbol would give another approximation, too, although I'm put off that because it's not so standardly a part of XEmacs yet. Or maybe w3's code for HTML mark up could be borrowed. X Multiple file improvements: add automatic/implict handling of multiple files, by retracting across file boundaries automatically if there is no support from the proof assistant to do this. Idea is that when we retract file B and loaded files list is A B C D E, then C D E are retracted too (one by one). Retraction should happen (before) first undo takes place in a buffer on the loaded files list. Type theory proof assistants with a linear context can be handled perfectly this way. X Usability enhancement: Enable toolbar in other PG buffers. Should switch to active scripting buffer first if it is non current. In fact, a sensible subset of scripting commands would work from other buffers. This suggestion is based on observation of a user's confusion when the toolbar disappears from other PG buffers. X Compatibility enhancement: - Consider sending comments to proof process after all. They might contain special (e.g. LaTeX) directives or something. Probably only worth considering if/when it becomes a problem. X bug: outline mode when proof-strict-read-only is nil ought to work, but there may be problems. X bug: mentioned by Martin H. with Lego: "don't know what I should be doing..." error when it shouldn't happen. [this item is useless without a more detailed description] X CVS repository issues. Where are obsolete 'fileattr' files generated from/maintained? Should junk these (which appear to say that tms is watching everything). B QUESTION: why do we have proof-shell-proof-completed-regexp's perhaps objectionable behaviour of forcing the response buffer? Would it be safe just to set the proof-shell-proof-completed flag and output as usual? (The effect would be to allow Isabelle's completed proof message to appear in the goals buffer since it's marked up as a proof state output) C proof-shell-exit has a time delay of 10 secs built-in, before which the process is killed off. This should be configurable to allow for proof assistants which really want to do some work before exiting, for example writing persistent databases out or the like. Also this fact should be documented. C 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(?). [4 hours] B 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? B 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. B outline configuration should be generic (or else documented for each prover separately, since not guaranteed to work for all). B Improve behaviour when switching active scripting buffer. Now kill buffer function retracts partially-processed files and removes them from proof-included-files-list, we could allow switching between scripting buffers automatically, (perhaps with an option akin to the old "steal scripting?" idea). B Check matching code carefully, in view of bug reported (now fixed) for Isabelle. Examine syntax tables for all instances, and whether word matching is based on whitespace constituents or non-word constituents. [6 hrs] C Reorganize menus in a better way. Have generic scripting commands for keyboard or menu/toolbar use. (2hrs) C Implement proof-auto-retract idea. (4hrs) C Make and test generic versions of <..>-goal-command-p, <...>-count-undos, to simplify prover-specific code. C Improve handling of process exiting early (see note at end of proof-shell-mode). (30mins) C 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) C 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) C 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. C 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). C Improve indentation code and see why it's so slow (at least for Isabelle). Enable it for particular provers if it works okay (but must test in on large files). C Proofs in script buffer have nice "name" property and configurers have to set regexps carefully so that it works, but is it actually used anywhere? What's it good for? C ROBUSTness: deal gracefully with possibility that goals buffer is killed during session. (2h) D Add support to filter out unwanted noise from the prover by setting up a regular expression proof-shell-noise-regexp (1h) C 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;" (1h) D Review "FIXME notes" which are notes about ongoing fixes or sometimes things to do. D automise testing procedures in etc/ C 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) C Toolbar icon for `proof-execute-minibuffer-cmd' (1.5hrs) C Clean up proof-assert-until-point behaviour. Discussion results: 1. At the moment we get an odd error if it is run in the locked region. This is a bug. Should behave same as proof-assert-next-command in this case (simpler) or give better error message. 2. At or before first character of proof command, "nothing to do" error message. This is a bug. Should behave same as proof-assert-next-command in this case. [1,2 have been "fixed" by rebinding C-c RET to proof-assert-next-command for now, eventually this may form a new version of proof-assert-until-point] 3. Movement and possible insertion of spaces/newlines for when new commands are added to the buffer needs careful thought! (1h) C 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;")) 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. [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). X Write test schedule for things to try out with a new instantiation of Proof General. X Add skeleton instantiation files for a dummy prover "myassistant" to make it easier to add support for new assistants -- looking at any of the existing modes is confusing because of the prover-specific stuff. Ideally it should work for one of the default provers as an impoverished example mode. C Reengineer *-count-undos and *-find-and-forget at generic level (3h) C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's. Generic problem, really: maybe CRs should be stripped, and just first line of multiline urgent message displayed in minibuffer. D Perhaps goal..save sequences should be closed also by the appearance of a new goal, even though this may be a "broken" proof. At the moment, undoing past the new goal causes errors: ... .. Will ACS idea handle this? 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 Display management is much better than it was, but perhaps not quite as good as it could be. It might be nice to display both the goals and response buffer occasionally (even with window-dedicated disabled). e.g. when proof-shell-erase-response-flag is non-nil and the goals buffer is updated: might like to still see what was in the response buffer. 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. D Fixup display of urgent messages in minibuffer: split at newlines so we don't get ^J's in FSF Emacs. D Make wellclean target remove images in html/images which are generated from the image directory. Consider putting all the image sources in images/ X Web pages: - Check appearance in V3 browsers. - Make front page logo be an image map. - Reduce text size and front page image, for 1024x768 screens. - Validate pages. Current failures for HTML 4.0 to do with CGI-style arguments with "&", this is a problem with PHP3 really. - Restructure so that page titles are different to help browsing. (Move links_arr from header.phtml somewhere new, and set $pg_title appropriately before head.phtml is included). - Add pdf documentation as soon as DCS upgrades its ancient TeX installation, or as soon as making release from elsewhere works. Also need to fix inclusion of image in pdf. - Add status bar messages to navigation bar - Get rid of footer() function. - Convert to SSI only plus a meta-generation phase? X Is it possible to let C-c C-c (SIGINT) issue additional process input? Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or rather, to fail gracefully. [ This item reduced to X since Poly/ML is now obsolete. This may still be useful for future proof assistants, though. ] X splash screen: report XEmacs problem of not displaying transparent gif properly. X Consider filtering out special annotations from shell buffer rather than merely making them invisible. X Allow bib-cite style clicking on Load/Import commands to go to file. X w3 manages to do toolbar enablers that work. How? 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. (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. Keep the xcf files under CVS rather than xpm files. (2h, da) X Remove .gif, .jpg, .xpm, .xbm files from the CVS repository. Add .cvsignore's for them instead. Disadvantage: developers will need to have the Gimp installed to build them via 'make images' (or copy them from the latest download). (da, 1hr) X proof-site (da): 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 FSF 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! X Support a history of proof commands, with a "redo" command to redo undo-to-point or sequences of toolbar undo's. 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. 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 Idea for future re-engineering: Indirect Buffers seem to be a cunning way to implement the response buffer and goals buffer, since they're basically variants on displaying fragments of the shell buffer output. Unfortunately seems to be implemented only in FSFmacs at the moment. * Things to do for Proof-by-Pointing ==================================== B Change proof by pointing (pbp) stuff into proofstate buffer stuff. (1h tms) C Fixing up errors caused by pbp-generated commands; currently, script management unwisely assumes that pbp commands cannot fail (2h) B Rename pbp-mode to response-mode or goals-mode (which doesn't support any actual proof-by-pointing) (30min) B Outsource actual pbp/goals functionality (30min tmd) (separate pbp annotations from other annotations). Make a file proof-goals.el. 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. * Things to do for Lego ======================= C 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) C 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) C fix Pbp implementation (10h) 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 Add support for changing directory when scripting buffer changes (see proof-activate-scripting-hook). This would alleviate users from some messing with LEGOPATH. (Possibly contentious). 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] * Things to do for Coq ====================== A C-c C-c breaks the coherence with prover state C Retraction in a Section should retract to the beginning of the whole section. See the section "Granularity of Atomic Commands" for a proposal on how to generalise the current implementation so that it can also deal with sections. [See also the LEGO problem with Discharge] (6h) 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) D Proof-by-Pointing (10h) D Add coq-add-tactic with a tactic name, which adds that tactic to the undoable tactics and to the font-lock. (2h) 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] * Things to do for Isabelle =========================== B auto-adjust Pretty.setmargin when window is resized C Unify display of proof output for final level "No subgoals" case with other levels (i.e. remove spurious newlines). NB: spurious newlines may be liked by other provers. C derive an isa-response-mode from proof-response-mode; see lego.el (10min) D Implement completion for Isabelle using tables generated by the running process. Would be a nice addition. (4 hours) D Add useful specific commands for Isabelle. Many could be added. Would be better to merge in Isamode's menus. (however, probably two week's work to bring together Isamode and proof.el, making some of Isamode generic) D Switching to other file with C-c C-o could be more savy with file names and extensions (use some standard function?) X Add ability to choose logic. Maybe not necessary: can use default set in Isabelle settings nowadays, in the premise that most people stick to a particular logic? But then no support for loading user-saved databases. (ponder this) X Write perl scripts to generate TAGS file for ML and thy files. (6h, I've completely forgotten perl). Does anyone actually want this? X Manage multiple proofs, perhaps by automatically inserting push_proof() and pop_proof() commands into the proof script. But would lead to unholy mess for script management! * FSF Emacs issues ================== A bug: FSF Emacs problem (showstopper): highlighting of locked region and queue region seems faulty nowadays for me (da). Only tested on Linux. Going back to 2.0 does not fix problem, on 20.2 or 20.3 C `proof-zap-commas-region' does not work for Emacs 20.2 on lego/example.l . On *initially* fontifying the buffer, commas are not zapped. However, when entering text, commata are zapped correctly. (2h) C proof-shell-dont-show-annotations doesn't seem to work. X possible bug: Thomas had a bizarre .emacs file which causes Seg Faults with Proof General and FSF Emacs. Doesn't happen with "emacs -q". Investigate which package/setting he adds is to blame. * Bugs in other packages beyond our control =========================================== . Odd behaviour of font-lock in script buffers when long strings contain lines with stuff that looks lisp-ish. e.g. "(asd . ads)" . 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) * New Stable Version Release checklist ====================================== 0. Make all files have same CVS branch with cvs commit -f (only seems to work locally, not via cvs server). Innessential convention. Could increment head number. 1. Test multiple file test suite for LEGO, Isabelle. Coq example. 2. Check case with FSF Emacs 3. Check case with compiled code, for XEmacs only. (Wait for error reports for FSF Emacs) 4. Dates and versions updated in: README, doc/ProofGeneral.texi, html/download.html 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. * Things to do for Proof General Project ======================================== A Try to get small project grant from LFCS to help with development of Proof General A Consider writing another grant proposal related to Proof General to generate funding for Proof General. A Find new person to help advance and develop Proof General. A Find new person to help maintain Coq Proof General A Polish ProofGeneral.texi and publish LaTeX as an LFCS Technical Report. * Fix page rearrangement to insert a blank page * Fix typos/other stuff found by Dave. * Suggestions, typos, contributions by Healf. (Dave has email) * Improve trivial and uniformative docstrings. * Fixup markup mistakes by editing docstrings. * Update menus in texi [6 hours] A Write paper for system demonstration of Proof General for some conference. Write paper on design and development of Proof General.