diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 929d492..113bade 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -10,7 +10,9 @@ namespace DocGen4 open Lean System IO def envOfImports (imports : Array Name) : IO Environment := do - importModules (imports.map (Import.mk · false)) Options.empty (leakEnv := true) + -- needed for modules which use syntax registered with `initialize add_parser_alias ..` + unsafe Lean.enableInitializersExecution + importModules (imports.map (Import.mk · false)) Options.empty (leakEnv := true) def loadInit (imports : Array Name) : IO Hierarchy := do let env ← envOfImports imports