to_additive & parallelism

Stream: general

[Reid Barton]

Just curious: Do we know how to_additive interacts with proving lemmas in side tasks?
Since to_additive translates definiitons to definitions and lemmas to lemmas, it should be possible for it to translate the statement of a lemma on the main task while translating the proof on a side task (which will join on the task that is checking the original lemma when it tries to fetch the original proof). But it would be easy to implement to_additive in a way for which that doesn't happen, which would mean that the main task ends up joining on the checking the original proof, which wouldn't happen in the absence of to_additive.

[Reid Barton]

Maybe it doesn't really matter because the theorems to which we apply to_additive generally have trivial proofs.

[Mario Carneiro]

it does exactly what you fear

[Mario Carneiro]

it joins the proof on the main task

[Mario Carneiro]

you know, I'm apparently the sole author of tactic.transform_decl but I don't recognize any of the functions in it