The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 15/03/2013 15:50, Adam Chlipala wrote:
> Nifty!  I'd love to see an evolution of this so that I can use it my
> scenario.  I imagine it would be worth throttling the rate at which
> processes are forked, based on how many cores are available.

Hi there,

I allow myself to resuscitate this thread to announce that, having taken
an hour or so to implement it properly, there is now a plugin that
allows to dispatch a tactic on several system processes. It can be found at:

https://github.com/ppedrot/vitef/tree/master/tacfork

It currently compiles on the current trunk, though it can be easily 
patched to compile against v8.4.

For now, it is still quite dumb as you mentioned, as a process is forked 
for each subgoal. It is really a hack, and it would need any polishing 
to be useful, but I wanted to advertise it nonetheless.

Cheers,
PMP