The Coq mailing list

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

On Sat, Mar 09, 2013 at 01:34:47PM -0500, Adam Chlipala wrote:
> I'd like to have a tactic that behaves like:
>     Ltac parallelSemicolon x y := x; abstract y.
> ...but runs the different "y" subgoal executions in parallel on
> multiple processors.
> 
> This doesn't sound too hard to implement from a scientific
> perspective, though I'm not sure of the engineering challenges.  Is
> anyone working on functionality like this, or does anyone have tips
> on how it could be achieved in today's Coq?

Well, not in today's Coq.  But eventually it will be doable in my
ParalITP branch.  But not today...

> (Of course, one can get a similar benefit in a laborious way today,
> by explicitly stating each subgoal as a theorem in a separate .v
> file, making it easy to prove each theorem with a separate 'coqc'

From an engineering point of view, OCaml leaves you no choice.  You have
to run your ys in different processes.  How to pass the state of the prover
back and forth is still an open question in ParalITP.

The quickest hack that comes to mind is the following one, but only if
you are not too picky. You could fork (hence the input state is already
there) and just call "exit 0" if "abstract y" succeeds and "exit 1"
otherwise.  The father process can then run admit if the corresponding
child exits with 0 and fail otherwise.  But spawning hundreds of
processes may not be a good idea anyway.

Ciao
-- 
Enrico Tassi