The Coq mailing list

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

On 03/09/2013 01:55 PM, AUGER Cédric wrote:
> Le Sat, 09 Mar 2013 13:34:47 -0500,
> Adam 
> Chlipala<adamc AT csail.mit.edu>
>   a écrit :
>
>    
> > 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.
> >      
> I fear there are some tricks with Coq’s side effects.
> For instance for your 'abstract' tactic, if the tactics contains a
> 'fix' tactic, then there must be a reference to "…_subproof<n>" but I
> think that the<n>  is just choised by inspecting the environment and
> finding the first<n>  which is free. Running in parallel would require
> to allocate first these<n>. As such, this is not really an issue, it
> seems easy to fix.

Yes, I would expect it would be easy to renumber all "locally generated" 
theorems as necessary, as each proven subgoal is merged back into the 
main process.

> There is also the "evar" problem. When you have two
> goals containing evars, some tactics have side effects on the other
> goal by fixing some evars. That means that you cannot really run the
> tactics in parallel. I think this problem could be solved by extending
> Ltac to have "true" parallel tactics which refutes side effects (or
> maybe cannot be run if there are evars in the parallel goals [if you
> want this only for your abstract tactic, that seems reasonnable as
> abstract does not handle evars AFAIK]).
>    

I do consider "abstract" to be a fundamental part of my request (it's 
absolutely necessary to keep memory usage down, even for serial 
execution), so, as you say, evars in the initial subgoals are ruled out, 
and there doesn't seem to be any problem.