The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

My two cents: 

- Structured script with bullets and curly brackets among other goals aim at identifying independent chunks. 

- Remember that ocaml has garbage collection, which may cause forked processes to stop sharing memory and ruin the "almost free forking" paradigm.

- However quick and dirty hack: maybe one could try to patch the external tactic to call a fork of coq instead of an external procedure?

Best regards

Pierre

 

 

> No, I don't think my jobs qualify as small, compared to the time for a UNIX fork().  A majority of my subgoals require a second or more to prove.  Some take minutes.  So, even an approach based on fork()ing for each subtask could work quite well, I expect.  I would expect to see almost perfect improvement in running time, i.e. N cores divides running time by N.

My two cents: 

- structured script with bullets and curly brackets among other goals aim at identifying independent chunks. 

- remember that ocaml has garbage collection, which may cause forked processes to stop sharing memory and ruin the "almost free forking". However maybe one could try to patch the external tactic to call a fork of coq instead of an external procedure?

 

> > 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.
> >    
>
> Well, my use case of the "parallel semicolon" would only appear as the top-level tactic for a theorem, so perhaps my scenario fits into your "sub proofs" case.
>
> I'll be watching your work in this direction with great interest.  Thanks for pursuing it!