Zulip Chat Archive

Stream: general

Topic: to_additive & parallelism

Reid Barton (Sep 08 2020 at 12:23):

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 (Sep 08 2020 at 12:23):

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

Mario Carneiro (Sep 08 2020 at 12:27):

it does exactly what you fear

Mario Carneiro (Sep 08 2020 at 12:27):

it joins the proof on the main task

Mario Carneiro (Sep 08 2020 at 12:28):

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

Last updated: Aug 03 2023 at 10:10 UTC