From e966ab85230885a8798408ccf468665db84b7506 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 18 Nov 2023 23:49:28 +0100
Subject: [PATCH] fix: we want to catch runtime exceptions in doc-gen4

---
 DocGen4/Load.lean                   | 1 +
 DocGen4/Process/Analyze.lean        | 5 +++--
 DocGen4/Process/DefinitionInfo.lean | 6 +-----
 3 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index c579837..6e1fc8a 100644
--- 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
index 932a34f..3e6600d 100644
--- 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
index 14cfdac..d0ce58e 100644
--- 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 =>