Weird initialize error

Stream: lean4

[Xubai Wang]

When I use initialize with @[extern] constant Lean would complain that it could not find native implementation of external declaration xxx. The code is like this and the full example is provided here.

@[extern "foo_initialize"] constant fooInit : IO Unit

initialize fooInit

The weird point is that when I change initialize to builtin_initialize, the code builds successfully.
After doing some search I found some discussions about initialize and builtin_initialize from other topics.

Sebastian Ullrich said:

Yes, it's not expected to also import a plugin, though we should probably make sure it still works since you might not be able to avoid it in case of some shared module. I'm not sure initialize being run in a plugin is even intended, usually builtin* means "run when native code is loaded, register into some global IO.Ref" and non-builtin means "run when imported, register into the environment".

Mac said:

I think initialize, despite its name, actually runs after initializing the environment, whereas bulitin_initialize actually runs during initialization.

Does this mean that the user provided external code should not be viewed as part of the package, and should always be called with builtin_initialize? And they are loaded whether or not the package is imported?

[Mac]

Xubai Wang said:

Mac said:

I think initialize, despite its name, actually runs after initializing the environment, whereas bulitin_initialize actually runs during initialization.

Note that I said this before user-defined attributes and environment extensions were supported. This may not be the case anymore (i.e., initialize now might run during initialization).