chore: fix the build

leanprover · Jun 7, 2024 · 4e570fe · 4e570fe
1 parent 1cae40a
commit 4e570fe
Show file tree

Hide file tree

Showing 4 changed files with 49 additions and 53 deletions.
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
@@ -36,7 +36,6 @@ 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
@@ -121,25 +121,30 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
     if !relevantModules.contains moduleName then
       continue
 
-    try
-      let config := {
-        maxHeartbeats := 5000000,
-        options := ← getOptions,
-        fileName := ← getFileName,
-        fileMap := ← getFileMap,
-        catchRuntimeEx := true,
-      }
-      let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
-      if let some dinfo := analysis then
-        let moduleName := env.allImportedModuleNames.get! modidx
-        let module := res.find! moduleName
-        res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
-    catch e =>
-      if let some pos := e.getRef.getPos? then
-        let pos := (← getFileMap).toPosition pos
-        IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}"
-      else
-        IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
+    res ← tryCatchRuntimeEx
+      (do
+        let config := {
+          maxHeartbeats := 5000000,
+          options := ← getOptions,
+          fileName := ← getFileName,
+          fileMap := ← getFileMap,
+        }
+        let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
+        if let some dinfo := analysis then
+          let moduleName := env.allImportedModuleNames.get! modidx
+          let module := res.find! moduleName
+          return res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
+        else
+          return res
+      )
+      (fun e => do
+        if let some pos := e.getRef.getPos? then
+          let pos := (← getFileMap).toPosition pos
+          IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}"
+        else
+          IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
+        return res
+      )
 
   -- TODO: This could probably be faster if we did sorted insert above instead
   for (moduleName, module) in res.toArray do

diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
@@ -32,43 +32,35 @@ def processEq (eq : Name) : MetaM CodeWithInfos := do
   let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
   stripArgs type prettyPrintTerm
 
+def computeEquations? (v : DefinitionVal) : MetaM (Array CodeWithInfos) := do
+  let eqs? ← getEqnsFor? v.name
+  match eqs? with
+  | some eqs =>
+    let eqs ← eqs.mapM processEq
+    return eqs
+  | none =>
+    let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
+    return equations
+
 def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let isUnsafe := v.safety == DefinitionSafety.unsafe
   let isNonComputable := isNoncomputable (← getEnv) v.name
 
-  try
-    let eqs? ← getEqnsFor? v.name
-
-    match eqs? with
-    | some eqs =>
-      let equations ← eqs.mapM processEq
-      return {
-        toInfo := info,
-        isUnsafe,
-        hints := v.hints,
-        equations,
-        isNonComputable
-      }
-    | none =>
-      let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
-      return {
-        toInfo := info,
-        isUnsafe,
-        hints := v.hints,
-        equations,
-        isNonComputable
-      }
-  catch err =>
-    IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
-    return {
-      toInfo := info,
-      isUnsafe,
-      hints := v.hints,
-      equations := none,
-      isNonComputable
-    }
+  let equations ←
+    tryCatchRuntimeEx
+      (.some <$> computeEquations? v)
+      (fun err => do
+        IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
+        return none)
 
+  return {
+    toInfo := info,
+    isUnsafe,
+    hints := v.hints,
+    equations,
+    isNonComputable
+  }
 
 
 end DocGen4.Process
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/xubaiw/CMark.lean",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "effd8b8771cfd7ece69db99448168078e113c61f",
+   "rev": "ef8b0ae5d48e7d5f5d538bf8d66f6cdc7daba296",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",