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