Stream: Coq users

Topic: Parallel proof processing


view this post on Zulip Michael Soegtrop (Mar 14 2023 at 13:46):

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

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 14:02):

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

view this post on Zulip Gaëtan Gilbert (Mar 14 2023 at 14:02):

AFAIK -async-proofs-tac-j works for tactic workers

view this post on Zulip 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: Mar 28 2024 at 14:01 UTC