document the omit proofs feature manual and changes file

2 files changed, 90 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index c10cec85..e1f63e82 100644
--- a/CHANGES
+++ b/CHANGES
@@ -151,6 +151,13 @@ 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  
+
 *** bug fixes
     - avoid leaving partial files behind when compilation fails
     - 123: Parallel background compliation fails to execute some
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 49275d64..c8f0c4c7 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
@@ -3640,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.
@@ -4293,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::
@@ -5139,6 +5191,37 @@ 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.
+
+
 @node Editing multiple proofs
 @section Editing multiple proofs