what is builtin_initialize

Stream: new members

[Xiyu Zhai]

As a newbie (an excuse I will use for at least three months), I'm curious what is builtin_initialize in the Lean source code? I couldn't find an explanation myself.

[Xiyu Zhai]

Where's the general place for explanation of compiler magic?

[Xiyu Zhai]

Does it mean something like in a scripting language, it will be executed when loaded?
Something like lazy_static in Rust?

[Kyle Miller]

There are two things going on here:

1. Yes, it is possible to associate code to modules that gets run when the module is loaded. This is the initialization code. It's only for compile time and not for run time (as far as I've understood).
2. The builtin part has to do with the staged compilation of Lean 4 itself. Since Lean 4 is largely written in Lean 4, some parts of it need to be set to be part of the compiled "stage 0" Lean 4, which is used to compile the next stage. I'm not super clear on the details, but here's the boostrapping page of the manual.

User code uses initialize rather than builtin_initialize.

[Xiyu Zhai]

thanks a lot