The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/09/2013 05:48 PM, Enrico Tassi wrote:
> 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...
>    

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? >:)

> 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.
>    

I think I'm "picky" according to the above.  I want to get out 
axiom-free proofs that can be validated by the usual Coq kernel. :)  
(Which is "easy" to do with manual creation of many files proving lemmas.)