Michael Soegtrop (Mar 14 2023 at 13:46): Michael Soegtrop (Mar 14 2023 at 13:46):I have a few questions on parallel proof processing (Coq 8.16):
-async-proofs on -async-proofs-j 6 - this gives me 6 instances of coqproofworker.opt and 2 instances of coqtacticworker.opt. In many of my applications the tactic workers are at 100% and the proof workers are at 0%, so I wonder if I can change the number of tactic workersabstract like coq-interval seem to create an anomaly with par: - I darkly remember that this is known issue, but I couldn't find one ... Gaëtan Gilbert (Mar 14 2023 at 14:02):about abstract there's always https://github.com/coq/coq/issues/9146
Gaëtan Gilbert (Mar 14 2023 at 14:02):AFAIK -async-proofs-tac-j works for tactic workers
Michael Soegtrop (Mar 15 2023 at 09:06):Thanks! It is a bit weird that this is not documented in https://coq.inria.fr/refman/addendum/parallel-proof-processing.html, but with the par: goal selector.
Last updated: Oct 13 2024 at 01:02 UTC