Skip to content

Commit

Permalink
fix: run Lean.enableInitializersExecution before importing modules
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser authored Nov 14, 2024
1 parent b0b73e5 commit c9ac6d4
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions ImportGraph/Cli.lean
Original file line number Diff line number Diff line change
Expand Up @@ -85,6 +85,7 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
| none => none
initSearchPath (← findSysroot)

Lean.enableInitializersExecution
let outFiles ← try unsafe withImportModules (to.map ({module := ·})) {} (trustLevel := 1024) fun env => do
let toModule := ImportGraph.getModule to[0]!
let mut graph := env.importGraph
Expand Down

0 comments on commit c9ac6d4

Please sign in to comment.