Cannot evaluation [init] declaration in same module

Stream: lean4

[Eric Wieser]

I'm getting the titular error message from a module that contains only imports, and so surely cannot claim any init declarations as its own.

Roughly my setup is:

-- In Linters/Foo.lean

register_option linter.foo : Bool := {
  defValue := true
  descr := "foo"
}

def fooLinter : Linter where
  run := someFactory linter.foo

initialize addLinter fooLinter

-- in Linters.lean
import Linters.Foo

which fails when building Linters.lean on 4.22.0, complaining about how linter.foo is accessed.

[Robin Arnez]

init declarations are run in the wrong order, this was also a problem on nightly-testing

[Eric Wieser]

Ultimately this was fixed with @[noinline] on a function like:

def logLint {m} [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT BaseIO m]
    (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit := do
  (if ← foo then logErrorAt else logWarningAt)
    stx (.tagged linterOption.name m!"{msg} [{linterOption.name}]")

which I guess was being inlined and the compiler then tried to inline linter.foo.name

[Eric Wieser]

@Robin Arnez, is there a bug report for that?

[Robin Arnez]

I don't think so

[Robin Arnez]

You can report it if you can find an mwe that works on latest nightly (just make a new project with today's nightly toolchain)

[Robin Arnez]

As far as I'm aware, the order specifically depends on the names of the init declarations..?

[Robin Arnez]

Actually, I'll make the issue

[Robin Arnez]

lean4#10175