diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index 9c27f8f..2df73fd 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -14,10 +14,13 @@ def setSearchPath (path : List FilePath) : IO PUnit := do def load (imports : List Name) : IO (HashMap Name Module) := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty - let doc ← Prod.fst <$> (Meta.MetaM.toIO (process) {} { env := env} {} {}) + -- TODO parameterize maxHeartbeats + let doc ← Prod.fst <$> (Meta.MetaM.toIO (process) { maxHeartbeats := 100000000} { env := env} {} {}) for (_, module) in doc.toList do let s ← Core.CoreM.toIO module.prettyPrint {} { env := env } IO.println s.fst + IO.println s!"Processed {List.foldl (λ a (_, b) => a + b.members.size) 0 doc.toList} declarations" + IO.println s!"Processed {doc.size} modules" return doc end DocGen4 diff --git a/Main.lean b/Main.lean index 8a6c700..639455f 100644 --- a/Main.lean +++ b/Main.lean @@ -3,9 +3,9 @@ import Lean open DocGen4 Lean + def main : IO Unit := do -- This should be set by lake at some point setSearchPath ["/home/nix/Desktop/formal_verification/lean/mathlib4/build/lib", "/home/nix/.elan/toolchains/leanprover--lean4---nightly-2021-11-24/lib/lean"] let doc ← load [`Mathlib] - IO.println s!"Processed {doc.size} declarations" return ()