builtin_initialize leads to "unknown declaration 'initFn...'

Stream: lean4

[Jannis Limperg]

I set up a fork of Lean 4 where I builtin_initialize an env extension and an attribute in a new file in the standard library. Lean then builds fine, but when I run the resulting lean binary, it reports

unknown declaration 'initFn._@.Init.Data.Random._hyg.631'

This happens with both the Nix build and the CMake build. I got this error a couple of times already and managed to 'solve' it by executing random commands until it went away, but I'd prefer to know what's actually going on.

[Jannis Limperg]

(If you need the code, I'll be happy to upload it of course, but I suspect this might be expected behaviour in some sense.)

[Sebastian Ullrich]

Did you update stage 0 (see Building Lean docs) after the change? Your binary with the attribute likely isn't compatible with the stdlib built without it, which might explain any weird behavior.

[Jannis Limperg]

Okay, that's probably the culprit then. Thanks! (Live support from the devs on a Saturday evening -- I am spoilt.)

[Kevin Buzzard]

When I'm advertising lean to mathematicians I tend to mention the "24/7 helpline" as I now call the Lean Zulip

[Jannis Limperg]

I'll need some more help from that helpline I'm afraid. After I update stage0 (make update-stage0 and commit), stage0 builds but stage1 does not. It fails to build Init/Data.lean with the same error:

Init/Data.lean:6:0: error: unknown declaration 'initFn._@.Init.Data.Random._hyg.631'

I also get the exact same error when I build stage2 without updating stage0 first. Same with the equivalent Nix commands as well.

[Sebastian Ullrich]

Ok, then it must be something specific to your code. I feel like I have seen that error once before when changing the stages, but not in a long while.

[Jannis Limperg]

Okay, let me minimise. So I should be able to build stage2 without updating stage0, right?

[Sebastian Ullrich]

Yes. Building stage2 or update-stage0+stage1 should be equivalent

[Jannis Limperg]

Minimised.

The issue is somehow sensitive to imports. Building this tree with nix build .#stage2 fails, but after removing the import Lean.Meta line, the same command succeeds.

[Jannis Limperg]

Minimised some more. Seems like it doesn't actually matter what I builtin_initialize.

[Jannis Limperg]

Turns out the error has nothing to do with builtin_initialize after all. It appears to be triggered by importing Lean.Meta.CollectFVars, a completely innocuous 30-line module. Importing it transitively also triggers the error; importing every other module doesn't. Should I open an issue at this point?

[Sebastian Ullrich]

It seems to work if you move your import to the end (presumably after the original imports). I'm not yet sure why.

[Sebastian Ullrich]

The import of Lean.Bug, that is

[Jannis Limperg]

Yes, that works, also for my non-minimised code.