diff options
| -rw-r--r-- | CHANGES | 26 | ||||
| -rw-r--r-- | TODO | 4 | ||||
| -rw-r--r-- | coq/todo | 5 | ||||
| -rw-r--r-- | hol98/todo | 9 | ||||
| -rw-r--r-- | todo | 65 |
5 files changed, 81 insertions, 28 deletions
@@ -13,7 +13,7 @@ (Nevertheless, please report problems as usual to proofgen@dcs.ed.ac.uk) See README in the hol98 directory for more details. -*** Plastic (http://www.dur.ac.uk/CARG/plastic.html) +*** Plastic (http://www.dur.ac.uk/CARG/plastic.html) (ongoing work) by Paul Callaghan <P.C.Callaghan@durham.ac.uk>. The Plastic system itself is not yet publicly available, @@ -22,6 +22,13 @@ ** Generic Changes +*** Added key binding C-c C-BS and menu entry for delete last command + + This restores the old function of the sequence "C-u C-c C-u" onto + a safer key. In version 3.0 it was only available via + control-button2 in the goals buffer. The function invoked is + `proof-undo-and-delete-last-successful-command'. + *** Separate README and BUGS files for each supported prover Check these files for detail of support and issues with each prover. @@ -34,13 +41,16 @@ *** Fixes for supporting Japanese versions of Emacs which have older CL macs. - Probs with CL macs with Japanicised documentation, defined in "egg.el". + Problems occurred with CL macs with Japanicised documentation, + defined in "egg.el". + Japanese Emacs users, please report any other problems you find, they - may be fixable for similar reasons. + may be fixable for similar reasons. Better still, report these compatibility + problems also to the Japanese Emacs developers, I don't know who to contact. *** Minor bug fix for duplicated short output. - Only seen with "val x=1" or similar messages. + Only seen with "val x=1" or similar very short messages. We now set proof-shell-eager-annotation-start-length appropriately. *** Bug fix with .thy files and X-Symbol mode @@ -73,12 +83,18 @@ This is added particularly for Isabelle running with Poly/ML, which requires interaction after an interrupt. -*** Minor cosmetic improvements +*** Minor cosmetic improvement Name of proof assistant "Start Isabelle" etc. in menu. ** Coq Changes +*** Incomplete handling of Section + + Coq PG will now issue Reset commands for sections. This still + doesn't mirror the undo behaviour of sections properly, which + should be treated as atomic, but it means that you can retract + a file with sections in, at least. ** LEGO Changes @@ -22,6 +22,10 @@ Plans for upcoming 3.x versions * Support more proof assistants +* New key bindings for prover specific commands. + This will unfortunately result in changing some bindings, but make + room for more and avoid the user-reserved sequences C-c <letter>. + * A more flexible way of choosing which instance of PG we want, allowing matches on the buffer before choosing the mode function. @@ -42,6 +42,11 @@ See also ../todo for generic things to do, priority codes. implementation so that it can also deal with sections. [See also the LEGO problem with Discharge] (6h) +** C Correct the C-c C-c bug (typing C-c C-c during the execution of a + tactic breaks the consitency with Coq) + +** C Fix the coq-lift-global code + ** 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) @@ -4,8 +4,13 @@ See also ../todo for generic things to do, priority codes. -** A Problem with displaying long help message: causes loop in PG - filtering, why? Process also takes a long time to kill off. +** A Problem with process filtering. + + Process (sometimes?) doesn't recover after interrupt, and no output + is seen. Why? + + Also problem with some input texts: try interactive version of + clScript.sml, inductive defn of CL terms breaks things. ** B Improve display to strip ugly val it and spurious >'s. @@ -33,12 +33,32 @@ X (Low) e.g. probably not worth spending time on - Recognition of ; only at eol (DvO reported bug here, shouldn't happen) - Web page: add notify when updated option - Manual: credits for other bug reporters - - Remove pbp.el, unused file. - + - Would be nice to fix spurious output of Coq and HOL from first line + when synchronization is gained. *** Scheduled improvements for 3.2 -**** B Fixup silly mess introduced by Isabelle's over the top +**** A Add a new keymap(s) for proof assistants. + Presently they naugthily bind C-c <letter> which are reserved for + users. As a prelude to introducing more prover-specific commands, + we should change these. New map choices: + + C-c C-a (but blasts command start) + C-c C-p (blasts proof-prf) + C-c C-x already seems to be a prefix? + +**** A Add efficiency improvement by turning on/off prover output. + Patch already tested. + +**** 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. + +**** B 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. + +**** A Fixup silly mess introduced by Isabelle's over the top proof-shell-proof-completed-regexp. We shouldn't match on the whole output, that was the point of start-goals and end-goals. Instead we should treat the proof-completed as a case within @@ -68,16 +88,24 @@ X (Low) e.g. probably not worth spending time on 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. +**** D Remove pbp.el, unused file. + ** 2. Things to in the generic interface +*** 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 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. + 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. *** C Add a new configuration setting for matching proof commands which have no undo effect --- should be treated like comments @@ -302,11 +330,6 @@ C New modules: *** D Check support for proof-guess-command-line, new generic setting added by Patrick. Don't know if anyone can use it, actually. -*** 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; @@ -346,12 +369,6 @@ C New modules: *** X Check compilation okay, check on use of eval-and-compile. -*** X 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. - *** D BUGLETS: - If Proof General is loaded with M-x load-library, it gets set up for *no* proof assistant!! @@ -402,10 +419,6 @@ C New modules: Where are obsolete 'fileattr' files generated from/maintained? Should junk these (which appear to say that tms is watching everything). -*** 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] - *** X Fixup display problems. The window dedicated stuff is a real pain and I've spent ages inserting workarounds. Why do we want it?? @@ -718,6 +731,16 @@ C New modules: output. Unfortunately seems to be implemented only in FSFmacs at the moment. +*** X 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. + But we can sidestep the issue by using prover-silent modes, + now in 3.2. + + + ** 3. FSF Emacs issues |