feat: Print count of declarations and modules processed
parent
54d7f92f2b
commit
d2fddd7cff
|
@ -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
|
||||
|
|
|
@ -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 ()
|
||||
|
|
Loading…
Reference in New Issue