1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
\achapter{Asynchronous and Parallel Proof Processing}
\aauthor{Enrico Tassi}
\label{pralitp}
\index{Asynchronous and Parallel Proof Processing!presentation}
This chapter explains how proofs can be asynchronously processed by Coq.
This feature improves the reactiveness of the system when used in interactive
mode via CoqIDE. In addition to that, it allows Coq 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, errors coming from the kernel of Coq are
signaled late. The most notable type of errors belonging to this category are
universe inconsistencies or unsatisfied guardedness conditions for fixpoints
built using tactics.
Last, at the time of writing, only opaque proofs (ending with \texttt{Qed}) can be
processed asynchronously.
\subsection{Proof annotations}
To process a proof asynchronously Coq 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 \texttt{Section} (see Section~\ref{Section}).
When a section ends, Coq 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
\texttt{Proof using} command (Section~\ref{ProofUsing}) that declares which
section variables the theorem uses.
The presence of \texttt{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 \texttt{Proof using}, the system records in an
auxiliary file, produced along with the \texttt{.vo} file, the list of
section variables used.
\subsubsection{Automatic suggestion of proof annotations}
The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a
\texttt{Qed} command is processed, a correct proof annotation. It is up
to the user to modify the proof script accordingly.
\subsection{Interactive mode}
At the time of writing the only user interface supporting asynchronous proof
processing is CoqIDE.
When CoqIDE is started, two Coq processes are created. The master one follows
the user, giving feedback as soon as possible by skipping proofs, which are
delegated to the worker process. The worker process, whose state can be seen
by clicking on the button in the lower right corner of the main CoqIDE window,
asynchronously processes the proofs. If a proof contains an error, it is
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 \texttt{Qed} command
is colored using a lighter color that usual. This signals that
the proof has been delegated to a worker process (or will be processed
lazily if the \texttt{-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. Only then are all the universe constraints checked.
\subsubsection{Caveats}
The number of worker processes can be increased by passing CoqIDE the
\texttt{-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 \texttt{-async-proofs off} flag to
CoqIDE.
\subsection{Batch mode}
When Coq is used as a batch compiler by running \texttt{coqc} or
\texttt{coqtop -compile}, it produces a \texttt{.vo} file for each
\texttt{.v} file. A \texttt{.vo} file contains, among other things,
theorems statements and proofs. Hence to produce a \texttt{.vo} Coq need
to process all the proofs of the \texttt{.v} file.
The asynchronous processing of proofs can decouple the generation of a
compiled file (like the \texttt{.vo} one) that can be loaded by
\texttt{Require} from the generation and checking of the proof objects.
The \texttt{-quick} flag can be passed to \texttt{coqc} or
\texttt{coqtop} to produce, quickly, \texttt{.vio} files. Alternatively,
when using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the
\texttt{quick} target can be used to compile all files using the
\texttt{-quick} flag.
A \texttt{.vio} file can be loaded using \texttt{Require} exactly as a
\texttt{.vo} file but proofs will not be available (the \texttt{Print}
command produces an error). Moreover, some universe constraints might be
missing, so universes inconsistencies might go unnoticed. A
\texttt{.vio} file does not contain proof objects, but proof tasks,
i.e. what a worker process can transform into a proof object.
Compiling a set of files with the \texttt{-quick} flag allows one to work,
interactively, on any file without waiting for all the proofs to be checked.
When working interactively, one can fully check all the \texttt{.v} files by
running \texttt{coqc} as usual.
Alternatively one can turn each \texttt{.vio} into the corresponding
\texttt{.vo}. All \texttt{.vio} files can be processed in parallel,
hence this alternative might be faster. The command \texttt{coqtop
-schedule-vio2vo 2 a b c} can be used to obtain a good scheduling for 2
workers to produce \texttt{a.vo}, \texttt{b.vo}, and \texttt{c.vo}. When
using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the
\texttt{vio2vo} target can be used for that purpose. Variable \texttt{J}
should be set to the number of workers, e.g. \texttt{make vio2vo J=2}.
The only caveat is that, while the \texttt{.vo} files obtained from
\texttt{.vio} files are complete (they contain all proof terms and
universe constraints), the satisfiability of all universe constraints has
not been checked globally (they are checked to be consistent for every
single proof). Constraints will be checked when these \texttt{.vo} files
are (recursively) loaded with \texttt{Require}.
There is an extra, possibly even faster, alternative: just check the
proof tasks stored in \texttt{.vio} files without producing the
\texttt{.vo} files. This is possibly faster because all the proof tasks
are independent, hence one can further partition the job to be done
between workers. The \texttt{coqtop -schedule-vio-checking 6 a b c}
command can be used to obtain a good scheduling for 6 workers to check
all the proof tasks of \texttt{a.vio}, \texttt{b.vio}, and
\texttt{c.vio}. Auxiliary files are used to predict how long a proof task
will take, assuming it will take the same amount of time it took last
time. When using a \texttt{Makefile} produced by \texttt{coq\_makefile},
the \texttt{checkproofs} target can be used to check all \texttt{.vio}
files. Variable \texttt{J} should be set to the number of workers,
e.g. \texttt{make checkproofs J=6}. As when converting \texttt{.vio}
files to \texttt{.vo} files, universe constraints are not checked to be
globally consistent. Hence this compilation mode is only useful for quick
regression testing and on developments not making heavy use of the $Type$
hierarchy.
\subsection{Limiting the number of parallel workers}
\label{coqworkmgr}
Many Coq processes may run on the same computer, and each of them may start
many additional worker processes.
The \texttt{coqworkmgr} utility lets one limit the number of workers, globally.
The utility accepts the \texttt{-j} argument to specify the maximum number of
workers (defaults to 2). \texttt{coqworkmgr} automatically starts in the
background and prints an environment variable assignment like
\texttt{COQWORKMGR\_SOCKET=localhost:45634}. The user must set this variable in
all the shells from which Coq processes will be started. If one uses just
one terminal running the bash shell, then \texttt{export `coqworkmgr -j 4`} will
do the job.
After that, all Coq processes, e.g. \texttt{coqide} and \texttt{coqc},
will honor the limit, globally.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
