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

[Sébastien Gouëzel]

I was about to mention a bad interaction between to_additive and noncomputable section that I encountered recently, with the following MWE:

import Mathlib

noncomputable section

@[to_additive]
def myOne (α : Type) [One α] : α := by
  have : ∃ (x : α), x = 1 := ⟨1, rfl⟩
  exact Classical.choose this

where one gets a complaint that the additivized declaration should be marked noncomputable, although one is already in a noncomputable section.

Then I realized that there was already a discussion about this on Zulip, initiated by myself (!) 2 years ago, with a suggested fix. @Kim Morrison, is it something core could consider fixing?

[Kim Morrison]

Yes, definitely. Someone would need to create an issue, however, explaining the problem, ideally something that doesn't need Mathlib at all.

Tagging Cameron Zwarich on such an issue is probably the right thing to do. Everything about noncomputable is in flux at the moment, as we switch everyone over to the new compiler in the near future.

[Sébastien Gouëzel]

There is already an issue and a PR at lean4#2610. @Cameron Zwarich

[Kim Morrison]

An separate issue is probably more likely to get traction than an abandoned broken PR.