branch: elpa/proof-general
commit 0e0170f96f5feaeefe59052a08373080acc20393
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
proof-stat: admitted proofs count as failing
Change `proof-check-chunks' such that Admitted proofs are reported as
failing.
---
ci/simple-tests/proof_stat.human.exp-out | 4 ++--
ci/simple-tests/proof_stat.tap.exp-out | 2 +-
ci/simple-tests/proof_stat.v | 2 +-
coq/coq-syntax.el | 6 ++++++
coq/coq.el | 3 ++-
doc/PG-adapting.texi | 20 +++++++++++++++++---
doc/ProofGeneral.texi | 20 ++++++++++++--------
generic/pg-user.el | 21 +++++++++++++++++----
generic/proof-config.el | 11 +++++++++++
9 files changed, 69 insertions(+), 20 deletions(-)
diff --git a/ci/simple-tests/proof_stat.human.exp-out
b/ci/simple-tests/proof_stat.human.exp-out
index 901c8b3820..472312ed81 100644
--- a/ci/simple-tests/proof_stat.human.exp-out
+++ b/ci/simple-tests/proof_stat.human.exp-out
@@ -1,10 +1,10 @@
Proof check results for proof_stat.v
-4 opaque proofs recognized: 2 successful 2 FAILING
+4 opaque proofs recognized: 1 successful 3 FAILING
FAIL a1_equal_4
OK b_equal_6
FAIL b2_equal_6
- OK use_admit
+ FAIL use_admit
diff --git a/ci/simple-tests/proof_stat.tap.exp-out
b/ci/simple-tests/proof_stat.tap.exp-out
index 1735d29f79..86bd533bac 100644
--- a/ci/simple-tests/proof_stat.tap.exp-out
+++ b/ci/simple-tests/proof_stat.tap.exp-out
@@ -3,6 +3,6 @@ TAP version 13
not ok 1 a1_equal_4
ok 2 b_equal_6
not ok 3 b2_equal_6
-ok 4 use_admit
+not ok 4 use_admit
diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
index 415b18bc2d..ffdccda668 100644
--- a/ci/simple-tests/proof_stat.v
+++ b/ci/simple-tests/proof_stat.v
@@ -22,7 +22,7 @@ Lemma b2_equal_6 : b = 2 * 3.
(* FAIL *)
Proof using. (* this proof should fail *)
Qed.
-Lemma use_admit : 0 = 1.
+Lemma use_admit : 0 = 1. (* FAIL *)
Proof using. (* this proof succeeds but should count as failing
*)
admit.
Admitted.
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e68bb8f88d..fbb5398f90 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1136,6 +1136,12 @@ different."
:type 'string
:group 'coq)
+(defcustom coq-omit-cheating-regexp "Admitted"
+ "Value for `proof-omit-cheating-regexp'.
+Very similar to `coq-omit-proof-admit-command', but without the dot."
+ :type 'regexp
+ :group 'coq)
+
;; ----- keywords for font-lock.
(defvar coq-keywords-kill-goal
diff --git a/coq/coq.el b/coq/coq.el
index 4d4b5a33ec..fdafe2dd43 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1964,7 +1964,8 @@ at `proof-assistant-settings-cmds' evaluation time.")
proof-script-definition-end-regexp coq-definition-end-regexp
proof-script-proof-admit-command coq-omit-proof-admit-command
proof-script-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission
- proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept)
+ proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept
+ proof-omit-cheating-regexp coq-omit-cheating-regexp)
;; proof-check-report/proof-check-annotate config
(setq
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index d63478a387..865a3083df 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1289,9 +1289,12 @@ The other material is asserted in the usual way and
opaque proofs it first tries to assert them in the usual way too. If
this succeeds the proof is considered valid. Otherwise the proof is
replaced with @code{proof-script-proof-admit-command} and the proof is
-considered invalid. To associate theorem names with opaque proofs, the
-function @code{proof-get-proof-info-fn} is called, which is identical
-to @code{proof-tree-get-proof-info}, @xref{Proof Tree Elisp
+considered invalid. In order to consider Admitted proofs as invalid
+ones, proofs whose last command matches
+@code{proof-omit-cheating-regexp} count as invalid. To associate
+theorem names with opaque proofs, the function
+@code{proof-get-proof-info-fn} is called, which is identical to
+@code{proof-tree-get-proof-info}, @xref{Proof Tree Elisp
configuration}.
To enable proof status statistics, the omit-proofs feature must be
@@ -1328,6 +1331,17 @@ This function takes a state as argument as returned by
the proof assistant back to the same state.
@end defvar
+@c TEXI DOCSTRING MAGIC: proof-omit-cheating-regexp
+@defvar proof-omit-cheating-regexp
+Regular expression matching proof closing commands for incomplete proofs.@*
+If set, this regular expression is applied to the last command of
+opaque proofs. If it matches the proofs counts as invalid for the
+proof-status statistics and annotation feature. For Coq this is
+used to mark Admitted proofs as invalid.
+
+This option can be left at @samp{nil}.
+@end defvar
+
@node Safe (state-preserving) commands
@section Safe (state-preserving) commands
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index e5aaeb23d3..acaed36176 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2267,7 +2267,8 @@ in the current buffer, i.e., it generates an overview
that shows which
of the opaque proofs in the current buffer are currently valid and
which are failing. When used interactively, the proof status is shown
in the buffer @code{*proof-check-report*} (as long as
-@code{proof-check-report-buffer} is not changed).
+@code{proof-check-report-buffer} is not changed). Note that incomplete
+proofs, i.e., Admitted proofs for Coq, count as invalid.
The command @code{proof-check-annotate} (menu @code{Proof-General ->
Annotate Failing Proofs}) modifies the current buffer and places
@@ -2285,7 +2286,10 @@ only work for Coq.
Generate an overview about valid and invalid proofs.@*
This command completely processes the current buffer and
generates an overview about all the opaque proofs in it and
-whether their proof scripts are valid or invalid.
+whether their proof scripts are valid or invalid. Note that
+proofs closed with a cheating command (see
+@samp{@code{proof-omit-cheating-regexp}}), i.e., Admitted for Coq, count as
+invalid.
This command makes sense for a development process where invalid
proofs are permitted and vos compilation and the omit proofs
@@ -5318,12 +5322,12 @@ The command @code{proof-check-report} (menu
@code{Proof-General ->
Check Opaque Proofs}) generates the proof status of all opaque proofs
in the current buffer, i.e., it generates an overview that shows which
of the opaque proofs in the current buffer are currently valid and
-which are failing. This command is useful for a development process
-where invalid proofs are permitted and vos compilation (@xref{Quick
-and inconsistent compilation}) and the omit proofs feature
-(@xref{Omitting proofs for speed}) are used to work at the most
-interesting or challenging point instead of on the first invalid
-proof.
+which are failing, where Admitted proofs count as failing. This
+command is useful for a development process where invalid proofs are
+permitted and vos compilation (@xref{Quick and inconsistent
+compilation}) and the omit proofs feature (@xref{Omitting proofs for
+speed}) are used to work at the most interesting or challenging point
+instead of on the first invalid proof.
The command @code{proof-check-annotate} (menu @code{Proof-General ->
Annotate Failing Proofs}) can then be used to consistently annotate
diff --git a/generic/pg-user.el b/generic/pg-user.el
index ed86fc062b..07ff560fba 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -735,7 +735,9 @@ errors are silently replaced by
`proof-script-proof-admit-command'. The result is a list of proof
status results, one for each 'proof chunk in the same order. Each
proof-status result is a list of 4 elements as follows.
-- 1st: proof status as `t' or `nil'.
+- 1st: proof status as `t' or `nil'. Proofs closed with a match
+ of `proof-omit-cheating-regexp', if defined, count as failing,
+ i.e., their status is `nil'.
- 2nd: the name of the proof as reported by
`proof-get-proof-info-fn'.
- 3rd: Position of the start of the span containing the theorem
@@ -762,7 +764,8 @@ proof-status result is a list of 4 elements as follows.
(nth 2 last-item)
(cons 'empty-action-list (nth 3 last-item))))
(vanillas-rev-updated (cons new-last-item (cdr vanillas-rev)))
- error)
+ error
+ cheated)
;; if this is a proof chunk the next must be no-proof or must not exist
(cl-assert (or (not (eq this-mode 'proof))
(or (eq next-mode 'no-proof) (eq next-mode nil)))
@@ -813,8 +816,15 @@ proof-status result is a list of 4 elements as follows.
(proof-set-locked-end last-span-end)
(cl-assert (not (cadr (funcall proof-get-proof-info-fn)))
nil "proof-check: still in proof after admitting"))
+ (when (and proof-omit-cheating-regexp
+ ;; check if somebody cheated - cheated proofs
+ ;; should count as failing
+ (proof-string-match
+ proof-omit-cheating-regexp
+ (mapconcat #'identity (nth 1 last-item) " ")))
+ (setq cheated t))
(push
- (cons (not error)
+ (cons (not (or error cheated))
(cons (cadr current-proof-state-and-name) proof-start-points))
proof-results)))
@@ -863,7 +873,10 @@ This function does not (re-)compile required files."
"Generate an overview about valid and invalid proofs.
This command completely processes the current buffer and
generates an overview about all the opaque proofs in it and
-whether their proof scripts are valid or invalid.
+whether their proof scripts are valid or invalid. Note that
+proofs closed with a cheating command (see
+`proof-omit-cheating-regexp'), i.e., Admitted for Coq, count as
+invalid.
This command makes sense for a development process where invalid
proofs are permitted and vos compilation and the omit proofs
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1c5ede8071..aa79b85c44 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -738,6 +738,17 @@ without surrounding space."
:type 'boolean
:group 'proof-script)
+(defcustom proof-omit-cheating-regexp nil
+ "Regular expression matching proof closing commands for incomplete proofs.
+If set, this regular expression is applied to the last command of
+opaque proofs. If it matches the proofs counts as invalid for the
+proof-status statistics and annotation feature. For Coq this is
+used to mark Admitted proofs as invalid.
+
+This option can be left at `nil'."
+ :type 'regexp
+ :group 'proof-script)
+
;; proof-omit-proofs-option is in proof-useropts as user option
(defcustom proof-script-proof-start-regexp nil
