The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

This is an important question. Also a pretty hard one.

The main problem is that tactics are inherently sequential (even with bullets and stuff, because of the existential variables as remarked earlier in this thread). This sequentiality is hard-coded in the type of tactics; very much so in fact. In my branch the situation is actually even worse : the (sequential) state of the proof contains the (partial) solutions for goals (because it handles dependent subgoals as well). So we need to be able to join states at the end of the fork (I hear there is a word for datastructure which support join operations: confluently persistent). My guess, is that given sufficient guarantees on the actual independence of goals and maybe a side of luck, this is a reasonable assumption (the state being essentially a typing and unification environment for existential variables, there is some kind of union on them which works under certain conditions (but bites you in the back quite a bit when they are not met)).

I used to think it was pretty much insurmountable a task, but I'm not so sure any more. With the proviso that without Enrico's aforementioned branch the abstract (and admit) tactic will not work as expected, I will try to hack a prototype (for my branch https://github.com/aspiwack/coq ) such tactical within a few weeks so that we can experiment with it. Or fail trying. And then get back to this thread. Watch for updates.

On 10 March 2013 22:48, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

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!