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 /generic/proof-useropts.el | |
| 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 'generic/proof-useropts.el')
| -rw-r--r-- | generic/proof-useropts.el | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index 4ce51c99..d5df0404 100644 --- a/generic/proof-useropts.el +++ b/generic/proof-useropts.el @@ -99,6 +99,17 @@ 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." + :type 'boolean + :group 'proof-user-options) + (defcustom pg-show-hints t "*Whether to display keyboard hints in the minibuffer." :type 'boolean |