In large, complex proofs it is sometimes difficult to make the overall argument parallel (due to linear
Require dependencies). However, it is common practice in individual proofs to see e.g.
apply lemma1; [ auto | firstorder | ]. apply lemma2; [ trivial | auto | ]. rest_of_proof...
In particular, applying
lemma2 creates several (here three) subgoals, of which only one (here the third) is particularly interesting and the others can be solved by automation individually (also contain no evars).
More often than not, heavy automation increases compilation time.
Assume in the above
rest_of_proof take roughly the same time to compile.
Suggestion (is the following interesting/feasible?):
Introduce a tactical
async such that given a tactic
t, the tactic
async t succeeds immediately (if the goal has no evars) and closes the goal. Simultaneously, a worker is spawned that is responsible to actually close the goal using the tactic
Returning to the above example
apply lemma1; [ async auto | async firstorder | ]. apply lemma2; [ trivial | async auto | ]. rest_of_proof...
would (given at least 4 CPU cores) compile several times faster. I know of
par:, which does not seem to fit the above use case.
Before adding another [wish] to the Coq bugtracker, I wanted to know your opinion. Somewhat related: #9550