Zulip Chat Archive
Stream: new members
Topic: When do `initialize` blocks run?
Andy Phan (Sep 03 2025 at 13:38):
I was reading about initialization in the reference manual (https://lean-lang.org/doc/reference/latest/////Elaboration-and-Compilation/#initialization). From the wording it seems like initialize would run before elaboration/compilation, but when I make an initialize block like below it also runs when I run the program after building it?
initialize
println! "hello"
Andy Phan (Sep 03 2025 at 13:47):
Also, what does it look like when the initialize block is used to add an environment extension?
Robin Arnez (Sep 03 2025 at 17:28):
initialize blocks are evaluated when the module they're in is imported + when a program that depends on a module is run
Last updated: Dec 20 2025 at 21:32 UTC