diff options
| -rw-r--r-- | CHANGES | 11 | ||||
| -rw-r--r-- | ci/simple-tests/.gitignore | 1 | ||||
| -rw-r--r-- | ci/simple-tests/omit_test.v | 25 | ||||
| -rw-r--r-- | ci/simple-tests/test-omit-proofs.el | 154 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 25 | ||||
| -rw-r--r-- | coq/coq.el | 8 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 92 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 109 | ||||
| -rw-r--r-- | generic/pg-user.el | 56 | ||||
| -rw-r--r-- | generic/proof-config.el | 64 | ||||
| -rw-r--r-- | generic/proof-faces.el | 7 | ||||
| -rw-r--r-- | generic/proof-menu.el | 6 | ||||
| -rw-r--r-- | generic/proof-script.el | 193 | ||||
| -rw-r--r-- | generic/proof-useropts.el | 15 |
14 files changed, 736 insertions, 30 deletions
@@ -151,6 +151,17 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac To change the default blacklist, set variable coq-search-blacklist-string (unchanged). +*** Proof General can omit complete opaque proofs + This speeds up asserting of larger chunks at the price of + letting errors in these proofs go unnoticed. Configure + `proof-omit-proofs-option' or select "Proof-General -> Quick + Options -> Processing -> Omit Proofs". See also section + "11.5 Omitting proofs for speed" in the manual. + + Beware that if lemmas are proved in a section, these lemmas should + start with a "Proof using" annotation, otherwise Coq would compute + a wrong type for them when this omitting-proofs feature is enabled. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some diff --git a/ci/simple-tests/.gitignore b/ci/simple-tests/.gitignore new file mode 100644 index 00000000..67f5cfcf --- /dev/null +++ b/ci/simple-tests/.gitignore @@ -0,0 +1 @@ +*.success diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v new file mode 100644 index 00000000..b8d177cc --- /dev/null +++ b/ci/simple-tests/omit_test.v @@ -0,0 +1,25 @@ + +Definition classical_logic : Prop := forall(P : Prop), ~~P -> P. + +(* automatic test marker 1 *) + +Lemma classic_excluded_middle : + (forall(P : Prop), P \/ ~ P) -> classical_logic. +Proof. + intros H P H0. + (* automatic test marker 2 *) + specialize (H P). +Abort. + +Lemma classic_excluded_middle : + (forall(P : Prop), P \/ ~ P) -> classical_logic. +Proof using. + intros H P H0. + specialize (H P). + (* automatic test marker 3 *) + destruct H. + trivial. + contradiction. +Qed. + +(* automatic test marker 4 *) diff --git a/ci/simple-tests/test-omit-proofs.el b/ci/simple-tests/test-omit-proofs.el new file mode 100644 index 00000000..20170e13 --- /dev/null +++ b/ci/simple-tests/test-omit-proofs.el @@ -0,0 +1,154 @@ +;; This file is part of Proof General. +;; +;; © Copyright 2021 Hendrik Tews +;; +;; Authors: Hendrik Tews +;; Maintainer: Hendrik Tews <hendrik@askra.de> +;; +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; +;; Test the omit proofs feature +;; +;; Test that with proof-omit-proofs-option +;; - the proof _is_ processed when using a prefix argument +;; - in this case the proof as normal locked color +;; - without prefix arg, the proof is omitted +;; - the proof has omitted color then +;; - stuff before the proof still has normal color + +;; reimplement seq-some from the seq package +;; seq-some not present in emacs 24 +;; XXX consider to switch to seq-some when support for emacs 24 is dropped +(defun list-some (pred list) + "Return non-nil if PRED is satisfied for at least one element of LIST. +If so, return the first non-nil value returned by PRED." + (let (res) + (while (and (consp list) (not res)) + (setq res (funcall pred (car list))) + (setq list (cdr list))) + res)) + +(defun wait-for-coq () + "Wait until processing is complete." + (while (or proof-second-action-list-active + (consp proof-action-list)) + ;; (message "wait for coq/compilation with %d items queued\n" + ;; (length proof-action-list)) + ;; + ;; accept-process-output without timeout returns rather quickly, + ;; apparently most times without process output or any other event + ;; to process. + (accept-process-output nil 0.1))) + +(defun overlay-less (a b) + "Compare two overlays. +Return t if overlay A has smaller size than overlay B and should +therefore have a higher priority." + (let ((sa (- (overlay-end a) (overlay-start a))) + (sb (- (overlay-end b) (overlay-start b)))) + (<= sa sb))) + +(defun overlays-at-point-sorted () + "Return overlays at point in decreasing order of priority. +Works only if no overlays has a priority property. Same +'(overlays-at (point) t)', except that it also works on Emacs <= 25." + (sort (overlays-at (point) t) 'overlay-less)) + +(defun first-overlay-face () + "Return the face of the first overlay/span that has a face property. +Properties configured in that face are in effect. Properties not +configured there may be taken from faces with less priority." + (list-some + (lambda (ov) (overlay-get ov 'face)) + ;; Need to sort overlays oneself, because emacs 25 returns overlays + ;; in increasing instead of decreasing priority. + (overlays-at-point-sorted))) + +(ert-deftest omit-proofs-omit-and-not-omit () + "Test the omit proofs feature. +In particular, test that with proof-omit-proofs-option configured: +- the proof _is_ processed when using a prefix argument +- in this case the proof as normal locked color +- without prefix arg, the proof is omitted +- the proof has omitted color then +- stuff before the proof still has normal color " + (setq proof-omit-proofs-option t + proof-three-window-enable nil) + (find-file "omit_test.v") + + ;; Check 1: check that the proof is valid and omit can be disabled + (message "1: check that the proof is valid and omit can be disabled") + (should (search-forward "automatic test marker 4" nil t)) + (forward-line -1) + ;; simulate C-u prefix argument + (proof-goto-point '(4)) + (wait-for-coq) + ;; Look into the *coq* buffer to find out whether the proof was + ;; processed fully without error. This is necessary for Coq >= 8.11. + ;; Coq < 8.11 prints a defined message, which ends up in *response*, + ;; for those versions it would be better to simply check the + ;; *response* buffer. However, consolidating all this is not easy, + ;; therefore I check the message in *coq* also for Coq < 8.11. + (with-current-buffer "*coq*" + ;; output *coq* content for debugging + ;; (message + ;; "*coq* content:\n%s" + ;; ;; (max 0 (- (point-max) 400)) + ;; (buffer-substring-no-properties (point-min) (point-max))) + + (goto-char (point-max)) + ;; goto second last prompt + (should (search-backward "</prompt>" nil t 2)) + ;; move behind prompt + (forward-char 9) + ;; There should be a Qed with no error or message after it + (should + (or + ;; for Coq 8.11 and later + (looking-at "Qed\\.\n\n<prompt>Coq <") + ;; for Coq 8.10 and earlier + ;; in 8.9 the message is on 1 line, in 8.10 on 3 + (looking-at "Qed\\.\n<infomsg>\n?classic_excluded_middle is defined")))) + + ;; Check 2: check proof-locked-face is active at marker 2 and 3 + (message "2: check proof-locked-face is active at marker 2 and 3") + (should (search-backward "automatic test marker 2" nil t)) + (should (eq (first-overlay-face) 'proof-locked-face)) + (should (search-forward "automatic test marker 3" nil t)) + (should (eq (first-overlay-face) 'proof-locked-face)) + + ;; Check 3: check that the second proof is omitted + (message "3: check that the second proof is omitted") + ;; first retract + (should (search-backward "automatic test marker 1" nil t)) + (proof-goto-point) + (wait-for-coq) + ;; move forward again + (should (search-forward "automatic test marker 4" nil t)) + (forward-line -1) + (proof-goto-point) + (wait-for-coq) + (with-current-buffer "*response*" + (goto-char (point-min)) + ;; There should be a declared message. + (should (looking-at "classic_excluded_middle is declared"))) + + ;; Check 4: check proof-omitted-proof-face is active at marker 3 + (message "4: check proof-omitted-proof-face is active at marker 3") + (should (search-backward "automatic test marker 3" nil t)) + ;; debug overlay order + ;; (mapc + ;; (lambda (ov) + ;; (message "OV %d-%d face %s" + ;; (overlay-start ov) (overlay-end ov) (overlay-get ov 'face))) + ;; (overlays-at-point-sorted)) + (should (eq (first-overlay-face) 'proof-omitted-proof-face)) + + ;; Check 5: check proof-locked-face is active at marker 1 and 2 + (message "5: check proof-locked-face is active at marker 1 and 2") + (should (search-backward "automatic test marker 1" nil t)) + (should (eq (first-overlay-face) 'proof-locked-face)) + (should (search-forward "automatic test marker 2" nil t)) + (should (eq (first-overlay-face) 'proof-locked-face))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index a517df71..8806774f 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1107,6 +1107,31 @@ It is used: (not (string-match "\\`Proof\\s-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" str)))))) +;; ----- regular expressions for the proof omit feature +;; see `proof-omit-proofs-configured' in generic/proof-config + +(defcustom coq-proof-start-regexp "^Proof\\(\\.\\| \\)" + "Value for `proof-script-proof-start-regexp'." + :type 'regexp + :group 'coq) + +(defcustom coq-proof-end-regexp "^\\(Qed\\|Admitted\\)\\." + "Value for `proof-script-proof-end-regexp'. +This is similar to `coq-save-command-regexp-strict' but slightly +different." + :type 'regexp + :group 'coq) + +(defcustom coq-definition-end-regexp "^\\(Defined\\|Abort\\)\\(\\.\\| \\)" + "Value for `proof-script-definition-end-regexp'." + :type 'regexp + :group 'coq) + +(defcustom coq-omit-proof-admit-command "Admitted." + "Value for `proof-script-proof-admit-command'." + :type 'string + :group 'coq) + ;; ----- keywords for font-lock. (defvar coq-keywords-kill-goal @@ -1979,6 +1979,14 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-tree-find-begin-of-unfinished-proof 'coq-find-begin-of-unfinished-proof) + ;; proof-omit-proofs config + (setq + proof-omit-proofs-configured t + proof-script-proof-start-regexp coq-proof-start-regexp + proof-script-proof-end-regexp coq-proof-end-regexp + proof-script-definition-end-regexp coq-definition-end-regexp + proof-script-proof-admit-command coq-omit-proof-admit-command) + (setq proof-cannot-reopen-processed-files nil) (proof-config-done) diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 025b4b07..74d576c1 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -648,6 +648,7 @@ the behaviour of script management. * Recognizing other elements:: * Configuring undo behaviour:: * Nested proofs:: +* Omitting proofs for speed:: * Safe (state-preserving) commands:: * Activate scripting hook:: * Automatic multiple files:: @@ -1137,6 +1138,97 @@ history. @end defvar +@node Omitting proofs for speed +@section Omitting proofs for speed + +In normal operation, the commands in an asserted region are sent +successively to the proof assistant. When the proof assistant +reports an error, processing stops. This ensures the consistency +of the development. Proof General supports omitting portions of +the asserted region to speed processing up at the cost of +consistency. Portions that can be potentially omitted are called +@emph{opaque proofs} in Proof General, because usually only +opaque proofs (in the sense of Coq) can be omitted without +risking to break the following code. This feature is also +described in the Proof General manual, @inforef{Script processing +commands, ,ProofGeneral} and @inforef{Omitting proofs for speed, +,ProofGeneral}. + +The omit proofs feature works in a simple, straightforward way: +After parsing the asserted region, Proof General uses regular +expressions to search for commands that start +(@code{proof-script-proof-start-regexp}) and end +(@code{proof-script-proof-end-regexp}) an opaque proof. If one is +found, the opaque proof is replaced with a cheating command +(@code{proof-script-proof-admit-command}). From this description +it is immediate, that the omit proof feature does only work if +proofs are not nested. If a nested proof is found, a warning is +displayed and omitting proofs stops at that location for the +currently asserted region. + +To enable the omit proofs feature, the following settings must be +configured. + +@c TEXI DOCSTRING MAGIC: proof-omit-proofs-configured +@defvar proof-omit-proofs-configured +t if the omit proofs feature has been configured by the proof assitant.@* +See also @samp{@code{proof-omit-proofs-option}} or the Proof General manual +for a description of the feature. This option can only be set, if +all of @samp{@code{proof-script-proof-start-regexp}}, +@samp{@code{proof-script-proof-end-regexp}}, +@samp{@code{proof-script-definition-end-regexp}} and +@samp{@code{proof-script-proof-admit-command}} have been configured. + +The omit proofs feature skips over opaque proofs in the source +code, admitting the theorems, to speed up processing. + +If @samp{@code{proof-omit-proofs-option}} is set by the user, all proof +commands in the source following a match of +@samp{@code{proof-script-proof-start-regexp}} up to and including the next +match of @samp{@code{proof-script-proof-end-regexp}}, are omitted (not send +to the proof assistant) and replaced by +@samp{@code{proof-script-proof-admit-command}}. If a match for +@samp{@code{proof-script-definition-end-regexp}} is found while searching +forward for the proof end, the current proof (up to and including +the match of @samp{@code{proof-script-definition-end-regexp}}) is considered +to be not opaque and not omitted, thus all these proof commands +_are_ sent to the proof assistant. + +The feature does not work for nested proofs. If a match for +@samp{@code{proof-script-proof-start-regexp}} is found before the next match +for @samp{@code{proof-script-proof-end-regexp}} or +@samp{@code{proof-script-definition-end-regexp}}, the search for opaque +proofs immediately stops and all commands following the previous +match of @samp{@code{proof-script-proof-start-regexp}} are sent verbatim to +the proof assistant. + +All the regular expressions for this feature are matched against +the commands inside proof action items, that is as strings, +without surrounding space. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-proof-start-regexp +@defvar proof-script-proof-start-regexp +Regular expression for the start of a proof for the omit proofs feature.@* +See @samp{@code{proof-omit-proofs-configured}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-proof-end-regexp +@defvar proof-script-proof-end-regexp +Regular expression for the end of an opaque proof for the omit proofs feature.@* +See @samp{@code{proof-omit-proofs-configured}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-definition-end-regexp +@defvar proof-script-definition-end-regexp +Regexp for the end of a non-opaque proof for the omit proofs feature.@* +See @samp{@code{proof-omit-proofs-configured}}. +@end defvar + +@c TEXI DOCSTRING MAGIC: proof-script-proof-admit-command +@defvar proof-script-proof-admit-command +Proof command to be inserted instead of omitted proofs. +@end defvar @node Safe (state-preserving) commands @section Safe (state-preserving) commands diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index beb5cc9f..bbd2515d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1495,6 +1495,42 @@ will stop exactly where the proof script fails, showing you the error message and the last processed command. So you can easily continue development from exactly the right place in the script. +In normal development, one often jumps into the middle or to the +end of some file, because this is the point, where a lemma must +be added or a definition must be fixed. Before starting the real +work, one needs to assert the file up to that point, usually with +@kbd{C-c C-RET} (@code{proof-goto-point}). Even for medium sized +files, asserting a big portion can take several seconds. There +are different ways to speed this process up. +@itemize @bullet +@item +One can split the development into smaller files. This works +quite well with Coq, automatic background compilation, +@ref{Automatic Compilation in Detail}, and the fast compilation +options, @ref{Quick and inconsistent compilation}. +@item +One can configure @code{proof-omit-proofs-option} to @code{t} to +omit complete opaque proofs when larger chunks are asserted. A +proof is opaque, if its proof script or proof term cannot +influence the following code. In Coq, opaque proofs are finished +with @code{Qed}, non-opaque ones with @code{Defined}. When this +omit proofs feature is configured, complete opaque proofs are +silently replace with a suitable cheating command +(@code{Admitted} for Coq) before sending the proof to the proof +assistant. For files with big proofs this can bring down the +processing time to 10% with the obvious disadvantage that errors +in the omitted proofs go unnoticed. For checking the proofs +occasionally, a prefix argument for @code{proof-goto-point} and +@code{proof-process-buffer} causes these commands to disregard +the setting of @code{proof-omit-proofs-option}. Currently, the +omit proofs feature is only supported for Coq. +@item +An often used poor man's solution is to collect all new material +at the end of one file, regardless where the material really +belongs. When the final theorem has been proved, one cleans up +the mess and moves all stuff where it really belongs. +@end itemize + Here is the full set of script processing commands. @c TEXI DOCSTRING MAGIC: proof-assert-next-command-interactive @@ -1522,15 +1558,19 @@ deleted text. @c TEXI DOCSTRING MAGIC: proof-goto-point -@deffn Command proof-goto-point +@deffn Command proof-goto-point &optional raw Assert or retract to the command at current position.@* Calls @samp{@code{proof-assert-until-point}} or @samp{@code{proof-retract-until-point}} as -appropriate. +appropriate. With prefix argument @var{raw} the omit proofs feature +(@samp{@code{proof-omit-proofs-option}}) is temporaily disabled to check all +proofs in the asserted region. @end deffn @c TEXI DOCSTRING MAGIC: proof-process-buffer -@deffn Command proof-process-buffer -Process the current (or script) buffer, and maybe move point to the end. +@deffn Command proof-process-buffer &optional raw +Process the current (or script) buffer, and maybe move point to the end.@* +With prefix argument @var{raw} the omit proofs feature (@samp{@code{proof-omit-proofs-option}}) +is temporaily disabled to check all proofs in the asserted region. @end deffn @c TEXI DOCSTRING MAGIC: proof-retract-buffer @@ -3636,6 +3676,21 @@ If non-nil, format for newlines after each command in a script. The default value is @code{t}. @end defopt +@c TEXI DOCSTRING MAGIC: proof-omit-proofs-option +@defvar proof-omit-proofs-option +Set to t to omit complete opaque proofs for speed reasons.@* +When t, complete opaque proofs in the asserted region are not +sent to the proof assistant (and thus not checked). For files +with big proofs this can drastically reduce the processing time +for the asserted region at the cost of not checking the proofs. +For partial and non-opaque proofs in the asserted region all +proof commands are sent to the proof assistant. + +Using a prefix argument for @samp{@code{proof-goto-point}} (M-x @code{proof-goto-point}) +or @samp{@code{proof-process-buffer}} (M-x @code{proof-process-buffer}) temporarily +disables omitting proofs. +@end defvar + @c TEXI DOCSTRING MAGIC: proof-prog-name-ask @defopt proof-prog-name-ask If non-nil, query user which program to run for the inferior process. @@ -4289,6 +4344,7 @@ assistant. It supports most of the generic features of Proof General. * Using the Coq project file:: * Proof using annotations:: * Multiple File Support:: +* Omitting proofs for speed:: * Editing multiple proofs:: * User-loaded tactics:: * Indentation tweaking:: @@ -5135,6 +5191,51 @@ General will perform some unnecessary compilations. @end itemize +@node Omitting proofs for speed +@section Omitting proofs for speed + +To speed up asserting larger chunks, Proof General can omit +complete opaque proofs by silently replacing the whole proof +script with @code{Admitted}, @ref{Script processing commands}. +This works when +@itemize +@item +proofs are not nested +@item +opaque and non-opaque proofs start with @code{Proof.} or +@code{Proof using} +@item +opaque proofs end with @code{Qed} or @code{Admitted} +@item +non-opaque proofs or definition end with @code{Defined} +@end itemize +Aborted proofs can be present if they start with a variant of +@code{Proof} and end with @code{Abort}. They are handled like +non-opaque proofs (i.e., not omitted). + +To enable omitting proofs, configure +@code{proof-omit-proofs-option} or select @code{Proof-General -> +Quick Options -> Processing -> Omit Proofs}. + +With a prefix argument, both @code{proof-goto-point} and +@code{proof-process-buffer} will temporarily disable the omit +proofs feature and send the full proof script to Coq. + +If a nested proof is detected while searching for opaque proofs +to omit, a warning is displayed and the complete remainder of the +asserted region is sent unmodified to Coq. + +If the proof script relies on sections, it is highly recommended to use +a @code{Proof using} annotation for all lemmas contained in a Section, +otherwise @code{Coq} will compute a wrong type for these lemmas when +this omitting-proofs feature is enabled. + +To automate this, we recall that ProofGeneral provides a dedicated +feature to generate these @code{Proof using} annotations (a defective +form being e.g. @code{Proof using Type} if no section hypothesis is +used), see the menu command @code{Coq > "Proof using" mode} and +@ref{Proof using annotations} for details. + @node Editing multiple proofs @section Editing multiple proofs diff --git a/generic/pg-user.el b/generic/pg-user.el index f10f02c1..005d919e 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -165,19 +165,24 @@ If called interactively, NUM is given by the prefix argument." ;; ;;;###autoload -(defun proof-goto-point () +(defun proof-goto-point (&optional raw) "Assert or retract to the command at current position. Calls `proof-assert-until-point' or `proof-retract-until-point' as -appropriate." - (interactive) - (save-excursion - (if (> (proof-queue-or-locked-end) (point)) - (proof-retract-until-point) - (if (proof-only-whitespace-to-locked-region-p) - (progn - (skip-chars-forward " \t\n") - (forward-char 1))) - (proof-assert-until-point)))) +appropriate. With prefix argument RAW the omit proofs feature +(`proof-omit-proofs-option') is temporaily disabled to check all +proofs in the asserted region." + (interactive "P") + (let ((proof-omit-proofs-option proof-omit-proofs-option)) + (when raw + (setq proof-omit-proofs-option nil)) + (save-excursion + (if (> (proof-queue-or-locked-end) (point)) + (proof-retract-until-point) + (if (proof-only-whitespace-to-locked-region-p) + (progn + (skip-chars-forward " \t\n") + (forward-char 1))) + (proof-assert-until-point))))) (defun proof-assert-next-command-interactive () "Process until the end of the next unprocessed command after point. @@ -198,18 +203,23 @@ If inside a comment, just process until the start of the comment." (proof-assert-until-point)) ;;;###autoload -(defun proof-process-buffer () - "Process the current (or script) buffer, and maybe move point to the end." - (interactive) - (proof-with-script-buffer - (save-excursion - (goto-char (point-max)) - (proof-assert-until-point-interactive)) - (proof-maybe-follow-locked-end)) - (when proof-fast-process-buffer - (message "Processing buffer...") - (proof-shell-wait) - (message "Processing buffer...done"))) +(defun proof-process-buffer (&optional raw) + "Process the current (or script) buffer, and maybe move point to the end. +With prefix argument RAW the omit proofs feature (`proof-omit-proofs-option') +is temporaily disabled to check all proofs in the asserted region." + (interactive "P") + (let ((proof-omit-proofs-option proof-omit-proofs-option)) + (when raw + (setq proof-omit-proofs-option nil)) + (proof-with-script-buffer + (save-excursion + (goto-char (point-max)) + (proof-assert-until-point-interactive)) + (proof-maybe-follow-locked-end)) + (when proof-fast-process-buffer + (message "Processing buffer...") + (proof-shell-wait) + (message "Processing buffer...done")))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; diff --git a/generic/proof-config.el b/generic/proof-config.el index 9632a268..951aade2 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -696,6 +696,70 @@ needed for Coq." :type 'boolean :group 'proof-script) +(defcustom proof-omit-proofs-configured nil + "t if the omit proofs feature has been configured by the proof assitant. +See also `proof-omit-proofs-option' or the Proof General manual +for a description of the feature. This option can only be set, if +all of `proof-script-proof-start-regexp', +`proof-script-proof-end-regexp', +`proof-script-definition-end-regexp' and +`proof-script-proof-admit-command' have been configured. + +The omit proofs feature skips over opaque proofs in the source +code, admitting the theorems, to speed up processing. + +If `proof-omit-proofs-option' is set by the user, all proof +commands in the source following a match of +`proof-script-proof-start-regexp' up to and including the next +match of `proof-script-proof-end-regexp', are omitted (not send +to the proof assistant) and replaced by +`proof-script-proof-admit-command'. If a match for +`proof-script-definition-end-regexp' is found while searching +forward for the proof end, the current proof (up to and including +the match of `proof-script-definition-end-regexp') is considered +to be not opaque and not omitted, thus all these proof commands +_are_ sent to the proof assistant. + +The feature does not work for nested proofs. If a match for +`proof-script-proof-start-regexp' is found before the next match +for `proof-script-proof-end-regexp' or +`proof-script-definition-end-regexp', the search for opaque +proofs immediately stops and all commands following the previous +match of `proof-script-proof-start-regexp' are sent verbatim to +the proof assistant. + +All the regular expressions for this feature are matched against +the commands inside proof action items, that is as strings, +without surrounding space." + :type 'boolean + :group 'proof-script) + +;; proof-omit-proofs-option is in proof-useropts as user option + +(defcustom proof-script-proof-start-regexp nil + "Regular expression for the start of a proof for the omit proofs feature. +See `proof-omit-proofs-configured'." + :type 'regexp + :group 'proof-script) + +(defcustom proof-script-proof-end-regexp nil + "Regular expression for the end of an opaque proof for the omit proofs feature. +See `proof-omit-proofs-configured'." + :type 'regexp + :group 'proof-script) + +(defcustom proof-script-definition-end-regexp nil + "Regexp for the end of a non-opaque proof for the omit proofs feature. +See `proof-omit-proofs-configured'." + :type 'regexp + :group 'proof-script) + +(defcustom proof-script-proof-admit-command nil + "Proof command to be inserted instead of omitted proofs." + :type 'string + :group 'proof-script) + + ;; ;; Proof script indentation ;; diff --git a/generic/proof-faces.el b/generic/proof-faces.el index 115d8667..b06a64fd 100644 --- a/generic/proof-faces.el +++ b/generic/proof-faces.el @@ -218,6 +218,13 @@ Warning messages can come from proof assistant or from Proof General itself." "Proof General face for highlighting an error in the proof script. " :group 'proof-faces) +(defface proof-omitted-proof-face + (proof-face-specs + (:background "#EAEFFF" :extend t) + (:background "#9C4A90" :extend t) + (:foreground "white" :background "black" :extend t)) + "*Face for background of omitted proofs" + :group 'proof-faces) ;;; Compatibility: these are required for use in GNU Emacs/font-lock-keywords diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 3846229e..e15ce4d5 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -334,6 +334,7 @@ without adjusting window layout." (proof-deftoggle proof-fast-process-buffer) (proof-deftoggle proof-imenu-enable proof-imenu-toggle) (proof-deftoggle proof-keep-response-history) +(proof-deftoggle proof-omit-proofs-option) (proof-eval-when-ready-for-assistant ;; togglers for settings separately configurable per-prover @@ -361,6 +362,11 @@ without adjusting window layout." ;;; :selected proof-keep-response-history] ("Processing" + ["Omit Proofs" proof-omit-proofs-option-toggle + :style toggle + :selected proof-omit-proofs-option + :active proof-omit-proofs-configured + :help "Skip over proofs, admitting theorems, when asserting larger chunks"] ["Fast Process Buffer" proof-fast-process-buffer-toggle :style toggle :selected proof-fast-process-buffer diff --git a/generic/proof-script.el b/generic/proof-script.el index 87a9975b..0c4a980d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1373,7 +1373,17 @@ With ARG, turn on scripting iff ARG is positive." (defun proof-done-advancing (span) "The callback function for `assert-until-point'. -Argument SPAN has just been processed." +Argument SPAN has just been processed. + +This is the callback for all the normal commands. Besides stuff +that is not yet documented here, this function +- extends the locked region +- creates additional spans (without 'type property) for help, + tooltips, color and menus +- merges spans with 'type as needed to achieve atomic undo for + proofs and sections +- enters some commands and their spans in some database (with for + me unknown purpose)" (let ((end (span-end span)) (cmd (span-property span 'cmd))) @@ -1406,6 +1416,8 @@ Argument SPAN has just been processed." ;; CASE 3: Proof completed one step or more ago, non-save ;; command seen, no nested goals allowed. ;; + ;; AFAICT case 3 is never taken for Coq. + ;; ;; We make a fake goal-save from any previous ;; goal to the command before the present one. ;; @@ -1463,11 +1475,23 @@ Argument SPAN has just been processed." (defun proof-done-advancing-save (span) - "A subroutine of `proof-done-advancing'. Add info for save span SPAN." + "Retire commands that close a proof or some other region. +This is a subroutine of `proof-done-advancing'. +Besides stuff that is not yet documented here, this function +- creates additional spans (without 'type property) for help, + tooltips, color and menus +- in particular, adds the background color for omitted proofs +- merges spans with 'type as needed to achieve atomic undo for + proofs and sections; for Coq this is done at least for proofs + and sections. +- enters some commands and their spans in some database (with for + me unknown purpose)" (unless (or (eq proof-shell-proof-completed 1) (eq proof-assistant-symbol 'isar)) ;; We expect saves to succeed only for recently completed top-level proofs. ;; NB: not true in Isar, because save commands can perform proof. + ;; Note: not true in Coq either, if there is a command (eg. a Check) + ;; between the tactic that finished the proof and the Qed. (proof-debug (format "PG: save command with proof-shell-proof-completed=%s, proof-nesting-depth=%s" @@ -1480,6 +1504,13 @@ Argument SPAN has just been processed." (savestart (span-start span)) (saveend (span-end span)) (cmd (span-property span 'cmd)) + ;; With the omit proofs feature (see + ;; `proof-omit-proofs-configured'), the span of the Admitted + ;; command that replaces the proof contains an + ;; 'omitted-proof-region property, that holds the start and + ;; end of the omitted proof for colouring. The property is + ;; only inserted for omitted proofs in the replacing Admitted. + (omitted-proof-region (span-property span 'omitted-proof-region)) lev nestedundos nam next) (and proof-save-with-hole-regexp @@ -1546,6 +1577,20 @@ Argument SPAN has just been processed." (proof-make-goalsave gspan (span-end gspan) savestart saveend nam nestedundos) + ;; In case SPAN (which is retired now) belongs to an admit + ;; command that closes an omitted proof: create an additional + ;; span for the different background color of the omitted span. + ;; Start and end point of this span has been computed before in + ;; `proof-script-omit-proofs'. This background color span is + ;; registered in the span of the goal command for the only + ;; reason to not leave it dangling around. + (when omitted-proof-region + (let ((omit-span (span-make (car omitted-proof-region) + (cadr omitted-proof-region)))) + (span-set-property omit-span 'face 'proof-omitted-proof-face) + (span-set-property omit-span 'omitted-proof-span t) + (span-set-property gspan 'omit-color-span omit-span))) + ;; *** Theorem dependencies *** (if proof-last-theorem-dependencies (proof-depends-process-dependencies nam gspan))))) @@ -1933,6 +1978,144 @@ Assumes that point is at the end of a command." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; +;; Omit proofs feature. +;; +;; See `proof-omit-proofs-configured' for the feature. When the parsed +;; buffer content has been converted to vanilla spans, +;; `proof-script-omit-proofs' searches for complete opaque proofs in +;; there and replaces them with `proof-script-proof-admit-command'. + +(defun proof-move-over-whitespace-to-next-line (pos) + "Return position of next line if one needs only to jump over white space. +Utility function. In the current buffer, check if beginning of +next line can be reached from POS by moving over white +space (spaces, tabs) only. If yes return the beginning of next +line, otherwise POS." + (save-excursion + (goto-char pos) + (skip-chars-forward " \t") + (setq pos (point)) + (if (eolp) + (1+ (point)) + pos))) + +(defun proof-script-omit-proofs (vanillas) + "Return a copy of VANILLAS with complete opaque proofs omitted. +See `proof-omit-proofs-configured' for the description of the +omit proofs feature. This function uses +`proof-script-proof-start-regexp', +`proof-script-proof-end-regexp' and +`proof-script-definition-end-regexp' to search for complete +opaque proofs in the action list VANILLAS. Complete opaque proofs +are replaced by `proof-script-proof-admit-command'. The span of +the admit command contains an 'omitted-proof-region property with +the region of the omitted proof. This is used in +`proof-done-advancing-save' to colour the omitted proof with +`proof-omitted-proof-face'. + +Report an error to the (probably surprised) user if another proof +start is found inside a proof." + (cl-assert + (and proof-omit-proofs-configured proof-script-proof-start-regexp + proof-script-proof-end-regexp proof-script-definition-end-regexp + proof-script-proof-admit-command) + nil + "proof-script omit proof feature not properly configured") + (let (result maybe-result inside-proof + proof-start-span-start proof-start-span-end + item cmd) + (while vanillas + (setq item (car vanillas)) + ;; cdr vanillas is at the end of the loop + (setq cmd (mapconcat 'identity (nth 1 item) " ")) + (if inside-proof + (progn + (if (string-match proof-script-proof-start-regexp cmd) + ;; found another proof start inside a proof + ;; stop omitting and pass the remainder unmodified + ;; the result in `result' is aggregated in reverse + ;; order, need to reverse vanillas + (progn + (setq result (nconc (nreverse vanillas) maybe-result result)) + (setq maybe-result nil) + (setq vanillas nil) + ;; for Coq nobody will notice the warning, because + ;; the error about nested proofs will pop up shortly + ;; afterwards + (display-warning + '(proof-script) + ;; use the end of the span, because the start is + ;; usually on the preceding line + (format (concat "found second proof start at line %d" + " - are there nested proofs?") + (line-number-at-pos (span-end (car item)))))) + (if (string-match proof-script-proof-end-regexp cmd) + (let + ;; Reuse the Qed span for the whole proof, + ;; including the faked Admitted command. + ;; `proof-done-advancing' expects such a span. + ((cmd-span (car item))) + (span-set-property cmd-span 'type 'omitted-proof) + (span-set-property cmd-span + 'cmd proof-script-proof-admit-command) + (span-set-endpoints cmd-span proof-start-span-end + (span-end (car item))) + ;; Throw away all commands between start of proof + ;; and the current point, in particular, delete + ;; all the spans. + (mapc + (lambda (item) (span-detach (car item))) + maybe-result) + (setq maybe-result nil) + ;; Record start and end point for the fancy + ;; colored span that marks the skipped proof. The + ;; span will be created in + ;; `proof-done-advancing-save' when + ;; `proof-script-proof-admit-command' is retired. + (span-set-property + cmd-span 'omitted-proof-region + ;; for the start take proper line start if possible + (list (proof-move-over-whitespace-to-next-line + proof-start-span-start) + ;; For the end, don't extend to the end of + ;; the line, because then the fancy color + ;; span is behind the end of the proof span + ;; and will get deleted when undoing just + ;; behind that proof. + (span-end (car item)))) + (push (list cmd-span + (list proof-script-proof-admit-command) + 'proof-done-advancing nil) + result) + (setq inside-proof nil)) + (if (string-match proof-script-definition-end-regexp cmd) + ;; A proof ending in Defined or something similar. + ;; Need to keep all commands from the start of the proof. + (progn + (setq result (cons item (nconc maybe-result result))) + (setq maybe-result nil) + (setq inside-proof nil)) + ;; normal proof command - maybe it belongs to a + ;; Defined, keep it separate, until we know. + (push item maybe-result))))) + ;; outside proof + (if (string-match proof-script-proof-start-regexp cmd) + (progn + (setq maybe-result nil) + ;; Keep the Proof using command in any case. + (push item result) + (setq proof-start-span-start (span-start (car item))) + (setq proof-start-span-end (span-end (car item))) + (setq inside-proof t)) + ;; outside, no proof start - keep it unmodified + (push item result))) + (setq vanillas (cdr vanillas))) + (nreverse (nconc maybe-result result)))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; Assert-until-point. ;; ;; This function parses some region of the script buffer into @@ -2005,12 +2188,16 @@ SEMIS must be a non-empty list, in reverse order (last position first). We assume that the list is contiguous and begins at (proof-queue-or-locked-end). We also delete help spans which appear in the same region (in the expectation that these may be overwritten). -This function expects the buffer to be activated for advancing." +This function expects the buffer to be activated for advancing. +If the omit proofs feature is active, complete opaque proofs will +be omitted from the vanilla action list obtained from SEMIS." (cl-assert semis nil "proof-assert-semis: argument must be a list") (let ((startpos (proof-queue-or-locked-end)) (lastpos (nth 2 (car semis))) (vanillas (proof-semis-to-vanillas semis displayflags))) (proof-script-delete-secondary-spans startpos lastpos) + (when (and proof-omit-proofs-option proof-omit-proofs-configured) + (setq vanillas (proof-script-omit-proofs vanillas))) (proof-extend-queue lastpos vanillas))) (defun proof-retract-before-change (beg end) diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index 4ce51c99..1432776f 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -99,6 +99,21 @@ be inserted as the user types commands to the prover." :set 'proof-set-value :group 'proof-user-options) +(defcustom proof-omit-proofs-option nil + "Set to t to omit complete opaque proofs for speed reasons. +When t, complete opaque proofs in the asserted region are not +sent to the proof assistant (and thus not checked). For files +with big proofs this can drastically reduce the processing time +for the asserted region at the cost of not checking the proofs. +For partial and non-opaque proofs in the asserted region all +proof commands are sent to the proof assistant. + +Using a prefix argument for `proof-goto-point' (\\[proof-goto-point]) +or `proof-process-buffer' (\\[proof-process-buffer]) temporarily +disables omitting proofs." + :type 'boolean + :group 'proof-user-options) + (defcustom pg-show-hints t "*Whether to display keyboard hints in the minibuffer." :type 'boolean |