Vincent Siles (Sep 21 2020 at 15:09): Vincent Siles (Sep 21 2020 at 15:09):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 ?
Enrico Tassi (Sep 21 2020 at 15:12):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.
Enrico Tassi (Sep 21 2020 at 15:13):See https://coq.inria.fr/refman/addendum/parallel-proof-processing.html and https://hal.archives-ouvertes.fr/hal-01135919
Vincent Siles (Sep 21 2020 at 15:54):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
Karl Palmskog (Sep 23 2020 at 11:56):@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).
Karl Palmskog (Sep 23 2020 at 11:58):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).
Matthieu Sozeau (Sep 23 2020 at 13:00):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)
Paolo Giarrusso (Sep 23 2020 at 13:03):How well does "par:" work?
Paolo Giarrusso (Sep 23 2020 at 13:04):IIRC the manual alleges it should be relevant.
Matthieu Sozeau (Sep 23 2020 at 13:13):Let me be more precise: I'd like Coq to rely on the bullet structure to parallelize the checking
Karl Palmskog (Sep 23 2020 at 13:27):@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?
Paolo Giarrusso (Sep 23 2020 at 13:39):@Vincent Siles no parallelism is needed in fixpoint proofs, hopefully?
Enrico Tassi (Sep 23 2020 at 13:46):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").
Enrico Tassi (Sep 23 2020 at 13:47):It could be extended to full (independent) subproofs (as in bullets).
Enrico Tassi (Sep 23 2020 at 13:51):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).
Enrico Tassi (Sep 23 2020 at 13:51):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.
Karl Palmskog (Sep 23 2020 at 13:52):on the other hand, PL-style proofs with really big inductive types is not what most people (in AFP) use Isabelle for
Enrico Tassi (Sep 23 2020 at 13:54):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.
Enrico Tassi (Sep 23 2020 at 13:55):For PL stuff, it is another story I agree
Bas Spitters (Sep 23 2020 at 14:14):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.
Matthieu Sozeau (Sep 23 2020 at 14:19):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
Paolo Giarrusso (Sep 23 2020 at 14:42):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
Vincent Siles (Sep 23 2020 at 14:43):Paolo Giarrusso said:
Vincent Siles no parallelism is needed in fixpoint proofs, hopefully?
Good question, I didn't though about link between subgoals.
Vincent Siles (Sep 23 2020 at 14:45):I don't remember seeing the equivalent of eapply & such in HOL Light, they might not have that
Vincent Siles (Sep 23 2020 at 14:48):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: Apr 19 2024 at 17:02 UTC