The Coq mailing list

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

On Sun, Mar 10, 2013 at 10:21:50AM -0400, Adam Chlipala wrote:
> My guess is that the subcase that interests me would be easy enough
> to have ready much earlier.  Could I convince you to give it a try?
> >:)

To exploit parallel hardware in OCaml you need some machinery to handle
a pool of already running workers and have an efficient way to transmit
a prover state back and forth.  The machinery in question must be
efficient enough to support the granularity of parallelism one wants.
The more fine grained it is, the more efficient the machinery must be.

If I understand well your use case, you want to delegate to slave
processes small jobs.  IMO it the most difficult case.

My plan is to begin parallelizing proofs, then sub proofs (assuming the
proof language lets you easily identify independent chunks) and finally,
only if the machinery turns out to be fast enough, tactics.
I'm sorry, but I'm not going to give it a try soon.
-- 
Enrico Tassi