From a93ef145c5a8180864f0483dd10aa9ee143dc2a7 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Sat, 16 May 2026 16:33:34 +0000
Subject: [PATCH 1/3] fix: fail gracefully on missing exports

---
 Export.lean | 4 ++--
 Main.lean   | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Export.lean b/Export.lean
index 2054d47..b1167cd 100644
--- a/Export.lean
+++ b/Export.lean
@@ -232,7 +232,7 @@ partial def dumpExpr (e : Expr) : M Nat := do
 
 partial def dumpConstant (c : Name) : M Unit := do
   let some declar := (← read).env.find? c
-    | panic! s!"Constant {c} not found in environment."
+    | return
   if (declar.isUnsafe && !(← get).exportUnsafe) || (← get).visitedConstants.contains c then
     return
   modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
@@ -291,7 +291,7 @@ partial def dumpConstant (c : Name) : M Unit := do
     dumpConstant ``Eq
     for c in [`Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind] do
       let some (.quotInfo val) := (← read).env.find? c
-        | panic! s!"Constant {c} not found in environment."
+        | return
       modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
       dumpObj [
         ("quot", .mkObj [
diff --git a/Main.lean b/Main.lean
index 806fcf7..cccd24b 100644
--- a/Main.lean
+++ b/Main.lean
@@ -15,4 +15,4 @@ def main (args : List String) : IO Unit := do
     dumpMetadata
     for c in constants do
       modify (fun st => { st with noMDataExprs := {} })
-      dumpConstant c
+      try dumpConstant c catch _ => pure ()

From d17578b17b86a30986e4536284c32e90b9b52812 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Tue, 2 Jun 2026 14:14:49 +0000
Subject: [PATCH 2/3] Add `--ignore-missing` flag

---
 Export.lean | 10 ++++++----
 Main.lean   |  5 ++++-
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/Export.lean b/Export.lean
index b1167cd..e77a14f 100644
--- a/Export.lean
+++ b/Export.lean
@@ -40,6 +40,7 @@ structure State where
   noMDataExprs : HashMap Expr Expr := HashMap.emptyWithCapacity 100000
   exportMData : Bool := false
   exportUnsafe : Bool := false
+  ignoreMissing : Bool := false
   /-- Maps the name of an inductive type to a list of names of corresponding recursors.
   This is used to facilitate exporting of related inductives, constructors, and recursors as a unit. -/
   recursorMap : NameMap NameSet := {}
@@ -68,8 +69,9 @@ def initState (env : Environment) (cliOptions : List String := []) : M Unit := d
           | none => some <| NameSet.empty.insert recVal.name
           | some recNames => some <| recNames.insert recVal.name
   modify fun st => { st with
-    exportMData  := cliOptions.any  (· == "--export-mdata")
-    exportUnsafe := cliOptions.any (· == "--export-unsafe")
+    exportMData   := cliOptions.any (· == "--export-mdata")
+    exportUnsafe  := cliOptions.any (· == "--export-unsafe")
+    ignoreMissing := cliOptions.any (· == "--ignore-missing")
     recursorMap
   }
 
@@ -232,7 +234,7 @@ partial def dumpExpr (e : Expr) : M Nat := do
 
 partial def dumpConstant (c : Name) : M Unit := do
   let some declar := (← read).env.find? c
-    | return
+    | if (← get).ignoreMissing then return else panic! s!"Constant {c} not found in environment."
   if (declar.isUnsafe && !(← get).exportUnsafe) || (← get).visitedConstants.contains c then
     return
   modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
@@ -291,7 +293,7 @@ partial def dumpConstant (c : Name) : M Unit := do
     dumpConstant ``Eq
     for c in [`Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind] do
       let some (.quotInfo val) := (← read).env.find? c
-        | return
+        | if (← get).ignoreMissing then return else panic! s!"Constant {c} not found in environment."
       modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
       dumpObj [
         ("quot", .mkObj [
diff --git a/Main.lean b/Main.lean
index cccd24b..52bc5f0 100644
--- a/Main.lean
+++ b/Main.lean
@@ -15,4 +15,7 @@ def main (args : List String) : IO Unit := do
     dumpMetadata
     for c in constants do
       modify (fun st => { st with noMDataExprs := {} })
-      try dumpConstant c catch _ => pure ()
+      if (← get).ignoreMissing then
+        try dumpConstant c catch _ => pure ()
+      else
+        dumpConstant c

From bac0c8f9de385abc3d649578542422295b502292 Mon Sep 17 00:00:00 2001
From: Auguste Poiroux <augustepoiroux@gmail.com>
Date: Fri, 5 Jun 2026 09:31:29 +0000
Subject: [PATCH 3/3] Revert now useless try-catch block

---
 Main.lean | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/Main.lean b/Main.lean
index 52bc5f0..806fcf7 100644
--- a/Main.lean
+++ b/Main.lean
@@ -15,7 +15,4 @@ def main (args : List String) : IO Unit := do
     dumpMetadata
     for c in constants do
       modify (fun st => { st with noMDataExprs := {} })
-      if (← get).ignoreMissing then
-        try dumpConstant c catch _ => pure ()
-      else
-        dumpConstant c
+      dumpConstant c