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
|
\achapter{Asynchronous Proof Processing}
\aauthor{Enrico Tassi}
\label{pralitp}
\index{Asynchronous 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 contruction and checking of proofs
objects.
This feature is desingned to help dealing with huge libraries of theorems
characterized by long proofs. At the current state it may not be beneficial
on small set 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
signalled late. The most notable type of errors belonging to this category are
universes inconsistency or unsatisfied guardedness conditions for fixpoints
built using tactics.
Last, at the time of writing, only opaque proofs (ending with $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 $Section$ (see Section~\ref{Section}).
When a section is ended 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 make the construction of the proofs not
mandatory for ending a section one can start each proof with the
$Proof using$ command~\ref{ProofUsing} that declares the subset of section
variables the theorem uses.
The presence of $Proof using$ is mandatory 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. In case 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 variable used.
\subsubsection{Automatic suggestion of proof annotations}
The command $Set Suggest Proof Using$ makes Coq suggest, when a $Qed$
command is processed, a correct proof annotation. It is up to the user
to modify the proof script adding the proof annotation.
\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, that 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 $Qed$ command is
is coloured using a color that is lighter 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 proof objects one has to click the button
with the gears.
Only when the gears button is pressed all universe constraints are checked.
\subsubsection{Caveats}
The number of worker processes can be increased by passing CoqIDE the
$-async-proofs-j 2$ flag. Note that the memory consumption increases
too, since each worker has to be an exact copy of the master process
and requires the same amount of memory. Also note that the master process
has to both respond to the user and manage the workers, hence increasing
their number may slow down the master process.
To disable this feature it is enough to pass the $-async-proofs off$ flag to
CoqIDE.
\subsection{Batch mode}
When Coq is used as a batch compiler by running $coqc$ or $coqtop -compile$
it produces a $.vo$ file for each $.v$ file. A $.vo$ file contains, among
other things, theorems statements and proofs. Hence to produce a $.vo$
Coq need to process all the proofs of the $.v$ file.
The asynchronous processing of proofs can decouple the generation of a
compiled file (like the $.vo$ one) that can be $Required$ from the generation
and checking of the proof objects. The $-quick$ flag can be passed to
$coqc$ or $coqtop$ to produce, quickly, $.vi$ files. Alternatively, if
the $Makefile$ one uses was produced by $coq\_makefile$ the $quick$
target can be used to compile all files using the $-quick$ flag.
A $.vi$ file can be $Required$ exactly as a $.vo$ file but: 1) proofs are
not available (the $Print$ command produces an error); 2) some universe
constraints are missing, hence universes inconsistencies may not be
discovered. A $.vi$ 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 $-quick$ flag allows one to work,
interactively, on any file without waiting for all proofs to be checked.
While one works interactively, he can fully check all $.v$ files by
running $coqc$ as usual.
Alternatively one can turn each $.vi$ into the corresponding $.vo$.
All $.vi$ files can be processed in parallel, hence this alternative
may be faster. The command $coqtop -schedule-vi2vo 2 a b c$
can be used to obtain a good scheduling for 2 workers to produce
$a.vo$, $b.vo$ and $c.vo$. If the $Makefile$ one uses was produced
by $coq\_makefile$ the $vi2vo$ target can be used for that.
The variable $J$ should be set to the number of workers, like
in $make vi2vo J=2$. The only caveat is that, while the $.vo$ file
obtained from $.vi$ 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 $.vo$ files
are (recursively) loaded with $Require$.
There is an extra, possibly even faster, alternative: just check
the proof tasks store in $.vi$ files without producing the $.vo$ files.
This is possibly faster because all proof tasks are independent, hence
one can further partition the job to be done between workers.
The $coqtop -schedule-vi-checking 6 a b c$ command can be used to obtain
a good scheduling for 6 workers to check all proof tasks of $a.vi$, $b.vi$ and
$c.vi$. 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.
If the $Makefile$ one uses was produced by $coq\_makefile$ the $checkproofs$
target can be used to check all $.vi$ files. The variable $J$ should be
set to the number of workers, like in $make checkproofs J=6$.
Checking all proof tasks does not guarantee the same degree of safety
that producing a $.vo$ file gives. In particular universe constraints
are checked to be consistent for every single proof, but not globally.
Hence this compilation mode is only useful for quick regression testing
and on developments not making heavy use of the $Type$ hierarchy.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
