From d2fddd7cff68994f790bfefa368cae8c34c38f0c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 1 Dec 2021 18:25:11 +0100
Subject: [PATCH] feat: Print count of declarations and modules processed

---
 DocGen4/Load.lean | 5 ++++-
 Main.lean         | 2 +-
 2 files changed, 5 insertions(+), 2 deletions(-)

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 ()