Zulip Chat Archive

Stream: general

Topic: to_additive & parallelism


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 08 2020 at 12:27):

it does exactly what you fear

view this post on Zulip Mario Carneiro (Sep 08 2020 at 12:27):

it joins the proof on the main task

view this post on Zulip 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: May 12 2021 at 03:23 UTC