Commit 2025-08-19 11:46 630b14d9

fix: handle noncomputable section in to_additive (#28610) This PR allows to_additive to succeed for unmarked noncomputable defs in noncomputable sections. Previously, to_additive on an unmarked noncomputable defs in noncomputable section would fail, since noncomputable section does not explicitly mark its noncomputable defs as noncomputable in the environment extension; instead, compilation just fails silently. This PR matches that behavior for the generated declaration when the original declaration has no executable code. Note that we cannot test for noncomputable section directly, since this is stored in the CommandElabM scopes, while the attribute's add function runs in CoreM. Hence, we use the lack of executable code as a proxy for noncomputable section. However, this is not a perfect workaround: if a definition tagged with to_additive is outside of noncomputable section but is not computable, compilation of the original declaration will fail and an error will be logged. But since the original now has no executable code, the generated to_additive declaration will be added without error. The messages and infostate are reset before running the attribute's add, so it is not possible to detect such a compilation error on the original declaration without a potentially costly recompilation of the original declaration. See Zulip.