I have a few questions on parallel proof processing (Coq 8.16):

- I start coqidetop with
`-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 workers - tactics which use
`abstract`

like coq-interval seem to create an anomaly with`par:`

- I darkly remember that this is known issue, but I couldn't find one ...

about abstract there's always https://github.com/coq/coq/issues/9146

AFAIK `-async-proofs-tac-j`

works for tactic workers

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: Jun 16 2024 at 02:41 UTC