diff options
| -rw-r--r-- | doc/refman/AsyncProofs.tex | 37 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 5 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 2 |
5 files changed, 44 insertions, 4 deletions
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 7cf500400..ebd11c168 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -46,6 +46,43 @@ proof does not begin with \texttt{Proof using}, the system records in an auxiliary file, produced along with the \texttt{.vo} file, the list of section variables used. +\section{Proof blocks and error resilience} + +Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq +is able to completely check a document containing errors instead of bailing +out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular commands and +errors occurring in proofs. + +To properly recover from a failing tactic, Coq needs to recognize the structure of +the proof in order to confine the error to a sub proof. Proof block detection +is performed by looking at the syntax of the proof script (i.e. also looking at indentation). +Coq comes with four kind of proof blocks, and an ML API to add new ones. + +\begin{description} +\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling} +\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector +\item[indent] blocks end with a tactic indented less than the previous one +\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level +\end{description} + +\subsection{Caveats} + +When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by +the first error. Error resiliency for vernacular commands can be switched off passing +\texttt{-async-proofs-command-error-resilience off} to CoqIDE. + +An incorrect proof block detection can result into an incorrect error recovery and +hence in bogus errors. Proof block detection cannot be precise for bullets or +any other non well parenthesized proof structure. Error resiliency can be +turned off or selectively activated for any set of block kind passing to +CoqIDE one of the following options: +\texttt{-async-proofs-tactic-error-resilience off}, +\texttt{-async-proofs-tactic-error-resilience all}, +\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. +Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. + \subsubsection{Automatic suggestion of proof annotations} The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a diff --git a/lib/flags.ml b/lib/flags.ml index e78fa7c0c..16996c144 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -69,7 +69,7 @@ let priority_of_string = function | "high" -> High | _ -> raise (Invalid_argument "priority_of_string") type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "proof-block" ]) +let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ]) let async_proofs_cmd_error_resilience = ref true let async_proofs_is_worker () = diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index ed8553d4b..ce12185cb 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -127,7 +127,7 @@ let dynamic_curly_brace { dynamic_switch = id } = | `Not -> `Leaks let () = register_proof_block_delimiter - "proof-block" static_curly_brace dynamic_curly_brace + "curly" static_curly_brace dynamic_curly_brace (* ***************** par: ************************************************* *) diff --git a/stm/stm.ml b/stm/stm.ml index 3ac1f9892..75d2e070a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -238,7 +238,10 @@ let default_info () = module DynBlockData : Dyn.S = Dyn.Make(struct end) (* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose - * no constraint on properties, here we impose boxes to be non overlapping. *) + * no constraint on properties, here we impose boxes to be non overlapping. + * Such invariant makes sense for the current kinds of boxes (proof blocks and + * entire proofs) but may make no sense and dropped/refined in the future. + * Such invariant is useful to detect broken proof block detection code *) type box = | ProofTask of pt | ProofBlock of static_block_declaration * proof_block_name diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 11e973bf5..a602d6b8a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -119,7 +119,7 @@ let rec classify_vernac e = VtLater | VernacEndSubproof -> VtProofStep { parallel = false; - proof_block_detection = Some "proof-block" }, + proof_block_detection = Some "curly" }, VtLater (* Options changing parser *) | VernacUnsetOption (["Default";"Proof";"Using"]) |