From 1062ff463ba12de5d3b8cdb5669ba544f24657f1 Mon Sep 17 00:00:00 2001
From: ammkrn <chris@christopherabailey.com>
Date: Thu, 27 Nov 2025 09:58:11 -0800
Subject: [PATCH] chore: Use ExceptT for error handling

As a triage to #8, adds some non-panic handling for the case where
a constant to be dumped by name is not found in the environment. This
should probably be considered an unrecoverable error in almost all
scenarios, so it simply throws and terminates with an error message
stating what declaration wasn't found, then terminates with a non-zero
error code (1).

For the other disallowed export items (mvar, fvar, mdata for now) which
are currently marked `unreachable`, they might as well be handled with
a little bit more information and similarly fail immediately.
---
 Export.lean    | 19 +++++++++++++------
 Main.lean      | 11 ++++++++---
 lean-toolchain |  2 +-
 3 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/Export.lean b/Export.lean
index 8a00d1c..5bef4ab 100644
--- a/Export.lean
+++ b/Export.lean
@@ -19,9 +19,9 @@ structure State where
   noMDataExprs : HashMap Expr Expr := {}
   exportUnsafe : Bool := false
 
-abbrev M := ReaderT Context <| StateT State IO
+abbrev M := ExceptT String <| ReaderT Context <| StateT State IO
 
-def M.run (env : Environment) (act : M α) : IO α :=
+def M.run (env : Environment) (act : M α) : IO (Except String α) :=
   StateT.run' (s := {}) do
     ReaderT.run (r := { env }) do
       act
@@ -46,7 +46,8 @@ def dumpName (n : Name) : M Nat := getIdx n (·.visitedNames) ({ · with visited
 
 def dumpLevel (l : Level) : M Nat := getIdx l (·.visitedLevels) ({ · with visitedLevels := · }) do
   match l with
-  | .zero | .mvar _ => unreachable!
+  | .zero => unreachable!
+  | .mvar _ => throw s!"level mvars may not be exported"
   | .succ l => return s!"#US {← dumpLevel l}"
   | .max l1 l2 => return s!"#UM {← dumpLevel l1} {← dumpLevel l2}"
   | .imax l1 l2 => return s!"#UIM {← dumpLevel l1} {← dumpLevel l2}"
@@ -71,7 +72,8 @@ def removeMData (e : Expr) : M Expr := do
     return x
   let e' ← match e with
   | .mdata _ e' => removeMData e'
-  | .fvar .. | .mvar ..=> unreachable!
+  | .fvar .. => throw "fvar found in removeMData; fvars may not be exported"
+  | .mvar ..=> throw "mvar found in removeMData; mvars may not be exported"
   | .bvar .. | .sort .. | .const .. | .lit _ => pure e
   | .app f a =>
     pure <| e.updateApp! (← removeMData f) (← removeMData a)
@@ -97,7 +99,9 @@ partial def dumpExprAux (e : Expr) : M Nat := do
     | .lam n d b bi => return s!"#EL {dumpInfo bi} {← dumpName n} {← dumpExprAux d} {← dumpExprAux b}"
     | .letE n d v b _ => return s!"#EZ {← dumpName n} {← dumpExprAux d} {← dumpExprAux v} {← dumpExprAux b}"
     | .forallE n d b bi => return s!"#EP {dumpInfo bi} {← dumpName n} {← dumpExprAux d} {← dumpExprAux b}"
-    | .mdata .. | .fvar .. | .mvar .. => unreachable!
+    | .mdata .. => throw "mdata found in dumpExprAux; mdata may not be exported"
+    | .fvar .. => throw "fvar found in dumpExprAux; fvars may not be exported"
+    | .mvar .. => throw "mvar found in dumpExprAux; mvars may not be exported"
     -- extensions compared to Lean 3
     | .proj s i e => return s!"#EJ {← dumpName s} {i} {← dumpExprAux e}"
     | .lit (.natVal i) => return s!"#ELN {i}"
@@ -117,7 +121,10 @@ def dumpUparams (uparams : List Name) : M (List Nat) := do
   pure nameIdxs
 
 partial def dumpConstant (c : Name) : M Unit := do
-  let declar := ((← read).env.find? c).get!
+  let declar ←
+    match ((← read).env.find? c) with
+    | none => throw s!"unable to find constant in current environment `{c}`"
+    | some d => pure d
   if (declar.isUnsafe && !(← get).exportUnsafe) || (← get).visitedConstants.contains c then
     return
   modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
diff --git a/Main.lean b/Main.lean
index 60d597d..7a9dea5 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,9 +1,9 @@
 import Export
 open Lean
 
-def semver := "2.0.0"
+def semver := "2.1.0"
 
-def main (args : List String) : IO Unit := do
+def main (args : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
   let (opts, args) := args.partition (fun s => s.startsWith "--" && s.length ≥ 3)
   let (imports, constants) := args.span (· != "--")
@@ -12,9 +12,14 @@ def main (args : List String) : IO Unit := do
   let constants := match constants.tail? with
     | some cs => cs.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get!
     | none    => env.constants.toList.map Prod.fst |>.filter (!·.isInternal)
-  M.run env do
+  let runResult ← M.run env do
     modify (fun st => { st with exportUnsafe := opts.any (· == "--export-unsafe") })
     IO.println semver
     for c in constants do
       modify (fun st => { st with noMDataExprs := {} })
       let _ ← dumpConstant c
+  match runResult with
+  | .ok _ => return 0
+  | e@(.error _) =>
+    IO.eprintln s!"{e}"
+    return 1
diff --git a/lean-toolchain b/lean-toolchain
index 9407130..7035713 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.25.0-rc2
+leanprover/lean4:v4.26.0-rc2
\ No newline at end of file