coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Multi-core execution?
- Date: Sat, 9 Mar 2013 23:48:27 +0100
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...
> (Of course, one can get a similar benefit in a laborious way today,
> by explicitly stating each subgoal as a theorem in a separate .v
> file, making it easy to prove each theorem with a separate 'coqc'
From an engineering point of view, OCaml leaves you no choice. You have
to run your ys in different processes. How to pass the state of the prover
back and forth is still an open question in ParalITP.
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.
Ciao
--
Enrico Tassi
- [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Jason Gross, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Jason Gross, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Jason Gross, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Pierre-Marie Pédrot, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/09/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Pierre Courtieu, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Arnaud Spiwack, 03/11/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/11/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/11/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/11/2013
- Re: [Coq-Club] Multi-core execution?, Arnaud Spiwack, 03/11/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/11/2013
- Re: [Coq-Club] Multi-core execution?, Pierre Courtieu, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Enrico Tassi, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, Adam Chlipala, 03/10/2013
- Re: [Coq-Club] Multi-core execution?, AUGER Cédric, 03/09/2013
Archive powered by MHonArc 2.6.18.