diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 04:21:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-03-13 04:21:14 +0000 |
| commit | 390a659861192ebf98811438f61c4f992ecad25a (patch) | |
| tree | b730ba7312568eaf620b4096a2af21eb953f9f5e | |
| parent | 441b6369abb7863cf65088915cb851ee98f5f59e (diff) | |
New/updated information files
| -rw-r--r-- | BUGS | 310 | ||||
| -rw-r--r-- | CHANGES | 11 | ||||
| -rw-r--r-- | README | 5 | ||||
| -rw-r--r-- | coq/README | 10 | ||||
| -rw-r--r-- | coq/todo | 22 | ||||
| -rw-r--r-- | demoisa/README | 22 | ||||
| -rw-r--r-- | hol98/README | 21 | ||||
| -rw-r--r-- | hol98/todo | 16 | ||||
| -rw-r--r-- | isa/BUGS | 33 | ||||
| -rw-r--r-- | isa/README | 17 | ||||
| -rw-r--r-- | isa/todo | 27 | ||||
| -rw-r--r-- | isar/BUGS | 9 | ||||
| -rw-r--r-- | isar/README | 25 | ||||
| -rw-r--r-- | isar/todo | 7 | ||||
| -rw-r--r-- | lego/BUGS | 53 | ||||
| -rw-r--r-- | lego/README | 10 | ||||
| -rw-r--r-- | lego/todo | 19 | ||||
| -rw-r--r-- | plastic/README | 12 | ||||
| -rw-r--r-- | plastic/todo | 10 | ||||
| -rw-r--r-- | todo | 460 |
20 files changed, 621 insertions, 478 deletions
@@ -1,207 +1,137 @@ -Known Bugs and Workarounds for Proof General. -============================================= +-*- outline -*- -Contact: proofgen@dcs.ed.ac.uk +* Known Bugs and Workarounds for Proof General. + +Contact: mailto:proofgen@dcs.ed.ac.uk See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS +Generic bugs are listed here, which may affect all of the supported +provers. See lego/BUGS coq/BUGS, etc, for specific bug lists for each +of the provers supported. + +* Proof General 3.0 BUGS addendum (fixed in current pre-rel) + +** FSF Emacs: problem with version 20.5 + + PG freezes when starting a proof assistant. + Fixed in the current pre-release. + +** Problems with Japanese versions of FSF Emacs (at least) -Proof General 3.0 BUGS addendum -=============================== + These have older versions of CL macros (defined in file "egg") + with Japanese documentation. + Hopefully fixed in current pre-release, please send in details of + any problems! -* FSF Emacs: problem with version 20.5: PG freezes when starting a -proof assistant. Fixed in the current pre-release. +** You may occasionally see duplications of short (<10 chars) + messages from the proof assistant. This is caused by a too high + setting of the configuration variable + proof-shell-eager-annotation-start-length. + Fixed in current pre-release. -* Problems with Japanese versions of FSF Emacs (at least) which have -older versions of CL macros (defined in file "egg"). Hopefully fixed -in current pre-release, please send in details of any problems! -Generic problems -================ -* If you have problems using Mule versions of FSF Emacs (beware -setting standard-display-european): Pascal Brisset suggests adding -this line to .emacs should help: +* Generic problems + +** If you have problems using Mule versions of FSF Emacs + +Beware setting standard-display-european: Pascal Brisset suggests +adding this line to .emacs should help: (setq process-coding-system-alist '(("" . no-conversion))) -* If the proof assistant goes into a loop displaying lots of -information, it may be difficult or impossible to interrupt it, -because Emacs doesn't get a chance to process the C-c C-c keypress -or "Stop" button push (or anything else). In this situation, you -will need to send an interrupt to the (e.g.) Isabelle process from -another shell. This problem can happen with looping rewrite rules in -the Isabelle simplifier, when tracing rewriting. - -* Highlighting script buffers in recent versions of FSF Emacs is a -mess. The underlying text property implementation has changed -and it seems difficult to get the desired behaviour of highlighting -now. Workaround: switch to using XEmacs. - -* If you use C-x C-v or C-x C-w on a script file which is in active -scripting mode, Proof General will lose track of the file. -Workaround: always turn off active scripting first with C-c C-s. - -* Toolbar enablers for XEmacs 21: since these have been switched on, -it is apparent that the recognition of completed proofs may be -unreliable (it wasn't used before). Also there is a timing issue, -so that occasionally the buttons are disabled/enabled when they -shouldn't be. An extra click on the toolbar solves this. - -* Ordinary undo in the script buffer can edit the "uneditable region" -in XEmacs. This doesn't happen in FSFmacs. Test case: +** If the proof assistant goes into a loop displaying lots of information + +It may be difficult or impossible to interrupt it, because Emacs +doesn't get a chance to process the C-c C-c keypress or "Stop" button +push (or anything else). In this situation, you will need to send an +interrupt to the (e.g.) Isabelle process from another shell. This +problem can happen with looping rewrite rules in the Isabelle +simplifier, when tracing rewriting. + +** Do not use C-x C-v or C-x C-w on a script file in active scripting mode + + Proof General will lose track of the file. + Workaround: always turn off active scripting first with C-c C-s. + +** Toolbar enablers for XEmacs 21, some artefacts. + + There is a timing issue, so that occasionally the buttons are + disabled/enabled when they shouldn't be. An extra click on the + toolbar solves this. + +** Ordinary undo in the script buffer can edit the "uneditable region" + + In XEmacs. This doesn't happen in FSFmacs. Test case: Insert some nonsense text after the locked region. Kill the line. Process to the next command. Press C-x u, nonsense text appears in locked region. -Workaround: take care with undo in XEmacs. - -* In FSFmacs, when proof-strict-read-only is set and font lock -is switched on, spurious "Region read only" errors are given -which break font lock. -Workaround: turn off proof-strict-read-only, font-lock, or for -the best of all possible worlds, switch to XEmacs. - -* As of FSFmacs 20.3, multi-byte character codes are used. This -breaks some of the code in Proof General, which is turned off in -case the suspicious looking function toggle-enable-multibyte-characters -is present. The code that is turned off deals with term markup -for proof by pointing, which only affects LEGO at the moment. -This problem could affect forthcoming versions of XEmacs (but hasn't -as far as XEmacs 21.1). Can anybody tell me if it affects Mule -versions of Emacs? -Workaround: for LEGO pbp, use FSFmacs 20.2, or XEmacs 20.4/later. - -* Using C-g can leave script management in a mess. The code -needs to have some regions protected from Emacs interrupts. -Workaround: Don't type C-g while script management is processing. -If you do, use proof-restart-scripting. - -* Outline-mode does not work in processed proof script files due to -read-only restrictions of the protected region. This is an inherent -problem with outline because it works by modifying the buffer. -Workaround: none, nevermind. (If it's hugely needed we could support -modified outline commands). - -* Multiple file handling for Lego and Isabelle is slightly vulnerable. -Files are not locked when they are being read by the prover, so a long -file could be edited and saved as the prover is processing it, -resulting in a loss of synchronization between Emacs and the proof -assistant. Files ought to be coloured red while they are being -processed, just as single lines are. Workaround: be careful not -to edit a file as it is being read by the proof assistant! - -* XEmacs sometimes has strange start-up delays of several seconds, -possibly due to face allocation, when running remotely and -displaying on an 8-bit display. One workaround (and in fact the -recommended way of working) is to run XEmacs locally and only -the proof assistant on your fast compute server, by setting -proof-rsh-command. - -* When proof-rsh-command is set to "ssh host" and you issue Ctrl-c to -interrupt, the whole process may be killed instead of interrupted. -This isn't a bug in Proof General, but the behaviour of ssh. Try -using rsh instead, it is said to forward signals to the remote command. - -* In tty mode, the binding C-c C-RET has no effect. -Workaround: manually bind C-c RET to 'proof-goto-point instead. - -* You may occasionally see duplications of short (<10 chars) -messages from the proof assistant. This is caused by a too high -setting of the configuration variable -proof-shell-eager-annotation-start-length. -Add (setq proof-shell-eager-annotation-start-length 1) to your .emacs -if it bothers you badly. This fix will be made in the next -pre-release phase, it was too late to make it in time for testing for -release 3.0. - - -LEGO Proof General Bugs -======================= - -* PBP doesn't work on FSF, see note above. - -* [FSF specific] `proof-zap-commas-region' does not work for Emacs - 20.2 on lego/example.l . On *initially* fontifying the buffer, - commas are not zapped [unfontified]. However, when entering text, - commata are zapped correctly. Workaround: don't stare too much at commata - -* If LEGO attempts to write a (object) file in a non-writable - directory, it forgets the protocol mechanism on how to interact with - Proof General and gets stuck. Workaround: Directly enter "Configure - AnnotateOn" in the Proof Shell to recover. - -* After a `Discharge', retraction ought to only be possible back to -the first declaration/definition which is discharged. However, LEGO -Proof General does not know that Discharge has such a non-local -effect. Workaround: retract back to the first -declaration/definition which is discharged. - -* A thorny issue is local definitions in a proof state. LEGO cannot -undo them explicitly. Workaround: retract back to a command before a -definition. - -* Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone -in a proof state by the Proof General. Workaround: retract back to the -start of the proof. - -* After LEGO has issued a `*** QED ***' you may undo steps in the proof -as long as you don't issue a `Save' command or start a new proof. The -LEGO Proof General assumes that all proofs are terminated with a -proper `Save' command. Workaround: Always issue a `Save' command after -completing a proof. If you forget one, you should retract to a point -before the offending proof development. - -*legotags doesn't find all declarations. It cannot handle lists e.g., -with [x,y:nat]; it only tags x but not y. [The same problem exists for -coqtags] Workaround: don't rely too much on the etags mechanism. - - -Coq Proof General Bugs -====================== - -* coqtags doesn't find all declarations. It cannot handle lists e.g., -with "Parameter x,y:nat" it only tags x but not y. [The same problem -exists for legotags] Workaround: don't rely too much on the etags -mechanism. - -* User defined tactics cannot be retracted. Workaround: you may need -to retract to the beginning of the proof. - -* Surely others that aren't mentioned here. Please report them -to proofgen@dcs.ed.ac.uk. - - -Isabelle Proof General Bugs -=========================== - -* set proof_timing is problematic: it will make the goals display -disappear during proof. This is because Proof General only displays -goals output that appears *after* Isabelle messages, but Isabelle -prints the timing message after the goals are displayed. - -* There is a general difficulty with proof scripts containing ML -structures, functions, etc. Proof General does not understand full -ML syntax(!), so it will be confused by structures which contain -semi-colons after declarations, for example. Also, it cannot undo -function declarations. See the section on ML files in the manual -for more details. - -* Blocking when processing multiple files, beginning from a .ML file. -Proof General will block the Emacs process when it is waiting for a -theory file (and it's ancestors) to be read as scripting is turned -on. To avoid this, assert the theory file rather than the ML file. - - -Isabelle and Isabelle/Isar Proof General Bugs -============================================= - -* We've heard from one user that there are problems using -Proof General with Isabelle compiled under MLWorks for Sun -Ultra/Solaris2.7. These may be to do with the piped -communication mechnism; perhaps MLWorks doesn't flush the -output after printing prompts. If anyone discovers this, -a possible work-around is to set process-connection-type to -t instead of nil in proof-shell.el. Please report to -proofgen@dcs.ed.ac.uk if you try this! + Workaround: take care with undo in XEmacs. + +** In FSFmacs, spurious "Region read only" errors + + When proof-strict-read-only is set and font lock is on, these + errors are given which break font lock. + Workaround: turn off proof-strict-read-only, font-lock, or for + the best of all possible worlds, switch to XEmacs. + +** As of FSFmacs 20.3, multi-byte character codes are used. + + This breaks some of the code in Proof General, which is turned off in + case the suspicious looking function + toggle-enable-multibyte-characters is present. The code that is + turned off deals with term markup for proof by pointing, which only + affects LEGO at the moment. This problem could affect forthcoming + versions of XEmacs (but hasn't as far as XEmacs 21.1). Can anybody + tell me if it affects Mule versions of Emacs? Workaround: for LEGO + pbp, use FSFmacs 20.2, or XEmacs 20.4/later. + +** Using C-g can leave script management in a mess. + + The code is not fully protected from Emacs interrupts. + Workaround: Don't type C-g while script management is processing. + If you do, use proof-restart-scripting. + +** Outline-mode does not work in processed proof script files + + Because of read-only restrictions of the protected region. + This is an inherent problem with outline because it works by + modifying the buffer. + Workaround: none, nevermind. (If it's hugely needed we could support + modified outline commands). + +** Multiple file handling for Lego and Isabelle is slightly vulnerable. + + Files are not locked when they are being read by the prover, so a long + file could be edited and saved as the prover is processing it, + resulting in a loss of synchronization between Emacs and the proof + assistant. Files ought to be coloured red while they are being + processed, just as single lines are. Workaround: be careful not + to edit a file as it is being read by the proof assistant! + +** XEmacs sometimes has strange start-up delays of several seconds. + + Possibly due to face allocation, when running remotely and + displaying on an 8-bit display. One workaround (and in fact the + recommended way of working) is to run XEmacs locally and only + the proof assistant on your fast compute server, by setting + proof-rsh-command. + +** When proof-rsh-command is set to "ssh host", C-c C-c broken + + The whole process may be killed instead of interrupted. This isn't a + bug in Proof General, but the behaviour of ssh. Try using rsh + instead, it is said to forward signals to the remote command. + +** In tty mode, the binding C-c C-RET has no effect. + + Workaround: manually bind C-c RET to 'proof-goto-point instead. + + + + + + @@ -10,6 +10,7 @@ by David Aspinall. This is a fairly basic Proof General instance only, hopefully to entice HOL users so that one of them may improve it. I don't plan to maintain or improve this instantiation myself. + (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) @@ -21,14 +22,16 @@ ** Generic Changes +*** Separate README and BUGS files for each supported prover + + Check these files for detail of support and issues with each prover. + *** Names of shell, goals, script buffers now based on proof assistant name Basing the name on the command isn't very abstract and leads to strange names for some provers, "coqtop" and "hol.unquote". Now we just use the lower case of the proof assistant name. -*** README file added for each supported prover, explaining support. - *** Fixes for supporting Japanese versions of Emacs which have older CL macs. Probs with CL macs with Japanicised documentation, defined in "egg.el". @@ -89,12 +92,12 @@ ** Isar Changes -*** Minor syntax tweaks. +*** Syntax tweaks. ** Changes for developers to note -*** todo file added for each prover, split from global todo file +*** todo files added for each prover (todo split from global todo). @@ -16,7 +16,8 @@ See COPYING for license details. See doc/ for documentation of Proof General. -For notes on the supported assistants, see the subdirectories, +For notes on the supported assistants, see the README files +in subdirectories: isa/ Isabelle isar/ Isabelle/Isar @@ -25,6 +26,8 @@ For notes on the supported assistants, see the subdirectories, hol98/ HOL 98 plastic/ Plastic +Check BUGS for problems and issues, in this directory, and +for specific issues, in each prover subdirectory. For the latest news and downloads, check the Proof General web page at: http://www.lfcs.informatics.ed.ac.uk/proofgen @@ -5,12 +5,18 @@ Later contributions by Patrick Loiseleur and Pierre Courtieu. $Id$ +Status: supported +Maintainer: Pierre Courieu +Coq version: 6.3 +Coq homepage: http://pauillac.inria.fr/coq/assis-eng.html + +======================================== + Presently Coq Proof General supports automatic multiple file support only (deduced file dependencies, not communicated ones). It does not have support for proof by pointing. -There is support for x-symbols, but not using a proper token -language. Try writing "philosophy" ! +There is support for X Symbol, but not using a proper token language. There is a tags program, coqtags. @@ -1,36 +1,38 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for Coq -====================== -B C-c C-c breaks the coherence with prover state +See also ../todo for generic things to do, priority codes. + +** B Fix silly startup sychronization problem that displays + cwd on startup. + +** B C-c C-c breaks the coherence with prover state (da: can somebody tell me if this is still true? what problem specifically?) -B Proof-by-Pointing [1 month] +** B Proof-by-Pointing [2 weeks] da: Yves Bertot told me that his CtCoq proof-by-pointing code is in the Coq kernel now, so would be useful for PG. We need a Coq hacker to do this (Pierre?) -C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? +** C Improve X-Symbol support. Integrate with Coq syntax mechanism somehow? -C Retraction in a Section should retract to the beginning of the whole +** 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. +** D Add Patrick Loiseleur's commands to search for vernac or ml files. (they are in a separate file that is part of Coq distrib. should I really integrate that in PG ? Patrick) (maybe not if they're orthogonal to PG, but might help users - da) -D Add coq-add-tactic with a tactic name, which adds that tactic to the +** 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 +** D Improve coqtags. It cannot handle lists e.g., with Parameter x,y:nat it only tags x but not y. [The same problem exists for legotags] diff --git a/demoisa/README b/demoisa/README index fe2b53d4..73770903 100644 --- a/demoisa/README +++ b/demoisa/README @@ -4,16 +4,21 @@ Written by David Aspinall. $Id$ +Status: supported as a demonstration only + +======================================== + + "Isabelle Proof General in 30 setqs" -This is a whittled down version of Isabelle Proof General, supplied -as an (almost) minimal demonstration of how to instantiate Proof -General to a particular proof assistant. You can use this as a -template to get support for a new assistant going. +This is a whittled down version of Isabelle Proof General, supplied as +an (almost) minimal demonstration of how to instantiate Proof General +to a particular proof assistant. You can use this as a template to +get support for a new assistant going. (I did for HOL Proof General). This mode uses the unadulterated terminal interface of Isabelle, to -demonstrate that hacking the proof assistant is not necessary to -get basic features working. +demonstrate that hacking the proof assistant is not necessary to get +basic features working. And it really works! You you get a toolbar, menus, short-cut keys, script management for multiple files, a function menu, ability to @@ -42,6 +47,9 @@ How easy is it to add all that? messages. But automatic multiple files may be all you need anyway. 6. Non trivial (but worth a go). - See demoisa.el and demoisa-easy.el for more details. + + + + diff --git a/hol98/README b/hol98/README index 84e4cc5a..a88902f5 100644 --- a/hol98/README +++ b/hol98/README @@ -4,6 +4,14 @@ Written by David Aspinall. $Id$ +Status: not officially supported yet +Maintainer: volunteer required +HOL version: HOL 98, tested with Taupo 2 +HOL homepage: http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html + +======================================== + + This is a "technology demonstration" of Proof General for HOL 98. It may work with other versions of HOL, but is untested (please let me @@ -12,16 +20,17 @@ know if you try). It has basic script management support, with a little bit of decoration of scripts and output. -There is support for x-symbols, but not using a proper token -language. Try writing "philosophy" ! +There is support for X Symbol, but not using a proper token language. +Try writing "philosophy" ! I have written this in the hope that somebody from the HOL community will adopt it, maintain and improve it, and thus turn it into a proper instantiation of Proof General. ------------------- -Note: +------------ + +Notes: There are some problems at the moment. HOL proof scripts often use batch-oriented single step tactic proofs, but Proof General does not @@ -34,8 +43,8 @@ interactive proofs would also be useful for Isabelle. Another problem is that HOL scripts sometimes use SML structures, which can cause confusion because Proof General does not really parse -SML, it just looks for semicolons. Again, this could be improved by -taking a better parser (e.g. from sml mode). +SML, it just looks for semicolons. This could be improved by taking a +better parser (e.g. from sml mode). These improvements would be worthwhile contributions to Proof General and also provide the HOL community with a nice front end. @@ -1,12 +1,18 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for HOL -====================== -A Problem with displaying long help message: causes loop in PG +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. -B Improve display to strip ugly val it's. +** B Improve display to strip ugly val it and spurious >'s. + +** B Add special markup to improve robustness + +** B Add support for multiple files + +** B Add support for proof by pointing. + diff --git a/isa/BUGS b/isa/BUGS new file mode 100644 index 00000000..0ec5719a --- /dev/null +++ b/isa/BUGS @@ -0,0 +1,33 @@ +-*- mode:outline -*- + +* Isabelle Proof General Bugs + +See also ../BUGS for generic bugs. + + +** "Stack overflow in regexp". + +This problem is caused by a poor regexp and large proofstates. It +needs some small alterations to other proof assistant regexps, so will +be fixed in 3.2. In the meantime, a workaround is to reduce the +number of subgoals displayed. + +** set proof_timing is problematic + +It will make the goals display disappear during proof. This is +because Proof General only displays goals output that appears *after* +Isabelle messages, but Isabelle prints the timing message after the +goals are displayed. + +** General difficulty with proof scripts containing ML structures, etc. + +Proof General does not understand full ML syntax(!), so it will be +confused by structures which contain semi-colons after declarations, +for example. Also, it cannot undo function declarations. See the +section on ML files in the manual for more details. + +** Blocking when processing multiple files, beginning from a .ML file. + +Proof General will block the Emacs process when it is waiting for a +theory file (and it's ancestors) to be read as scripting is turned on. +To avoid this, assert the theory file rather than the ML file. @@ -5,10 +5,25 @@ Markus Wenzel and David von Oheimb. $Id$ +Status: supported +Maintainer: David Aspinall +Isabelle version: 99 +Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ + +======================================== + Isabelle Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and Proof General. It has a mode for editing theory files taken from Isamode. -There is no support for proof by pointing yet. +There is proper support for X Symbol, using the Isabelle print mode +for X Symbol tokens. Many Isabelle theories have X Symbol syntax +already defined and it's easy to add to your own theories. + +There is no support for proof by pointing yet, and no tags program. + +The script `interface' and file 'interface-setup.el' are used to start +Isabelle Proof General via the 'Isabelle' shell command. These files +were provided by Markus Wenzel. @@ -1,15 +1,14 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for Isabelle -=========================== -C Investigate fix for looping rewriting in Isabelle. Continual +See also ../todo for generic things to do, priority codes. + +** C Investigate fix for looping rewriting in Isabelle. Continual and frequent messages from the prover lock out the user. Is there any easy way of fixing this? -C X-Symbol support for theory files: bugs at the moment, because +** C X-Symbol support for theory files: bugs at the moment, because of duplicate calls to proof-x-symbol-mode and mess with font-lock initialization. Problem with current version: visit a.thy, b.thy then turn on xsym. Broken in b.thy. @@ -19,22 +18,22 @@ C X-Symbol support for theory files: bugs at the moment, because [DvO reports okay]. (May need to split extra modes into two parts?) -B auto-adjust Pretty.setmargin when window is resized. Use +** B auto-adjust Pretty.setmargin when window is resized. Use generic code once it's implemented. -D Implement completion for Isabelle using tables generated by +** D Implement completion for Isabelle using tables generated by the running process. Ideally context sensitive. Would be a nice addition. (1 week) -D Add useful specific commands for Isabelle. Many could +** D Add useful specific commands for Isabelle. Many could be added. Would be better to merge in Isamode's menus. (however, probably 2 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 +** D Switching to other file with C-c C-o could be more savy with file names and extensions (use some standard function?) -X weird bug: interrupting Isabelle process (under sml-nj) sometimes +** X weird bug: interrupting Isabelle process (under sml-nj) sometimes doesn't return, why? (see first half of interrupt error only: *** Interrupt. @@ -58,15 +57,15 @@ X weird bug: interrupting Isabelle process (under sml-nj) sometimes ProofGeneral.isa_restart(); /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b -X Add ability to choose logic. Maybe not necessary: can use default +** 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). +** X Write perl scripts to generate TAGS file for ML and thy files. + (6h, any volunteers?). -X Manage multiple proofs, perhaps by automatically inserting +** 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! diff --git a/isar/BUGS b/isar/BUGS new file mode 100644 index 00000000..baddf520 --- /dev/null +++ b/isar/BUGS @@ -0,0 +1,9 @@ +-*- mode:outline -*- + +* Isabelle/Isar Proof General Bugs + +See also ../BUGS for generic bugs. + +Nothing specific here, check isa/BUGS for some issues that may apply +to Isar as well. + diff --git a/isar/README b/isar/README new file mode 100644 index 00000000..f9d0e689 --- /dev/null +++ b/isar/README @@ -0,0 +1,25 @@ +Isabelle/Isar Proof General + +Written by Markus Wenzel + +$Id$ + +Status: supported +Maintainer: Markus Wenzel +Isabelle version: 99 +Isar homepage: http://isabelle.in.tum.de/Isar/ + +======================================== + +Isabelle/Isar Proof General has full support for multiple file +scripting, with dependencies between theories communicated between +Isabelle and Proof General. + +There is proper support for X Symbol, using the Isabelle print mode +for X Symbol tokens. Many Isabelle theories have X Symbol syntax +already defined and it's easy to add to your own theories. + +There is no support for proof by pointing yet, and no tags program. + +The script `interface' and file 'interface-setup.el' are used to start +Isabelle Proof General via the 'Isabelle' shell command. @@ -1,9 +1,8 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for Isabelle/Isar -================================ -C Combine with isa/ to get single Isabelle PG instance, maybe? +See also ../todo for generic things to do, priority codes. + +** C Combine with isa/ to get single Isabelle PG instance, maybe? diff --git a/lego/BUGS b/lego/BUGS new file mode 100644 index 00000000..bfe39752 --- /dev/null +++ b/lego/BUGS @@ -0,0 +1,53 @@ +-*- mode:outline -*- + +* LEGO Proof General Bugs + +See also ../BUGS for generic bugs. + + +** PBP doesn't work on FSF, reason mentioned in generic bugs. + +** [FSF specific] `proof-zap-commas-region' does not work for Emacs + + On lego/example.l . On *initially* fontifying the buffer, + commas are not zapped [unfontified]. However, when entering text, + commata are zapped correctly. Workaround: don't stare too much at commata + +** If LEGO attempts to write a (object) file in a non-writable directory + + It forgets the protocol mechanism on how to interact with + Proof General and gets stuck. Workaround: Directly enter "Configure + AnnotateOn" in the Proof Shell to recover. + +** After a `Discharge', retraction ought to only be possible back + + to the first declaration/definition which is discharged. However, + LEGO Proof General does not know that Discharge has such a non-local + effect. Workaround: retract back to the first declaration/definition + which is discharged. + +** A thorny issue is local definitions in a proof state. + + LEGO cannot undo them explicitly. Workaround: retract back to a + command before a definition. + +** Normalisation commands such as `Dnf', `Hnf' `Normal' cannot be undone + + in a proof state by Proof General. Workaround: retract back to the + start of the proof. + +** After LEGO has issued a `*** QED ***' you may undo steps in the proof + + as long as you don't issue a `Save' command or start a new proof. + LEGO Proof General assumes that all proofs are terminated with a + proper `Save' command. Workaround: Always issue a `Save' command after + completing a proof. If you forget one, you should retract to a point + before the offending proof development. + +** legotags doesn't find all declarations. + + It cannot handle lists e.g., with [x,y:nat]; it only tags x but not y. + [The same problem exists for coqtags] + Workaround: don't rely too much on the etags mechanism. + + diff --git a/lego/README b/lego/README index a8fa6850..2ddd6fd1 100644 --- a/lego/README +++ b/lego/README @@ -5,11 +5,17 @@ Later maintainance by David Aspinall and Paul Callaghan. $Id$ +Status: supported +Maintainer: Paul Callaghan / David Aspinall +LEGO version: 1.3.1 +LEGO homepage: http://www.lfcs.informatics.ed.ac.uk/lego + +======================================== + LEGO Proof General has full support for multiple file scripting, and experimental support for proof by pointing. -There is support for x-symbols, but not using a proper token -language. Try writing "philosophy" ! +There is support for X Symbol, but not using a proper token language. There is a tags program, legotags. @@ -1,27 +1,26 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. +* Things to do for LEGO -* Things to do for Lego -======================= +See also ../todo for generic things to do, priority codes. -C Improve X-Symbol support. +** C Improve X-Symbol support. -D Fix Pbp implementation in LEGO itself (10h) +** D Fix Pbp implementation in LEGO itself (10h) -D In LEGO, apart from Goal...Save pairs, we have +** D In LEGO, apart from Goal...Save pairs, we have declaration...discharge pairs. See the section "Granularity of Atomic Commands" for a proposal on how to generalise the current implementation so that it can also deal with "Discharge". [See also the Coq problem with Sections] (6h) -D Inoking an "Expand" command produces a new proof state. But this is +** D Inoking an "Expand" command produces a new proof state. But this is incorrectly displayed in the response buffer and not the goals buffer because special annotations are missing. Presumably, one ought to replace "Toplevel.Pr()" by "Toplevel.PR()" in the definition of "Expand" (see file newtop.sml [Version 1.4]). (30min) -D Even with the more flexible region model, with +** D Even with the more flexible region model, with proof-nested-goals-behaviour=closequick, Proof General doesn't do quite the right thing. Forget for a definition when inside a proofstate kills off the whole proofstate. Effectively, @@ -34,11 +33,11 @@ D Even with the more flexible region model, with some retraction action. More generally this could be used for error handling. -D Improve legotags. It cannot handle lists e.g., with +** D Improve legotags. It cannot handle lists e.g., with [x,y:nat]; it only tags x but not y. [The same problem exists for coqtags] -X Mechanism to save object file. Specifically, after having processed +** 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. diff --git a/plastic/README b/plastic/README new file mode 100644 index 00000000..b96cd172 --- /dev/null +++ b/plastic/README @@ -0,0 +1,12 @@ +Plastic Proof General + +Written by Paul Callaghan + +$Id$ + +Status: under development together with Plastic +Maintainer: Paul Callaghan +Plastic version: ?? +Plastic homepage: http://www.dur.ac.uk/CARG/plastic.html + +======================================== diff --git a/plastic/todo b/plastic/todo new file mode 100644 index 00000000..5ea74023 --- /dev/null +++ b/plastic/todo @@ -0,0 +1,10 @@ +-*- mode:outline -*- + +* Things to do for Plastic + +See also ../todo for generic things to do, priority codes. + +** Add as part of main distribution when Plastic ready + + Edit Makefile.devel + @@ -1,29 +1,24 @@ -*- mode:outline -*- * Proof General Low-level List of Things to Do -============================================== $Id$ This is an outline file. Use C-c C-n, C-c C-p or menu to navigate. -* Contents -========== +** 0. Contents - * Priorities - * Things to do in the generic interface - * FSF Emacs issues - * Things to do for Proof-by-Pointing - * Bugs in other software beyond our control - * Stable version release checklist - * Things to do for Proof General Project + 1. Priorities + 2. Things to do in the generic interface + 3. FSF Emacs issues + 4. Things to do for Proof-by-Pointing + 5. Bugs in other software beyond our control + 6. Stable version release checklist + 7. Things to do for Proof General Project + 8. See <prover>/todo for things to do for each prover. -See <prover>/todo for things to do for each prover. - - -* Priorities -============ +** 1. Priorities A (High) e.g. to be fixed ASAP for next pre-release B e.g. to be fixed before next release @@ -32,41 +27,64 @@ D e.g. desirable to fix at some point X (Low) e.g. probably not worth spending time on +*** Top Priority Fixes for 3.1 -* Top Priority Fixes for 3.1 -============================ + - Solaris ^G problem and FSF Emacs mule/non-mule support + - 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. -** Isabelle regexp overflow problem on proof-shell-proof-completed-regexp -** Solaris ^G problem and FSF Emacs mule/non-mule support -** Recognition of ; only at eol (DvO reported bug here, shouldn't happen) -** Web page: add notify when updated option +*** Scheduled improvements for 3.2 -* Scheduled improvements for 3.2 -================================ +**** B 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 + start-goals and end-goals, as well as outside it for other + provers. Then automatically display will be in right place. + Shouldn't need proof-goals-display-qed-message any more. + This change not yet in 3.1 because it risks changing behaviour + of other provers. -B Scheme to detect type of buffer and choose between possible modes. +**** B 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. + +**** B Scheme to detect type of buffer and choose between possible modes. Help select Isar over Isa, maybe sml over HOL etc? -B Yet more proof assistants supported. Perhaps we will introduce +**** B Yet more proof assistants supported. Perhaps we will introduce class of "unsupported" Proof General interfaces. -B Add to proof-config those variables created in proof-easy-config for +**** B 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 More flexible help configuration is needed. HOL has some nice +**** C 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. +** 2. Things to in the generic interface + +*** 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. -* Things to in the generic interface -==================================== +*** C 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*. -B Manual improvements before techreport publishing (see notes at end also): +*** 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, @@ -77,44 +95,44 @@ B Manual improvements before techreport publishing (see notes at end also): - add screenshots? - add more index entries -C Investigate support under Mule. Suggestion we need to set +*** C Investigate support under Mule. Suggestion we need to set process-coding-system-alist somehow to prevent coding. What about Mew ? -D Change the name of "automatic multiple files" to something +*** D Change the name of "automatic multiple files" to something more comprehensible. -D X-Symbol improvements: see if we can get support for +*** D 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). -D X-Symbol improvement: turning it on/off seems to move point. +*** D X-Symbol improvement: turning it on/off seems to move point. -D Strange problem when running in tty mode: c-c c-RET seems to be +*** 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 texi-docstring-magic: first time deffn's, etc, are added, whitespace +*** D texi-docstring-magic: first time deffn's, etc, are added, whitespace after magic comment is left. -C Tidy up library-loading and dependencies. (Probably do +*** C Tidy up library-loading and dependencies. (Probably do this at the same time as organizing for the XEmacs packaging mechanism) -C Make compile should give error if any elisp compile fails. +*** C Make compile should give error if any elisp compile fails. -C Make the remaining options in the quick-opts-menu be more +*** C Make the remaining options in the quick-opts-menu be more dynamic: same function as in proof-x-symbol.el to redisplay after changing output hightlighting, make/delete frames, etc. -X Why does dired get loaded when PG loads? (Can we speed +*** X Why does dired get loaded when PG loads? (Can we speed loading by avoiding a particular function?) -B Display buffer clearing: response buffer is cleared +*** B 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 @@ -124,88 +142,88 @@ B Display buffer clearing: response buffer is cleared See attempted patch in etc/patches/fix-attempt-for-eager-cleaning.txt -B Fix problems with C-x C-v and C-x C-w +*** B Fix problems with C-x C-v and C-x C-w -B Make tags support in lego.el and coq.el a bit more generic. +*** B Make tags support in lego.el and coq.el a bit more generic. Use customization option proof-tags-support. -B Fix up sources to conform to library header conventions +*** B Fix up sources to conform to library header conventions see (lispref)Library Headers. -B Proof shell exit function -- could try sending an interrupt first +*** B 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). -B Display functions: does auto-delete-windows work with +*** B Display functions: does auto-delete-windows work with window-dedicated as it should? (I thought it would switch between 2/3 bufs as appropriate?). -B Clean up assert-until-point stuff: should have just one +*** B Clean up assert-until-point stuff: should have just one function, as a subroutine of assert-next-command; and no bizarre never-used arguments! -B proof-shell-restart should clear response buffer (only noticed with +*** B proof-shell-restart should clear response buffer (only noticed with proof-tidy-response=nil) -B Continue program of making adaptation easier. +*** B Continue program of making adaptation easier. - Test proof-easy-config mechanism. - Add proof-shell-important-settings and test that they're set. -B Documentation in pdf format: need to fix inclusion of image +*** B Documentation in pdf format: need to fix inclusion of image problem. -C See if there is a way of postponing func-menu loading. +*** C See if there is a way of postponing func-menu loading. -C Quit timeout enhancement: instead of killing immediately after +*** C Quit timeout enhancement: instead of killing immediately after timeout, could give a message "not responding, kill immediately?" -B Doc enhancement: explain conditions for switching buffers and auto +*** B Doc enhancement: explain conditions for switching buffers and auto switching of scripting buffers. (See doc of proof-auto-action-when-switching-scripting) -B make pretty printer line width altering generic. +*** B make pretty printer line width altering generic. 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). -B Implement proof-generic-find-and-forget +*** B Implement proof-generic-find-and-forget -C X-Symbol: is there a function to input in the minibuffer using +*** C X-Symbol: is there a function to input in the minibuffer using a token language? -C Investigate possible toolbar refresh problems. +*** C Investigate possible toolbar refresh problems. Sometimes extra clicks *are* needed. Why? -B "Confused" bug: shows up when do lots of C-c C-n as +*** B "Confused" bug: shows up when do lots of C-c C-n as process is starting up, when it takes a long time, esp for Isabelle. Perhaps in filter, more output arrives before properly initialized? A bit of a mystery, since code explicitly waits for initialization to complete. -B C-x C-v does not seem to run kill buffer hooks properly: at +*** B C-x C-v does not seem to run kill buffer hooks properly: at least, what happens is buffer name changes to **lose** and (e.g.) a completely processed file doesn't get added to the included files list. Auto retraction appears to work. -B Now we have proof-shell-error-or-interrupt-seen flag, we maybe don't +*** B Now we have proof-shell-error-or-interrupt-seen flag, we maybe don't need proof-shell-handle-error-hook: presently only use is in Plastic to set a similar flag. -B Add something to better document two-buffer versus three-buffer +*** 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. -B Oops --- here's an alternate and better fix to Isabelle goals +*** B Oops --- here's an alternate and better fix to Isabelle goals problem: just 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. This gets rid of the proof-goals-display-qed-message kludge. See comments in code. -C Consider supporting imenu instead, or as well as, func-menu. +*** C Consider supporting imenu instead, or as well as, func-menu. -C Fix the sentinel infinite loop bug which occurs in some cases +*** C 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 FSF Emacs. Why? See note at end of proof-shell. [2hrs] @@ -215,13 +233,13 @@ C New modules: pbp-{blah} -> proof-goals-{blah}, new proof-goals.el Low-level commands in proof-script.el -> proof-core.el -C Package management for X-Emacs. +*** C Package management for X-Emacs. - Add auto-autoloads - install under ~/.xemacs -C Improve relocatability of RPM package. +*** C Improve relocatability of RPM package. -C Improved configurability of command settings, etc. +*** C Improved configurability of command settings, etc. We should let command settings, etc, be a special type which can be one of three things: @@ -234,15 +252,15 @@ C Improved configurability of command settings, etc. args, as well as elisp functions which do whatever's necessary. Then use a generic function "proof-invoke-function" or similar. -D Consider proof-generic-goal-hyp function, for proof by +*** 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 +*** D Make code robust against accidental deletion of response/goals buffer. Add functions proof-get-or-create-{response,goals}-buffer. [30 mins] -D Making undoing better. +*** D 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 @@ -254,51 +272,51 @@ D Making undoing better. [Maybe a design principle is that spans should coincide with undoable regions] -D proof-script-next-entity-regexps: +*** 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. -C Usability enhancement: +*** 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: +*** C Usability enhancement: - Fix proof-script-command-separator and proof-one-command-per-line flag, document them. -C Make and test generic versions of <..>-goal-command-p, +*** C Make and test generic versions of <..>-goal-command-p, <...>-count-undos, to simplify prover-specific code. Reengineer *-count-undos and *-find-and-forget at generic level [5h] -D Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General +*** D Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. -D Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting +*** D Improve Makefile.devel, Makefile, ProofGeneral.spec by abstracting ELISP_DIRS somehow. -D Check support for proof-guess-command-line, new generic setting +*** 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 +*** 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: +*** 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 +*** 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. +*** 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 @@ -314,27 +332,27 @@ D Internal improvements for marking up proof assistant output. markupo in the future, too. Or maybe w3's code for HTML mark up could be borrowed. -D Idea: introduce a dynamic follow mode which follows +*** D 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] +*** 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 Check compilation okay, check on use of eval-and-compile. -X Improve efficiency for processing for large proofs. +*** 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: +*** D BUGLETS: - If Proof General is loaded with M-x load-library, it gets set up for *no* proof assistant!! - Repetition of "load .emacs" on menu bar even when it's been loaded. @@ -344,7 +362,7 @@ D BUGLETS: - are face defconsts still needed now we use defface? - XEmacs pg forces on font-lock! -D SMALL DELTAS: +*** D SMALL DELTAS: - Consider setting proof-mode-for-script automatically? Is it ever needed in the shell before the script mode has been entered? @@ -357,14 +375,14 @@ D SMALL DELTAS: implementation. Maybe we have four commands: find command start, command end, and move to next command/previous command. -X Update logo to include new "???" prover badge (maybe it should be +*** X Update logo to include new "???" prover badge (maybe it should be "...") from graphics file elsewhere (da) -X Why don't PG's minor modes appear on XEmacs minor mode menu? +*** X Why don't PG's minor modes appear on XEmacs minor mode menu? (C-right on status bar). Perhaps they shouldn't anyway, they're not very useful in non-scripting buffers. -X Usability enhancement: +*** 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 @@ -372,23 +390,23 @@ X Usability enhancement: This suggestion is based on observation of a user's confusion when the toolbar disappears from other PG buffers. -X Compatibility enhancement: +*** 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 +*** X bug: outline mode when proof-strict-read-only is nil ought to work, but there may be problems. -X CVS repository issues. +*** X CVS repository issues. 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 +*** 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. +*** 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 @@ -400,22 +418,22 @@ X Fixup display problems. proof-display-and-keep-buffer? [da: can't repeat this now, presume it has gone away?] -D Make completion more generic. For Isabelle and Lego, we can build a +*** 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 +*** D outline configuration should be generic (or else documented for each prover separately, since not guaranteed to work for all). -D Check matching code carefully, in view of bug reported (now fixed) +*** D 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] -D Implement proof-auto-retract idea. [4hrs] +*** D Implement proof-auto-retract idea. [4hrs] -D da: Suggested improvement to interface for included files: +*** 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 @@ -430,20 +448,20 @@ D da: Suggested improvement to interface for included files: 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 +*** 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) -X Process handling output. +*** 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. -D proof-goal-command-regexp: the syntax of Coq spoils the +*** 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 @@ -452,28 +470,28 @@ D proof-goal-command-regexp: the syntax of Coq spoils the function to be invoked instead? (Cf font lock). Or via a new generic mechanism for matching or invoking a fn. -D Improve indentation code and see why it's so slow (at +*** D 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). -D ROBUSTness: deal gracefully with possibility that goals buffer is +*** D 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 +*** D Add support to filter out unwanted noise from the prover by setting up a regular expression proof-shell-noise-regexp [2hr] -D support for templates e.g., in LEGO it would be nice if, by default, +*** 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. [2hr] -D Review and prune "FIXME notes" which are notes about ongoing fixes +*** 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 +*** 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: +*** 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; @@ -482,9 +500,9 @@ D Improve proof-goal-command and proof-save-command: 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;")) + (setq proof-goal-command (proof-prompt-named-goal "Goal %s :" "%s;")) -X Cleanup handling of proof-terminal-string. At the moment some +*** 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. @@ -494,19 +512,19 @@ X Cleanup handling of proof-terminal-string. At the moment some [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 +*** 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 +*** X Write test schedule for things to try out with a new instantiation of Proof General. -X automise testing procedures in etc/ +*** X automise testing procedures in etc/ -C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's. +*** 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 +*** 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: @@ -515,34 +533,34 @@ D Perhaps goal..save sequences should be closed also by the appearance <new goal> .. - Will ACS idea handle this? +*** Will ACS idea handle this? -D Multiple files: handle failures in reading ancestors. +*** D Multiple files: handle failures in reading ancestors. -D Provide a sensible default frame/buffer layout (4h) +*** D Provide a sensible default frame/buffer layout (4h) -D Implement mouse drag-and-drop support for selecting subterms in the +*** 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 +*** 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 +*** 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 +*** 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 Implement a function to undo to the previous goal. -D Remove duplication of variables e.g., proof-prog-name and +*** 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 +*** 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). @@ -550,43 +568,43 @@ D Display management is much better than it was, but perhaps and the goals buffer is updated: might like to still see what was in the response buffer. - Oddities: +*** D 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. -C Support an extended version of dynamic abbreviations, to work +*** 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. -D Is it possible to let C-c C-c (SIGINT) issue additional process input? +*** D 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. -D Make wellclean target remove images in html/images which are +*** 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 splash screen: report XEmacs problem of not displaying transparent +*** X splash screen: report XEmacs problem of not displaying transparent gif properly. -X Consider filtering out special annotations from shell buffer +*** X Consider filtering out special annotations from shell buffer rather than merely making them invisible. Probably NOT: this is a design decision that interaction with the shell should be minimal, so we don't help with fontifying or fixing cut-and-paste. -X Allow bib-cite style clicking on Load/Import commands to go +*** 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 +*** 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 +*** 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 @@ -599,42 +617,42 @@ X Customization mechanism: is there a way to make saved settings 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 +*** 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 +*** 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. +*** X Span convenience functions for special 'type property. Could put these in proof.el or somewhere. - (defsubst set-span-type-property (span val) +*** (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) +*** (defsubst span-type-property (span) "Get type property of SPAN" (span-property span 'type)) - etc. (1hr) +*** etc. (1hr) -X Read-only mode of extents sometimes gets in the way: for example, +*** 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 +*** 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 +*** 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 General customization: how should it work? +*** X Proof General customization: how should it work? Presently we have a bunch of variables in proof.el which are set from a bunch of similarly named variables in <engine>-syntax.el. Seems a bit daft: why not just have the customization in @@ -642,7 +660,7 @@ X Proof General customization: how should it work? That way we can see which settings are part of instantiation of proof.el, and which are part of cusomization for <engine>. -X Moreover, I think it would be nice to change the architecture +*** 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 @@ -657,19 +675,19 @@ X Moreover, I think it would be nice to change the architecture 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 +*** 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 +*** 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 +*** 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, +*** 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 @@ -679,7 +697,7 @@ X Make process handling smarter: because Emacs is single-threaded, 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 +*** 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" @@ -689,11 +707,11 @@ X Ideas for efficiency improvements. Rather than repeatedly The function proof-segment-up-to could be made to cache its result. -X proof-mark-buffer-atomic marks the buffer as only containing +*** 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: +*** 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 @@ -702,10 +720,9 @@ X Idea for future re-engineering: -* FSF Emacs issues -================== +** 3. FSF Emacs issues -B Changed implementation of overlays inside Emacs itself. We seem to +*** B 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 highlighting is strange, and background face spoils the others. Transparent? @@ -713,44 +730,43 @@ B Changed implementation of overlays inside Emacs itself. We seem to 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 +*** 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) -* Things to do for Proof-by-Pointing -==================================== +** 4. Things to do for Proof-by-Pointing -B Unify proof-insert-pbp-command and proof-shell-insert-loopback-cmd. +*** 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. +*** 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 Usability enhancement: have a ballon-help style popup (in the +*** C Usability enhancement: have a ballon-help style popup (in the minibuffer) to indicate what command pbp will choose, without actually running it. -C Fixing up errors caused by pbp-generated commands; currently, script +*** 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 +*** 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 +*** 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. @@ -758,72 +774,74 @@ X pbp code doesn't quite accord with the tech report; in particular it -* Things to do for Web Pages, Distribution -========================================== +** 5. Things to do for Web Pages, Distribution -A Add some one-stop-shop pages. Ask permission to redistribute + +*** A Update ETAPS demo + +*** A Add some one-stop-shop pages. Ask permission to redistribute packages for PAs. Maybe do Windows and Linux versions. -B Add an animation, showing proof replay. +*** B Add an animation, showing proof replay. -B Validate pages. +*** B Validate pages. Current failures for HTML 4.0 to do with CGI-style arguments with "&", this is a problem with PHP3 really. -B Update ETAPS demo - -C Wanted for links: something to UITP. Are there any pages? +*** C Wanted for links: something to UITP. Are there any pages? -C Broken (old) links: +*** C Broken (old) links: (Applications of a Type Theory based Proof Assistant) http://www.dcs.ed.ac.uk/lfcs/research/logic_and_proof/attbpa.html -C Reduce text size and front page image, for 1024x768 screens. +*** C Reduce text size and front page image, for 1024x768 screens. -D Restructure so that page titles are different to help +*** D 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). -C Add etc/announce somewhere. +*** C Add etc/announce somewhere. -X Convert to SSI only plus a meta-generation phase? +*** X Convert to SSI only plus a meta-generation phase? -X Check appearance in V3 browsers. +*** X Check appearance in V3 browsers. -X Make front page logo be an image map. -X Add status bar messages to navigation bar +*** X Make front page logo be an image map. -X Get rid of footer() function. +*** X Add status bar messages to navigation bar +*** X Get rid of footer() function. -* Bugs in other software beyond our control -=========================================== -X Odd behaviour of font-lock in script buffers when long strings + +** 6. Bugs in other software beyond our control + + +*** 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 +*** 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 spurious byte comp warning in XEmacs 21.1.4: +*** X spurious byte comp warning in XEmacs 21.1.4: While compiling proof-x-symbol-encode-shell-input: ** buffer-substring called with 3 args, but requires 0-3 for this code: (prog1 (buffer-substring) (kill-buffer (current-buffer)) -X Error with pdftexinfo (hacked version of teTeX pre-release, 1.0.6). +*** X Error with pdftexinfo (hacked version of teTeX pre-release, 1.0.6). Gives problem with @value{blah} inside @pdfurl. May be absent from pdftexinfo.tex, but that version doesn't seem to generate web links? -(/usr/share/texmf.local/pdftex/texinfo/pdftexinfo.tex +*** (/usr/share/texmf.local/pdftex/texinfo/pdftexinfo.tex Loading texinfo [version 1999-09-25.10]: Basics, pdf, (/usr/share/texmf/pdftex/plain/misc/pdfcolor.tex) fonts, page headings, tables, conditionals, indexing, sectioning, toc, environments, defuns, macros, @@ -860,55 +878,53 @@ Output written on ProofGeneral.pdf (2 pages, 54702 bytes). -* 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) - Even if the code is faulty afterwards, compiling is - worthwhile just because it shows up bugs in unbound variables, etc. -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. -9. Update and distribute etc/announce. - Message to PG mailing list. +** 7. 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) + Even if the code is faulty afterwards, compiling is + worthwhile just because it shows up bugs in unbound variables, etc. +*** 4. Dates and versions updated. + Check 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. +*** 9. Update and distribute etc/announce. +*** 10. Message to PG mailing list. + + +** 8. Things to do for Proof General Project -* Things to do for Proof General Project -======================================== -A Try to get small project grant from LFCS to help with +*** A Try to get small project grant from LFCS to help with development of Proof General. Latest news: success is doubtful. Needs a self-contained project that *would be useful to LFCS* -A Find new people to help advance and develop Proof General. +*** A Find new people to help advance and develop Proof General. Getting more instances would be a good way. Also encouraging feedback. Here stories of bugs by word-of-mouth, they don't get reported often enough. Consider passing on project elsewhere if no LFCS interest. -A Polish ProofGeneral.texi and publish LaTeX as an LFCS - Technical Report. +*** A Polish ProofGeneral.texi and publish LaTeX as a tech report -A Write paper on design and development of Proof General. +*** A Write paper on design and development of Proof General. -A Write white paper on future of PG project. +*** A Write white paper on future of PG project. -A Write grant proposal on white paper to generate funding for - Proof General. +*** A Write grant proposal on white paper for Proof General Kit. -A Add more PG projects, ensure interest is generated and as many - as possible proposed!
\ No newline at end of file +*** A Add more PG projects, ensure interest is generated! |