fix: we want to catch runtime exceptions in doc-gen4

leanprover · Nov 18, 2023 · e966ab8 · e966ab8
1 parent d70b47c
commit e966ab8
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 7 deletions.
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
@@ -33,6 +33,7 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
     -- TODO: Figure out whether this could cause some bugs
     fileName := default,
     fileMap := default,
+    catchRuntimeEx := true,
   }
 
   Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}

diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean
@@ -123,10 +123,11 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
 
     try
       let config := {
-        maxHeartbeats := 50000000,
+        maxHeartbeats := 5000000,
         options := ← getOptions,
         fileName := ← getFileName,
-        fileMap := ← getFileMap
+        fileMap := ← getFileMap,
+        catchRuntimeEx := true,
       }
       let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
       if let some dinfo := analysis then

diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
@@ -38,11 +38,7 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
   let isNonComputable := isNoncomputable (← getEnv) v.name
 
   try
-    -- Temporary workaround until
-    -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/maxRecDepth.20in.20getEqnsFor.3F/near/402917295
-    -- is adddressed
-    let eqs? : Option (Array Name) := none
-    -- let eqs? ←  getEqnsFor? v.name
+    let eqs? ← getEqnsFor? v.name
 
     match eqs? with
     | some eqs =>