Hi ! We are using a modified version of HOL Light to perform aggressive parallelization of proof search:
This is used with some machine learning technics to train our models. We are wondering if we could perform the same kind of operations in Coq (serializing any subgoal and restoring a coq process at this location), so we could also train with Coq in the same way we do with HOL Light and share our infra.
It's been a decade I had a look at Coq's internal, so if this idea is not completely crazy, can anyone point me in the right direction ?
There is some support for parallellizing files, proofs and "leaf goals" in Coq. It's based on processes, marshaling and pipes/socket. Thee is no code to start workers remotely, but it is surely doable.
See https://coq.inria.fr/refman/addendum/parallel-proof-processing.html and https://hal.archives-ouvertes.fr/hal-01135919
Thank you for the info, I'll study that. My current understanding of the model is that we can basically do that but at the proof granularity, not at any subgoal (but I'm lagging.. like 10 years) :D
@Vincent Siles we go through almost all possible ways of parallelizing Coq proofs in the following papers, with benchmarks on large projects:
http://users.ece.utexas.edu/~gligoric/papers/PalmskogETAL18piCoq.pdf
The following paper also has some perspective on parallel proving, but its focus is different:
http://users.ece.utexas.edu/~gligoric/papers/CelikETAL19mCoq.pdf
If you only have time for one paper, I recommend the middle one (from 2018).
bottom line is that parallelization at subgoal level is not currently possible. But on the other hand, well-factored Coq projects don't spawn lots of subgoals all the time, so not clear to me subgoal parallelization would even help. However, we establish that proof-level parallelization is helpful to almost all Coq projects (at the cost of dropping global universe consistency checking).
Paralllel subgoal proof checking would be very useful to those of us doing inductive proofs (on large inductives or involving large subproofs in each case)
How well does "par:" work?
IIRC the manual alleges it should be relevant.
Let me be more precise: I'd like Coq to rely on the bullet structure to parallelize the checking
@Matthieu Sozeau but this kind of low-level (bullet) parallelization would have quite a lot of overhead unless new jobs are cheap. Are you aiming to use OCaml-level parallelization?
@Vincent Siles no parallelism is needed in fixpoint proofs, hopefully?
par:
works for leaf goals, eg par: tac
requires tac
to kill the goal and the goals must be independent (unlike "a < ?b" and "?b < c").
It could be extended to full (independent) subproofs (as in bullets).
According to M. Wnzel, in Isabelle most of the parallelism still comes from proof-level parallelism, even if they have "forward step" parallelism as well (ISAR is mostly "assert STATEMENT by CODE", each of these is potentially a separate job). I mean that you can saturate all your cores with just the proofs, adding proof steps does not change the game (of saturating CPUs, on AFP).
I still think it can be useful in interactive mode, in order to jump to the second bullet and have the first one be run in the background.
on the other hand, PL-style proofs with really big inductive types is not what most people (in AFP) use Isabelle for
BTW, @Karl Palmskog par:
was added because some power users had scripts like VC_gen; solver
, which is not very commonly structured but could benefit for leaf goal parallelization. I agree that in math-comp, for example, par: is useless and even bullet level would be of dubious interest.
For PL stuff, it is another story I agree
A slight tangent. How about parallelization of big computations in Coq? E.g. 4-color.
We're also looking at some embarrassingly parallel algorithms where having parmap from ocaml would help.
Enrico Tassi said:
I still think it can be useful in interactive mode, in order to jump to the second bullet and have the first one be run in the background.
Yes, that's my main wish actually
I'd also love par-bullets. Doing this on all bullets might be too slow, but I'd consider writing p* instead of * at the right places to get parallelism
Paolo Giarrusso said:
Vincent Siles no parallelism is needed in fixpoint proofs, hopefully?
Good question, I didn't though about link between subgoals.
I don't remember seeing the equivalent of eapply & such in HOL Light, they might not have that
Karl Palmskog said:
bottom line is that parallelization at subgoal level is not currently possible. But on the other hand, well-factored Coq projects don't spawn lots of subgoals all the time, so not clear to me subgoal parallelization would even help. However, we establish that proof-level parallelization is helpful to almost all Coq projects (at the cost of dropping global universe consistency checking).
While parallelization in Coq at the subgoal level is not something which is currently possible, do you think we could serialize some internal Coq state from each subgoal, to restore the work on another Coq instance ? Or is this also not possible ? I read that a lot of care has been done in crafting the state to allow proof level parallelisation. I don't know enough of the internal to checker whether we could do a similar thing to the subgoal infra and try to import/export subgoals do to the parallelization "externally"
Last updated: Jun 08 2023 at 04:01 UTC