\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Asynchronous and Parallel Proof Processing

Author:

  Enrico Tassi

This chapter explains how proofs can be asynchronously processed by Rocq. This feature improves the reactivity of the system when used in interactive mode via RocqIDE. In addition, it allows Rocq to take advantage of parallel hardware when used as a batch compiler by decoupling the checking of statements and definitions from the construction and checking of proofs objects.

This feature is designed to help dealing with huge libraries of theorems characterized by long proofs. In the current state, it may not be beneficial on small sets of short files.

This feature has some technical limitations that may make it unsuitable for some use cases.

For example, in interactive mode, some errors coming from the kernel of Rocq are signaled late. The type of errors belonging to this category are universe inconsistencies.

At the time of writing, only opaque proofs (ending with `Qed` or `Admitted`) can be processed asynchronously.

Finally, asynchronous processing is disabled when running RocqIDE in Windows. The current implementation of the feature is not stable on Windows. It can be enabled, as described below at Interactive mode, though doing so is not recommended.

## Proof annotations

To process a proof asynchronously Rocq needs to know the precise statement of the theorem without looking at the proof. This requires some annotations if the theorem is proved inside a Section (see Section Sections).

When a section ends, Rocq looks at the proof object to decide which section variables are actually used and hence have to be quantified in the statement of the theorem. To avoid making the construction of proofs mandatory when ending a section, one can start each proof with the `Proof using` command (Section Entering and exiting proof mode) that declares which section variables the theorem uses.

The presence of `Proof using` is needed to process proofs asynchronously in interactive mode.

It is not strictly mandatory in batch mode if it is not the first time the file is compiled and if the file itself did not change. When the proof does not begin with `Proof using`, the system records in an auxiliary file, produced along with the `.vo` file, the list of section variables used.

If a theorem has an incorrect annotation that omits a needed variable, you may see a message like this:

>     File "./Pff.v", line 2372, characters 0-4:
>     Error: The following section variable is used but not declared:
>     precisionNotZero.

>     You can either update your proof to not depend on precisionNotZero, or you can
>     update your Proof line from
>     Proof using FtoRradix b pGivesBound precision radix radixMoreThanOne radixMoreThanZERO
>     to
>     Proof using FtoRradix b pGivesBound precision precisionNotZero radix radixMoreThanOne radixMoreThanZERO

In this case the minimal annotation suggested by the `Suggest Proof Using` flag is `Print Using pGivesBound precisionNotZero radixMoreThanOne.` The other variables in the suggestion are unnecessary because they will be transitively included from the minimal annotation.

Alternatively, if the `Proof using` included unneeded variables, they become extra parameters of the theorem, which may generate errors. This example shows an example of an unneeded variable. One possible error is `(in proof <theorem name>) Attempt to save an incomplete proof`, which may indicate that the named theorem refers to an earlier theorem that has an incorrect annotation.

### Automatic suggestion of proof annotations

The `Suggest Proof Using` flag makes Rocq suggest, when a `Qed` command is processed, a correct proof annotation. It is up to the user to modify the proof script accordingly.

## Proof blocks and error resilience

In interactive mode Rocq is able to completely check a document containing errors instead of bailing out at the first failure.

Two kind of errors are handled: errors occurring in commands and errors occurring in proofs.

To properly recover from a failing tactic, Rocq 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). Rocq comes with four kind of proof blocks, and an ML API to add new ones.

curly:

  blocks are delimited by { and }, see Chapter Proof mode

par:

  blocks are atomic, i.e. just one tactic introduced by the `par:` goal selector

indent:

  blocks end with a tactic indented less than the previous one

bullet:

  blocks are delimited by two equal bullet signs at the same indentation level

### Caveats

When a command fails the subsequent error messages may be bogus, i.e. caused by the first error. Error resilience for commands can be switched off by passing `-async-proofs-command-error-resilience off` to RocqIDE.

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 resilience can be turned off or selectively activated for any set of block kind passing to RocqIDE one of the following options:

- `-async-proofs-tactic-error-resilience off`

- `-async-proofs-tactic-error-resilience all`

- `-async-proofs-tactic-error-resilience` `blocktype*,`

Valid proof block types are: “curly”, “par”, “indent”, and “bullet”.

## Interactive mode

RocqIDE and VsCoq support asynchronous proof processing.

When RocqIDE is started and async mode is enabled, two or more Rocq processes are created. The master one follows the user, giving feedback as soon as possible by skipping proofs, which are delegated to the worker processes. The worker processes asynchronously processes the proofs. The Jobs panel in the main RocqIDE window shows the status of each worker process. If a proof contains an error, it's reported in red in the label of the very same button, that can also be used to see the list of errors and jump to the corresponding line.

If a proof is processed asynchronously the corresponding `Qed` command is colored using a lighter color than usual. This signals that the proof has been delegated to a worker process (or will be processed lazily if the `-async-proofs lazy` option is used). Once finished, the worker process will provide the proof object, but this will not be automatically checked by the kernel of the main process. To force the kernel to check all the proof objects, one has to click the button with the gears (Fully check the document) on the top bar. Only then all the universe constraints are checked.

## Limiting the number of parallel workers

Many Coq processes may run on the same computer, and each of them may start many additional worker processes. The `rocq workmgr` utility lets one limit the number of workers, globally.

The utility accepts the `-j` argument to specify the maximum number of workers (defaults to 2). `rocq workmgr` automatically starts in the background and prints an environment variable assignment like `ROCQWORKMGR_SOCKET=localhost:45634`. The user must set this variable in all the shells from which Rocq processes will be started. If one uses just one terminal running the bash shell, then `export $(rocq workmgr -j 4)` will do the job.

After that, all Coq processes, e.g. `rocqide` and `rocq compile`, will honor the limit, globally.

### Caveats

The number of worker processes can be increased by passing RocqIDE the `-async-proofs-j n` flag. Note that the memory consumption increases too, since each worker requires the same amount of memory as the master process. Also note that increasing the number of workers may reduce the reactivity of the master process to user commands.

To disable this feature, one can pass the `-async-proofs off` flag to RocqIDE. Conversely, on Windows, where the feature is disabled by default, pass the `-async-proofs on` flag to enable it.

Proofs that are known to take little time to process are not delegated to a worker process. The threshold can be configured with `-async-proofs-delegation-threshold`. Default is 0.03 seconds.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF