The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Jun 17, 2015 at 07:08:17AM +0000, Soegtrop, Michael wrote:
> and of cause in large developments, make -j <#threads> is your friend.

Thanks for reminding coq-club that Coq features a (sort of) separate
compilation!

> actually Coq/CoqIDE 8.5 does several proofs in one file in parallel. I
> don’t know how it works exactly. It looks like it first parses the Coq
> file and loads the libraries and then runs several Coqtops in parallel
> to proof several theorems in parallel. I didn’t figure out as yet how
> the dependency handling works. Sometimes I have the impression it

The main idea is that Coq 8.5 can separate the work of checking a
document into two phases: checking the statements and checking the
opaque proofs (Proof..Qed blocks).  This works both in batch and
interactive mode.
All opaque proofs are independent, so Coq can process them in an arbitrary
order.  On PIDE based interfaces (Coqoon or Jedit) it gives priority to
the ones you have on the screen.  CoqIDE goes FIFO.
For the records, there is no real notion of dependency among proofs and
definitions or statements, so if you change a definition or statement
Coq will re-check everything that follows it.

The doc is here:
  https://coq.inria.fr/distrib/8.5beta2/refman/Reference-Manual031.html

For the ones really interested in the details (including a benchmark,
section 5) there is a paper: https://hal.inria.fr/hal-01135919
(the PDF should pop up soon, it you don't see it here an alternative
link: http://www-sop.inria.fr/members/Enrico.Tassi/stm.pdf)

To go back to the original question, my experience is that on a
development that never saturates 3 cores with `make -j12`, you can
saturate almost 10 with `make -j12 quick; make vio2vo J=12`.  So buying
parallel hardware may not be a bad idea.  W.r.t. RAM usage,
parallelism is obtain by running multiple processes, and I've seen
myself coqtop instances eating 2G of memory.  If you run 10 of them
in parallel you surely need 20G of RAM (no sharing at all).

Best,
-- 
Enrico Tassi