noncomputable and to_additive

Stream: mathlib4

[Sebastien Gouezel]

A weird interaction between to_additive and noncomputable. The following works fine

import Mathlib.MeasureTheory.Measure.Haar.Basic
noncomputable section
open MeasureTheory

-- @[to_additive]
instance (α : Type*) [MeasurableSpace α] (G : Type*) [SMul G α] : SMul G (Measure α) :=
{ smul := fun g μ ↦ Measure.map (fun x ↦ g • x) μ }

But if you uncomment the to_additive, then you get a complaint

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'MeasureTheory.Measure.map', and it does not have executable code

Marking it by hand as noncomputable fixes it, so this is not a blocker at all, but still it doesn't seem right. @Floris van Doorn , any idea what could be going wrong?

[Alex J. Best]

I would say this is a core issue. Declarations in noncomputable sections that are not compiled are not currently tagged noncomputable
see

import Mathlib.Tactic


noncomputable section
def t : ℕ := Classical.choose (⟨0, trivial⟩ : ∃ n, True)

end section
noncomputable def t' : ℕ := Classical.choose (⟨0, trivial⟩ : ∃ n, True)


#eval t

open Lean Tactic Elab Meta
#eval show MetaM Unit from do
  dbg_trace isNoncomputable (← getEnv) `t

#eval show MetaM Unit from do --for comparison
  dbg_trace isNoncomputable (← getEnv) `t'

[Alex J. Best]

I'll make a PR to change this later today, and see if it is a desired change or not

[Alex J. Best]

This is now https://github.com/leanprover/lean4/pull/2610