Nowhere to add `noncomputable`

Stream: lean4

[Eric Wieser]

For this example:

noncomputable def ohno := 1

structure OhNo where
  x := ohno

lean says

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

How do I "mark this as noncomputable"?

[Damiano Testa]

Does wrapping it in suppress_compilation work? It is either a success or a feature request...

[Eric Wieser]

Nope, nor does noncomputable section

[Jireh Loreaux]

It seems that marking inductives (hence also structure) is expressly prohibited by docs#checkValidInductiveModifier defined in Lean.Elab.Inductive and used in Lean.Elab.Declaration when parsing the declaration. It is also expressly prohibited on fields of a structure in Lean.Elab.Structure. I'm not sure why its use is prohibited though. Maybe because Lean can't construct the recursor? That's beyond my understanding.

[Eric Wieser]

The recursor, constructor, and projections should all be computable here

[Eric Wieser]

All that's noncomputable is the magic for the {} notation

[Kevin Buzzard]

Is this a theoretical observation or did it actually happen to you btw?

[Eric Wieser]

This happened to me while trying to help someone in #new members

[Eric Wieser]

:= in structures is not useful very often anyway, but if it doesn't work for noncomputable then it's going to be even more useless for mathlib!

[Eric Wieser]

(the kicker here is that the the real example is only noncomputable because of suppress_compilation and the compiler being too slow)

[Alex J. Best]

You could do

import Mathlib.Tactic
noncomputable def ohno := 1
open Lean Elab
macro "ok" :tactic =>
`(tactic| exact ohno)
structure OhNo where
  x : Nat := by ok

#check OhNo.mk

lol. Its not clear where you can add a modifier like this tbh, maybe after the := ?
It is the def OhNo.x._default that you'd like to have a way of marking noncomputable indeed.

It turns out both of these are valid syntax but turned down by the elaborator, they wouldnt be the right thing anyway.

structure OhNo where
noncomputable mk ::
  noncomputable (x : Nat := 1)

[Mario Carneiro]

Another fix would be to make the compiler allow this definition, it should not be noncomputable in the first place because the bad term appears in an annotation

[Eric Wieser]

I think it would be reasonable for it to force me to write

structure OhNo where
  x := noncomputable ohno

[Eric Wieser]

Since Lean seems to want noncomputability to never be implicit

[Scott Morrison]

A bug report would be good!

[Eric Wieser]

lean4#2710

[Eric Wieser]

Am I imagining that the lean4 web editor used to have a button to reveal the version number of lean, but no longer does?

[Scott Morrison]

No sure about the button. #eval Lean.versionString is a workaround.