diff options
| -rw-r--r-- | doc/NewDoc.texi | 127 | ||||
| -rw-r--r-- | doc/notes.txt | 4 | ||||
| -rw-r--r-- | lego/lego.el | 31 |
3 files changed, 126 insertions, 36 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index 607285a5..157bc477 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -637,11 +637,13 @@ Otherwise, you will need to restart script management altogether, @pxref{Toolbar @menu * Support for function menus:: +* Support for tags:: @end menu @node Support for function menus @section Support for function menus @vindex proof-goal-with-hole-regexp +@cindex fume-func fume-func is a handy package which makes a menu from the function declarations in a buffer. Proof General configures fume-func so that @@ -669,7 +671,11 @@ the following code for your @file{.emacs} file: If you have another version of Emacs, you should check the fume-func.el file supplied with it. +@node Support for tags +@section Support for tags +@cindex tags +@c FIXME: instructions for setting up etags are needed @node Customizing Proof General @@ -821,36 +827,106 @@ At present there is no easy way to get around this. @node LEGO Proof General @chapter LEGO Proof General -LEGO mode is a mode derived from proof script mode for editing LEGO -scripts. An important convention is that proof script buffers @emph{must} -start with a module declaration. If the proof script buffer's file name -is @file{fermat.l}, then it must commence with a declaration +LEGO proof script mode is a mode derived from proof script mode for +editing LEGO scripts. An important convention is that proof script +buffers @emph{must} start with a module declaration. If the proof script +buffer's file name is @file{fermat.l}, then it must commence with a +declaration of the form @lisp +Module fermat; +@end lisp + +If, in the development of the module @samp{fermat}, you require material +from other module e.g., @samp{lib_nat} and @samp{galois}, you need to +specify this dependency as part of the module declaration: +@lisp +Module fermat Import lib_nat galois; @end lisp +No need to worry too much about effeciency. When you retract back to a +module declaration to add a new import item, LEGO does not actually +retract the previously imported modules. Therefore, reasserting the +extended module declaration really only processes the newly imported +modules. +Using the LEGO Proof General, you never ever need to use administrative +LEGO commands such as @samp{Forget}, @samp{ForgetMark}, @samp{KillRef}, +@samp{Load}, @samp{Make}, @samp{Reload} and @samp{Undo} again +@footnote{And please, don't even think of including those in your LEGO +proof script!}. You can concentrate on your actual proof developments. +Script management in the Proof General will invoke the appropriate +commands for you. Proving with LEGO has never been easier. @menu * LEGO specific commands:: +* LEGO tags:: * LEGO customizations:: @end menu @node LEGO specific commands @section LEGO specific commands +In addition to the commands provided by the generic Proof General, see +the previous sections, the LEGO Proof General provides a few extensions. +In proof scripts, there are some abbreviations for common commands: + +@table @kbd +@item C-c i +intros +@item C-c I +Intros +@item C-c R +Refine +@end table + +@node LEGO tags +@section LEGO tags + +The LEGO Proof General provides the program @file{legotags} to generate +tags for LEGO proof scripts. Invoking @samp{legotags *.l} produces a +file @file{TAGS} for all LEGO modules in the current directory. The LEGO +library itself is shipped out with all its modules already being tagged. +See @ref{Support for tags} for further details. + + @node LEGO customizations @section LEGO customizations -********** +We refer to chapter @ref{Customizing Proof General} for an introduction +to the customisation mechanism. In addition to customizations at the +generic level, for LEGO you can also customize: + +@defopt lego-tags +The directory of the TAGS table for the LEGO library. The default is +@code{"/usr/lib/lego/lib_Type/"}. +@end defopt + +@defopt lego-help-menu-list +List of menu items, as defined in @code{easy-menu-define} for LEGO + specific help. +@end defopt + +@c We don't worry about the following for now. These are too obscure. +@c lego-indent +@c lego-test-all-name -Support for font-lock under FSF Emacs 20.2 +@c We also don't document any of the internal variables which have been +@c set to configure the generic Proof General and which the user should +@c not tamper with -To automatically switch on fontification, set +In Xemacs 20.4, LEGO script buffer are coloured (fontified as they say) +by default. To automatically switch on fontification in FSF Emacs 20.2, +you need to set +@vindex lego-mode-hooks +@cindex font-lock colour +@lisp (add-hook 'lego-mode-hooks 'turn-on-font-lock) - ^ +@end lisp + +in your @file{~/.emacs} file. @@ -1232,6 +1308,14 @@ in the distribution for more detailed and up-to-date information. @* If you discover a problem which isn't mentioned in @file{BUGS}, please let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. +@menu +* Bugs at the generic level:: +* Bugs specific to LEGO Proof General:: +@end menu + +@node Bugs at the generic level +@section Bugs at the generic level + @unnumberedsubsec Undo in XEmacs Ordinary undo in script buffer can edit the "uneditable region" in @@ -1259,6 +1343,33 @@ simultaneously. @strong{Workaround:} stick to one prover per Emacs session. +@node Bugs specific to LEGO Proof General +@section Bugs specific to LEGO Proof General + +Getting retracting right is tricky when working on proofs. + +@unnumberedsubsec Definitions in a proof state +A thorny issues are local +definitions in a proof state. LEGO cannot undo them explicitly. + +@strong{Workaround:} retract back to a command before a definition. + +@unnumberedsubsec Normalisation in proofs +Normalisation commands such as @samp{Dnf}, @samp{Hnf} @samp{Normal} +cannot be undone in a proof state by the Proof General. + +@strong{Workaround:} retract back to the start of the proof. + +@unnumberedsubsec Not saving proofs. +After LEGO has issued a @samp{*** +QED ***} you may undo steps in the proof as long as you don't issue a +@samp{Save} command or start a new proof. The LEGO Proof General assumes +that all proofs are terminated with a proper @samp{Save} command. + +@strong{Workaround:} Always issue a @samp{Save} command after completing +a proof. If you forget one, you should retract to a point before the +offending proof development. + diff --git a/doc/notes.txt b/doc/notes.txt index 5ebe8c35..fd32d00b 100644 --- a/doc/notes.txt +++ b/doc/notes.txt @@ -26,7 +26,7 @@ Suggestion for outline of improved documentation. 2.5 Other commands 2.4 Walkthrough example [maybe in appendix?] - 3. Advanced script management [tms] + 3. Advanced script management [done] 3.1 Proof General's view of processed files 3.2 Switching between proof scripts 3.3 Retracting across files @@ -41,7 +41,7 @@ Suggestion for outline of improved documentation. 4.2 Using proof assistant on another machine 4.3 Examining configuration settings (xref'd later) - 5. LEGO Proof General [tms] + 5. LEGO Proof General [done] 5.1 LEGO commands 5.2 LEGO customizations diff --git a/lego/lego.el b/lego/lego.el index 72b81f0b..04f02224 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -25,7 +25,7 @@ ;; I believe this is standard for Linux under RedHat -tms (defcustom lego-tags "/usr/lib/lego/lib_Type/" - "*the default TAGS table for the LEGO library" + "*The directory of the TAGS table for the LEGO library" :type 'file :group 'lego) @@ -89,7 +89,7 @@ :group 'lego) (defcustom lego-www-latest-release - "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3/" + "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3.1/" "The WWW address for the latest LEGO release." :type 'string :group 'lego) @@ -107,17 +107,6 @@ :group 'lego) -;; ----- legostat and legogrep, courtesy of Mark Ruys - -(defvar legogrep-command (concat "legogrep -n \"\" " lego-test-all-name) - "Last legogrep command used in \\{legogrep}; default for next legogrep.") - -(defvar legostat-command "legostat -t") - -(defvar legogrep-regexp-alist - '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) - "Regexp used to match legogrep hits. See `compilation-error-regexp-alist'.") - ;; ----- lego-shell configuration options (defvar lego-prog-name "lego" @@ -297,11 +286,6 @@ (defun lego-state-preserving-p (cmd) (not (string-match lego-undoable-commands-regexp cmd))) -(defun lego-retract-command (file) - "LEGO command to retract file." - (concat "ForgetMark file " - (file-name-sans-extension (file-name-nondirectory file)))) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Commands specific to lego ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -522,14 +506,9 @@ We assume that module identifiers coincide with file names." proof-shell-retract-files-regexp "forgot back through Mark \"\\(.*\\)\"" - ;;FIXME: we ought to set up separate font-lock instructions for - ;;the response, the goal buffer and the script - font-lock-keywords lego-font-lock-keywords-1) - -;; FIXME: da: I've removed this, I think fset is bad and proof-retract-command -;; doesn't seem to exist. -;; (fset 'proof-retract-command 'lego-retract-command) - (setq proof-shell-compute-new-files-list + font-lock-keywords lego-font-lock-keywords-1 + + proof-shell-compute-new-files-list 'lego-shell-compute-new-files-list) (lego-init-syntax-table) |