lean_initialize_runtime_module
lean_initialize
Calling both runs the initializers twice, resulting in a memory leak
parseQuotWithCurrentStage
true
stderrAsMessages