Skip to content

Commit

Permalink
fix: resolve build issues with mathlib
Browse files Browse the repository at this point in the history
See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/lean4checker.20failure/near/486823143 for more details.

If initializers don't run, then the parsers registered with `initlialize add_parser_alias ..` do not run, and so the alias never exists and the downstream code that references the alias crashes.

`import-graph` and the Batteries linter framework already include this line.
  • Loading branch information
eric-wieser authored Dec 9, 2024
1 parent 4e07f92 commit fae3926
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion DocGen4/Load.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 ..`
Lean.enableInitializersExecution
importModules (imports.map (Import.mk · false)) Options.empty (leakEnv := true)

def loadInit (imports : Array Name) : IO Hierarchy := do
let env ← envOfImports imports
Expand Down

0 comments on commit fae3926

Please sign in to comment.