diff options
| -rw-r--r-- | BUGS | 27 | ||||
| -rw-r--r-- | CHANGES | 22 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 162 |
3 files changed, 146 insertions, 65 deletions
@@ -11,16 +11,24 @@ See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS Generic problems ================ -* Highlighting of locked (blue) and queue (red) regions in FSF Emacs -may be unreliable (disappear) in some cases. Cause unknown. If you -observe this, please submit a bug report with details of your system -and any other information you think may be relevant. Workaround: -switch to using XEmacs. +* 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. * 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). Please report cases where the -buttons are enabled/disabled at the wrong time. +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. + +* Synchronization during start-up: if you press C-c C-n quickly +in succession whilst the prover is cranked up, synchronization +may be spoilt, and you see the message "script management confused" +later on. This is a minor bug, most likely to be noticed when it +takes a while to start the proof assistant (e.g. Isabelle!). +Workarounds: many! Type slowly. Use C-c C-RET. Start the prover +first via the menu, or C-c C-s. * Ordinary undo in the script buffer can edit the "uneditable region" in XEmacs. This doesn't happen in FSFmacs. Test case: @@ -56,10 +64,6 @@ problem with outline because it works by modifying the buffer. Workaround: none, nevermind. (If it's hugely needed we could support modified outline commands). -* `proof-find-next-terminator' (bound to C-c C-e) doesn't work -properly. Neither does 'proof-goto-command-start' (C-c C-a). -Workaround: use other means to navigate in a proof scipt buffer. - * 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, @@ -82,7 +86,6 @@ using rsh instead, it is said to forward signals to the remote command. - LEGO Proof General Bugs ======================= @@ -4,6 +4,20 @@ Summary of Changes for Proof General 3.0 from 2.1 Generic Changes --------------- +* The excellent X-Symbol package is now well supported by + Proof General. This allows proof assistants to display logical + symbols, Greek letters, etc, with ease. The original patches + for Isabelle are courtesy of David von Oheimb. There are + early experimental configurations provided for LEGO and Coq + which use ordinary character sequences rather than escaped + tokens (so "/\" appears as a wedge, and "Gamma" appears + as the letter Gamma). You may need to install X-Symbol first; + visit http://www.fmi.uni-passau.de/~wedler/x-symbol + +* Demonstration instance of Proof General for Isabelle shows + how you can get the interface going with a minimum of fuss. + It has just 30 simple settings. + * Proof General is now more cany about the queue of commands. You can now add more proof commands on the end of the queue, without the "Proof Process Busy" message. @@ -82,6 +96,14 @@ Generic Changes assistant to load files it depends on, so it is also handy to see what happens before scripting begins in the buffer. +* Proof by pointing has been re-enabled in the code. + LEGO's implementation of the proof-by-pointing rule choices + is dodgy, but works sometimes, and it is nice to demonstrate + Proof General's support for pbp until another prover implements + it. (It should be straightforward to implement for Coq, since the + CtCoq pbp code is now embedded in the core system; we need + a Coq expert to do this). + * Cleaned up example files so all demonstrate same theorem "conj_comms". Would be nice to add more theorems to compare scripts/proofs in different systems. Please send in example scripts! diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 38750386..2dd0dbd2 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -503,8 +503,18 @@ General. For more details, see @ref{Toolbar commands}, @ref{Proof assistant commands}, and @ref{Customizing Proof General}. -@c not yet -@c @item @i{Proof by pointing} +@item @i{Proof by pointing} +Proof General has support for proof-by-pointing and similar features. +Proof by pointing allows you to click on a subterm of a goal to +be proved, and automatically apply an appropriate proof rule or +tactic. Proof by pointing is specific to the proof assistant +(and logic) in use; therefore it is configured mainly on the +proof assistant side. +@c Proof General expects to parse +@c term-structure annotations on the output syntax of the prover. +@c It uses these to construct a message to the prover indicating +@c where the user has clicked, and the proof assistant can +@c response with a suggested tactic. @end itemize @@ -1000,8 +1010,8 @@ Move point to start of current (or final) command of the script. @end deffn @c TEXI DOCSTRING MAGIC: proof-goto-command-end -@deffn Command proof-find-next-terminator -Set point after next @samp{@code{proof-terminal-char}}. +@deffn Command proof-goto-command-end +Set point to next @samp{@code{proof-terminal-char}}. @end deffn @vindex proof-terminal-char @@ -2096,7 +2106,8 @@ One basic example of a setting you may like to tweak is: @c TEXI DOCSTRING MAGIC: proof-assistant-home-page @defvar proof-assistant-home-page -Web address for information on proof assistant +Web address for information on proof assistant.@* +Used for Proof General's help menu. @end defvar Most of the others are more complicated. For more details of the settings, @@ -2714,7 +2725,8 @@ commands and menus available in Proof General. @c TEXI DOCSTRING MAGIC: proof-assistant-home-page @defvar proof-assistant-home-page -Web address for information on proof assistant +Web address for information on proof assistant.@* +Used for Proof General's help menu. @end defvar @c TEXI DOCSTRING MAGIC: proof-context-command @defvar proof-context-command @@ -2771,12 +2783,17 @@ String which starts a comment in the proof assistant command language.@* The script buffer's @code{comment-start} is set to this string plus a space. Moreover, comments are ignored during script management, and not sent to the proof process. + +You should set this variable for reliable working of Proof General, +as well as @samp{@code{proof-comment-end}}. @end defvar @c TEXI DOCSTRING MAGIC: proof-comment-end @defvar proof-comment-end String which ends a comment in the proof assistant command language.@* The script buffer's @code{comment-end} is set to this string plus a space. See also @samp{@code{proof-comment-start}}. + +You should set this variable for reliable working of Proof General, @end defvar @c TEXI DOCSTRING MAGIC: proof-case-fold-search @defvar proof-case-fold-search @@ -2798,7 +2815,7 @@ Used for setting names of goal..save regions and for default @end defvar @c TEXI DOCSTRING MAGIC: proof-goal-command-regexp @defvar proof-goal-command-regexp -Matches a goal command. +Matches a goal command in the proof script. Must be set. @end defvar @c TEXI DOCSTRING MAGIC: proof-goal-with-hole-regexp @defvar proof-goal-with-hole-regexp @@ -2807,6 +2824,20 @@ Match number 2 should be the name of the goal issued. Used for setting names of goal..save regions and for default @code{function-menu} configuration in @code{proof-script-find-next-entity}. @end defvar +@c TEXI DOCSTRING MAGIC: proof-non-undoables-regexp +@defvar proof-non-undoables-regexp +Regular expression matching commands which are @strong{not} undoable.@* +Used in default functions @samp{@code{proof-generic-state-preserving-p}} +and @samp{@code{proof-generic-count-undos}}. If you don't use those, +May be left as nil. +@end defvar +@c TEXI DOCSTRING MAGIC: proof-ignore-for-undo-count +@defvar proof-ignore-for-undo-count +Matcher for script commands to be ignored in undo count.@* +May be left as nil, in which case it will be set to +@samp{@code{proof-non-undoables-regexp}}. +Used in default function @samp{@code{proof-generic-count-undos}}. +@end defvar @c TEXI DOCSTRING MAGIC: proof-script-next-entity-regexps @defvar proof-script-next-entity-regexps Regular expressions to help find definitions and proofs in a script.@* @@ -2868,7 +2899,7 @@ default. @c TEXI DOCSTRING MAGIC: proof-goal-command-p @defvar proof-goal-command-p -Is this really a goal command? +A function to test: is this really a goal command? @end defvar @c TEXI DOCSTRING MAGIC: proof-completed-proof-behaviour @defvar proof-completed-proof-behaviour @@ -2906,10 +2937,25 @@ or if you don't want to write a function to do move them around. @end defvar @c TEXI DOCSTRING MAGIC: proof-count-undos-fn @defvar proof-count-undos-fn -Function to compute number of undos in a target segment.@* +Function to calculate a command to issue undos to reach a target span.@* +The function takes a span as an argument, and should return a string +which is the command to undo to the target span. The target is +guaranteed to be within the current (open) proof. This is an important function for script management. -Study one of the existing instantiations for examples of how to write it. +The default setting @samp{@code{proof-generic-count-undos}} is based on the +settings @samp{@code{proof-non-undoables-regexp}} and +@samp{@code{proof-non-undoables-regexp}}. @end defvar +@c TEXI DOCSTRING MAGIC: proof-generic-count-undos +@defun proof-generic-count-undos span +Count number of undos in a span, return command needed to undo that far.@* +Command is set using @samp{@code{proof-undo-n-times-cmd}}. + +A default value for @samp{@code{proof-count-undos-fn}}. + +For this function to work properly, you must configure +@samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}. +@end defun @c TEXI DOCSTRING MAGIC: proof-find-and-forget-fn @defvar proof-find-and-forget-fn Function that returns a command to forget back to before its argument span.@* @@ -2921,15 +2967,37 @@ of definitions, declarations, or whatever. The special string @code{proof-no-command} means there is nothing to do. +Important: the generic implementation @samp{@code{proof-generic-find-and-forget}} +does nothing, it always returns @samp{@code{proof-no-command}}. + This is an important function for script management. Study one of the existing instantiations for examples of how to write it. @end defvar +@c TEXI DOCSTRING MAGIC: proof-generic-find-and-forget + +@defun proof-generic-find-and-forget span +Calculate a forget/undo command to forget back to @var{span}.@* +This is a long-range forget: we know that there is no +open goal at the moment, so forgetting involves unbinding +declarations, etc, rather than undoing proof steps. + +@var{currently} @var{unimplemented}: just returns @code{proof-no-command}. +Check the @code{lego-find-and-forget} or @code{coq-find-and-forget} +functions for examples of how to write this function. + +In the next release of Proof General, there will be +a generic implementation of this. +@end defun @c TEXI DOCSTRING MAGIC: proof-goal-hyp-fn @defvar proof-goal-hyp-fn Function which returns cons cell if point is at a goal/hypothesis.@* -First element of cell is a symbol, @code{'goal'} or @code{'hyp'}. The second -element is a string: the goal or hypothesis itself. This is used -when parsing the proofstate output. +This is used to parse the proofstate output to mark it up for +proof-by-pointing. It should return a cons or nil. First element of +the cons is a symbol, @code{'goal'} or @code{'hyp'}. The second element is a +string: the goal or hypothesis itself. + +If you leave this variable unset, no proof-by-pointing markup +will be attempted. @end defvar @c TEXI DOCSTRING MAGIC: proof-kill-goal-command @defvar proof-kill-goal-command @@ -3071,6 +3139,14 @@ The @code{proof-terminal-char} is added on to the end. A command to quit the proof process. If nil, send EOF instead.@* The @code{proof-terminal-char} is added on to the end. @end defvar +@c TEXI DOCSTRING MAGIC: proof-shell-quit-timeout +@defvar proof-shell-quit-timeout +The number of seconds to wait after sending @code{proof-shell-quit-cmd}.@* +After this timeout, the proof shell will be killed of more rudely. +If your proof assistant takes a long time to clean up (for +example writing persistent databases out or the like), you may +need to bump this value up. +@end defvar @c TEXI DOCSTRING MAGIC: proof-shell-cd-cmd @defvar proof-shell-cd-cmd Command to the proof assistant to change the working directory.@* @@ -3145,10 +3221,13 @@ Set to nil if proof assistant does not support annotated prompts. First special character.@* Codes above this character can have special meaning to Proof General, and are stripped from the prover's output strings. +Leave unset if no special characters are being used. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-prompt-pattern @defvar proof-shell-prompt-pattern -Proof shell's value for comint-prompt-pattern, which see. +Proof shell's value for comint-prompt-pattern, which see.@* +This pattern is just for interaction in comint (shell buffer). +You don't really need to set it. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp @defvar proof-shell-annotated-prompt-regexp @@ -3217,13 +3296,20 @@ and possibly analysed further for proof-by-pointing markup. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp @defvar proof-shell-end-goals-regexp -Regexp matching the end of the proof state output. +Regexp matching the end of the proof state output, or nil.@* +If nil, just use the rest of the output following @code{proof-shell-start-goals-regexp}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-start @defvar proof-shell-eager-annotation-start Eager annotation field start. A regular expression or nil.@* -An eager annotation indicates to Emacs that some following output -should be displayed immediately and not accumulated for parsing. +An eager annotation indicates to Proof General that some following output +should be displayed immediately and not accumulated for parsing later. +It's nice to recognize warnings or file-reading messages with this +regexp. + +See also @samp{@code{proof-shell-eager-annotation-start-length}}, +@samp{@code{proof-shell-eager-annotation-end}}. + Set to nil to disable this feature. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-eager-annotation-end @@ -3442,45 +3528,15 @@ See documentation of @code{proof-shell-start-char}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-goal-char @defvar proof-shell-goal-char -goal mark -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-field-char -@defvar proof-shell-field-char -annotated field end -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-start-char -@defvar proof-shell-start-char -Starting special for a subterm markup.@* -Subsequent characters with values @strong{below} @code{proof-shell-first-special-char} -are assumed to be subterm position indicators. Subterm markups should -be finished with @code{proof-shell-end-char}. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-end-char -@defvar proof-shell-end-char -Finishing special for a subterm markup.@* -See documentation of @code{proof-shell-start-char}. -@end defvar -@c TEXI DOCSTRING MAGIC: proof-shell-goal-char -@defvar proof-shell-goal-char -goal mark +Mark for goal. + +This setting is also used to see if proof-by-pointing features +are configured. If it is unset, some of the code +for parsing the is disabled. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-field-char @defvar proof-shell-field-char -annotated field end -@end defvar - - -The final setting just configures where the ``proof completed'' -message appears. -@c TEXI DOCSTRING MAGIC: proof-goals-display-qed-message -@defvar proof-goals-display-qed-message -If non-nil, display the proof-completed message in the goals buffer.@* -For some proof assistants (e.g. Isabelle) it seems aesthetic to -display the QED message in the goals buffer, even though it doesn't -contain any goals and shouldn't be marked up for proof-by-pointing. - -If this setting is non-nil, QED messages appear in the goals -buffer. Otherwise they appear in the response buffer. +Annotated field end @end defvar |