Large-scale verification projects using proof assistants typically
contain many proofs that must be checked at each new project
revision. While proof checking can sometimes be parallelized at the
coarse-grained file level to save time, recent changes in some proof
assistant in the LCF family, such as Coq, enable fine-grained
parallelism at the level of proofs. However, these parallel techniques
are not currently integrated with regression proof selection, a
technique that checks only the subset of proofs affected by a
change. We present techniques that blend the power of parallel proof
checking and selection to speed up regression proving in verification
projects, suitable for use both on users' own machines and in
workflows involving continuous integration services. We implemented
the techniques in a tool, piCoq, which supports Coq projects. piCoq
can track dependencies between files, definitions, and lemmas and
perform parallel checking of only those files or proofs affected by
changes between two project revisions. We applied piCoq to perform
regression proving over many revisions of several large open source
projects and measured the proof checking time. While gains from using
proof-level parallelism and file selection can be considerable, our
results indicate that proof-level parallelism and proof selection is
consistently much faster than both sequential checking from scratch
and sequential checking with proof selection. In particular, 4-way
parallelization is up to 28.6 times faster than the former, and up to
2.8 times faster than the latter.