How do I check the proofs within a single file in parallel when building with -vok? There used to be flags along the lines of -async-proofs-j and such for vio2vo conversion; what’s the official way to do this today for -vok?
As far as I can see, there is no code in 8.11.0 at all in (files related to) coqc for setting up processing of proof tasks like for vio. In fact, the production of vok shares most of its processing code with vo files.
Wouldn’t this kind of asynchronous, possibly-out-of-order proof processing require suspended proofs like for vio? I was at least under the impression that only file-level parallelism was possible for vos/vok, but someone with more knowledge of the Stm should confirm.
Maybe you can use -async-proofs on.
Not sure how well it works.
We tried that form of parallelism in our empirical investigation of mutation analysis for Coq, and the results were mostly terrible, even for projects with quite long-running proofs. One part of the problem is that one normally wants to do some kind of scheduling over the workers (to assign them mostly equal workshares), and to my knowledge this is either impossible or very difficult to set up with this approach.
What’s the problem? If the problem is estimating the workload, couldn’t you use work-stealing? If a worker is done earlier, it can fetch more tasks.
This question was about existing options for coqc, not functionality that could be added. From my recollections of when I last looked at the code, -schedule-vio-checking and -vio2vo do not use any form of work stealing, and -async-proofs does not for sure. To add work stealing, one could either change this code or write some new external system for worker management, but I think this would be best discussed as a Coq issue or under the “Developing the Coq System” topic.
1 Like