diff options
| author | Hendrik Tews | 2021-03-14 23:07:37 +0100 |
|---|---|---|
| committer | Hendrik Tews | 2021-04-16 22:53:05 +0200 |
| commit | e454ae013827b98b814c99ffbc1ca7f2525fb030 (patch) | |
| tree | e4df56200641e8c235a180aa86bb68392c7e1f45 /coq | |
| parent | f0f0476d07401aba2cf428a71f7ee960cd1b3154 (diff) | |
add feature to omit complete opaque proofs
This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.
With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.
To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 25 | ||||
| -rw-r--r-- | coq/coq.el | 8 |
2 files changed, 33 insertions, 0 deletions
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) |