From ec1fd38ee4cb8770cf73e1f1164f6a1fb30f3557 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Wed, 29 Apr 2026 15:46:41 -0400
Subject: [PATCH 1/9] feat: add --help and --all-module-constants command line
 options

---
 Export.lean |  30 ++++++++--------
 Main.lean   | 101 +++++++++++++++++++++++++++++++++++++++++++++-------
 README.md   |  10 +++++-
 3 files changed, 112 insertions(+), 29 deletions(-)

diff --git a/Export.lean b/Export.lean
index 2054d47..457c4c2 100644
--- a/Export.lean
+++ b/Export.lean
@@ -29,7 +29,13 @@ def Lean.DefinitionSafety.toJson : DefinitionSafety → Json
 def Lean.KVMap.toJson (kvs: Lean.KVMap) : Json :=
   .mkObj <| kvs.entries.map (fun (k, v) => (k.toString, reprStr v))
 
+structure Flags where
+  printHelp : Bool := false
+  exportMData : Bool := false
+  exportUnsafe : Bool := false
+
 structure Context where
+  flags : Flags
   env : Environment
 
 structure State where
@@ -38,17 +44,15 @@ structure State where
   visitedExprs : HashMap Expr Nat := HashMap.emptyWithCapacity 10000000
   visitedConstants : NameHashSet := {}
   noMDataExprs : HashMap Expr Expr := HashMap.emptyWithCapacity 100000
-  exportMData : Bool := false
-  exportUnsafe : 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 := {}
 
 abbrev M := ReaderT Context <| StateT State IO
 
-def M.run (env : Environment) (act : M α) : IO α :=
+def M.run (flags : Flags) (env : Environment) (act : M α) : IO α :=
   StateT.run' (s := {}) do
-    ReaderT.run (r := { env }) do
+    ReaderT.run (r := { env, flags }) do
       act
 
 /--
@@ -58,7 +62,7 @@ of relevant recursors, which is used to ensure that for any inductive
 declaration, the inductives, constructors, and recursors are exported
 together in that order.
 -/
-def initState (env : Environment) (cliOptions : List String := []) : M Unit := do
+def initState (env : Environment) : M Unit := do
   let mut recursorMap : NameMap NameSet := {}
   for (_, constInfo) in env.constants do
     if let .recInfo recVal := constInfo then
@@ -67,11 +71,7 @@ def initState (env : Environment) (cliOptions : List String := []) : M Unit := d
           fun
           | 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")
-    recursorMap
-  }
+  modify fun st => { st with recursorMap }
 
 /--
 For a given primitive (name, level, expr) to be exported:
@@ -228,12 +228,12 @@ partial def dumpExpr (e : Expr) : M Nat := do
     let aux (e : Expr) : M Expr := do
       modify (fun st => { st with noMDataExprs := HashMap.emptyWithCapacity })
       removeMData e
-    dumpExprAux <| ← if (← get).exportMData then pure e else aux e
+    dumpExprAux <| ← if (← read).flags.exportMData then pure e else aux e
 
 partial def dumpConstant (c : Name) : M Unit := do
   let some declar := (← read).env.find? c
     | panic! s!"Constant {c} not found in environment."
-  if (declar.isUnsafe && !(← get).exportUnsafe) || (← get).visitedConstants.contains c then
+  if (declar.isUnsafe && !(← read).flags.exportUnsafe) || (← get).visitedConstants.contains c then
     return
   modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
   match declar with
@@ -307,12 +307,12 @@ partial def dumpConstant (c : Name) : M Unit := do
     let mut recursorNames := NameSet.empty
     for indName in baseIndVal.all do
       let val := ((← read).env.find? indName |>.get!).inductiveVal!
-      assert! ((!val.isUnsafe) || (← get).exportUnsafe)
+      assert! ((!val.isUnsafe) || (← read).flags.exportUnsafe)
       indVals := indVals.push val
       for ctor in val.ctors do
         match ((← read).env.find? ctor |>.get!) with
         | .ctorInfo ctorVal =>
-          assert! ((!ctorVal.isUnsafe) || (← get).exportUnsafe)
+          assert! ((!ctorVal.isUnsafe) || (← read).flags.exportUnsafe)
           ctorVals := ctorVals.push ctorVal
         | _ => panic! "Expected a `ConstantInfo.ctorInfo`."
       modify fun st => { st with visitedConstants:= st.visitedConstants.insert indName }
@@ -332,7 +332,7 @@ partial def dumpConstant (c : Name) : M Unit := do
     for recursorName in recursorNames do
       match ((← read).env.find? recursorName |>.get!) with
       | .recInfo recVal =>
-        assert! ((!recVal.isUnsafe) || (← get).exportUnsafe)
+        assert! ((!recVal.isUnsafe) || (← read).flags.exportUnsafe)
         recursorVals := recursorVals.push recVal
       | _ => panic! "expected a `constantinfo.recinfo`."
     for recursorVal in recursorVals do
diff --git a/Main.lean b/Main.lean
index 806fcf7..9c51127 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,18 +1,93 @@
 import Export
 open Lean
 
+/--
+Whether to export all constants, all the constants in the specified modules
+(including private and internal constants) or specific named constants.
+-/
+inductive ConstantExportSetting where
+  | all : ConstantExportSetting
+  | allInModules : ConstantExportSetting
+  | specificConstants : List Name → ConstantExportSetting
+
+structure Opts extends Flags where
+  modules : Array Name
+  constantExport : ConstantExportSetting
+
+def parseOpts : List String → Except String Opts := go {} #[] .none
+where
+  go (flags : Flags) (modules : Array Name) (constantExport : Option ConstantExportSetting) : List String → Except String Opts
+    | "--" :: rest => do
+      unless constantExport = .none do
+        throw s!"Cannot describe individual constants using `--` in combination with --all-module-constants"
+      let constants ← rest.mapM fun constant => do
+        let .some name := Syntax.decodeNameLit ("`" ++ constant)
+          | throw s!"Could not turn constant `{constant}` into an identifier"
+        return name
+      return ⟨flags, modules, .specificConstants constants⟩
+    | [] => .ok ⟨flags, modules, constantExport.getD .all⟩
+    | "-h" :: rest => go { flags with printHelp := true } modules constantExport rest
+    | "--help" :: rest => go { flags with printHelp := true } modules constantExport rest
+    | "--export-mdata" :: rest => go { flags with exportMData := true } modules constantExport rest
+    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules constantExport rest
+    | "-m" :: rest => do
+      unless constantExport = .none do
+        throw s!"Redundant or conflicting constant export settings"
+      go flags modules (.some .allInModules) rest
+    | "--all-module-constants" :: rest => do
+      unless constantExport = .none do
+        throw s!"Redundant or conflicting constant export settings"
+      go flags modules (.some .allInModules) rest
+    | mod :: rest => do
+      let .some name := Syntax.decodeNameLit ("`" ++ mod)
+        | throw s!"Could not turn module name `{mod}` to an identifier"
+      go flags (modules.push name) constantExport rest
+
+def usage := "usage: lean4export <modules> [-h | --help]
+                   [--export-mdata] [--export-unsafe]
+                   [-m | --all-module-constants | -- <constants>]"
+
+/--
+Get all suitable constants defined in a module
+-/
+def pickConstants (flags : Flags) (env : Environment) (mod: Name) : Array Name :=
+  let moduleIdx := env.getModuleIdx? mod |>.get!
+
+  -- Grab all constants from the module
+  let moduleData := env.header.moduleData[moduleIdx]!
+  moduleData.constants
+    |>.filterMap (fun const =>
+      -- include all non-internal constants AND constants that are non-internal but private
+      let constNameWithPrivateRemoved := const.name.components.filter (· != `_private)
+      if constNameWithPrivateRemoved.any (·.isInternal) then
+        .none
+      -- omit internal constants that are partial or unsafe
+      else if const.isUnsafe && not flags.exportUnsafe then
+        .none
+      else
+        .some const.name)
+
+
 def main (args : List String) : IO Unit := do
   initSearchPath (← findSysroot)
-  let (opts, args) := args.partition (fun s => s.startsWith "--" && s.length ≥ 3)
-  let (imports, constants) := args.span (· != "--")
-  let imports := imports.toArray.map fun mod => { module := Syntax.decodeNameLit ("`" ++ mod) |>.get! }
-  let env ← importModules imports {}
-  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 _ ← initState env opts
-    dumpMetadata
-    for c in constants do
-      modify (fun st => { st with noMDataExprs := {} })
-      dumpConstant c
+  match parseOpts args with
+  | .error msg => do
+    IO.eprintln s!"{msg}\n\n{usage}\n"
+    IO.Process.exit 1
+  | .ok ⟨flags, imports, constants⟩ => do
+    if flags.printHelp then
+      IO.eprintln usage
+      IO.Process.exit 0
+    let env ← importModules (imports.map ({ module := · })) {}
+    let constants := match constants with
+      | .all => env.constants.toList.map Prod.fst |>.filter (Name.isInternal · |> not)
+      | .allInModules => imports.foldl (init := NameSet.empty)
+          (fun set mod => pickConstants flags env mod |>.foldl (init := set) NameSet.insert)
+          |>.toList
+      | .specificConstants c => c
+    M.run flags env do
+      initState env
+      dumpMetadata
+      for c in constants do
+        modify (fun st => { st with noMDataExprs := {} })
+        dumpConstant c
diff --git a/README.md b/README.md
index e692109..fc725b8 100644
--- a/README.md
+++ b/README.md
@@ -20,10 +20,18 @@ We can invoke the exporter on the "top level" mathlib file and export mathlib wi
 ```sh
 lake env ../.lake/build/bin/lean4export Mathlib > out.ndjson
 ```
-This exports the contents of the given Lean module (here just the top level `Mathlib` module in the `Mathlib.lean` file), and its transitive dependencies. A specific list of declarations to be exported from these modules can be given after a separating `--`, and more than one module can be passed to the initial invocation by including more than one name (separted with a space).
+This exports the contents of the given Lean module (here just the top level `Mathlib` module in the `Mathlib.lean` file), and its transitive dependencies. 
+
+More than one module can be passed to the initial invocation by including more than one name (separated with a space).
 
 ### Options
 
 The option `--export-unsafe` can be used to include unsafe declarations in the export file. This may be useful for testing and debugging other tools, where unsafe declarations can serve as negative examples.
 
 The option `--export-mdata"` can be used to include `Expr.mdata` items in the export file, which are removed by default as they should not have an effect on type checking.
+
+By default, all constants in the environment are exported, except for those excluded by `--export-unsafe` or `--export-mdata`, are exported.
+To instead export only the constants directly mentioned in the specified modules (and their transitive dependencies), use option command `--all-module-constants`.
+Alternatively, to export specific set of constants (and their transitive dependencies), list them after the argument `--`, separated by spaces.
+
+The option `--help` prints usage information.
\ No newline at end of file

From 0889ad7ac0c9478370a8980e4d108d7703ab07e3 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 14:12:06 -0400
Subject: [PATCH 2/9] Change 'all constants' to the less fraught 'all theorems'

---
 Export.lean |  1 +
 Main.lean   | 79 +++++++++++++++++++++++++++++------------------------
 2 files changed, 45 insertions(+), 35 deletions(-)

diff --git a/Export.lean b/Export.lean
index 457c4c2..51219b6 100644
--- a/Export.lean
+++ b/Export.lean
@@ -31,6 +31,7 @@ def Lean.KVMap.toJson (kvs: Lean.KVMap) : Json :=
 
 structure Flags where
   printHelp : Bool := false
+  allModuleTheorems : Bool := true
   exportMData : Bool := false
   exportUnsafe : Bool := false
 
diff --git a/Main.lean b/Main.lean
index 9c51127..8224e73 100644
--- a/Main.lean
+++ b/Main.lean
@@ -7,65 +7,57 @@ Whether to export all constants, all the constants in the specified modules
 -/
 inductive ConstantExportSetting where
   | all : ConstantExportSetting
-  | allInModules : ConstantExportSetting
   | specificConstants : List Name → ConstantExportSetting
 
+/--
+Command line options for lean4export
+-/
 structure Opts extends Flags where
   modules : Array Name
   constantExport : ConstantExportSetting
 
-def parseOpts : List String → Except String Opts := go {} #[] .none
+def parseOpts : List String → Except String Opts := go {} #[]
 where
-  go (flags : Flags) (modules : Array Name) (constantExport : Option ConstantExportSetting) : List String → Except String Opts
+  go (flags : Flags) (modules : Array Name) : List String → Except String Opts
     | "--" :: rest => do
-      unless constantExport = .none do
-        throw s!"Cannot describe individual constants using `--` in combination with --all-module-constants"
       let constants ← rest.mapM fun constant => do
         let .some name := Syntax.decodeNameLit ("`" ++ constant)
           | throw s!"Could not turn constant `{constant}` into an identifier"
         return name
       return ⟨flags, modules, .specificConstants constants⟩
-    | [] => .ok ⟨flags, modules, constantExport.getD .all⟩
-    | "-h" :: rest => go { flags with printHelp := true } modules constantExport rest
-    | "--help" :: rest => go { flags with printHelp := true } modules constantExport rest
-    | "--export-mdata" :: rest => go { flags with exportMData := true } modules constantExport rest
-    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules constantExport rest
-    | "-m" :: rest => do
-      unless constantExport = .none do
-        throw s!"Redundant or conflicting constant export settings"
-      go flags modules (.some .allInModules) rest
-    | "--all-module-constants" :: rest => do
-      unless constantExport = .none do
-        throw s!"Redundant or conflicting constant export settings"
-      go flags modules (.some .allInModules) rest
+    | [] =>
+      -- If `--all-module-theorems` is set, just include module theorems
+      if flags.allModuleTheorems then
+        .ok ⟨flags, modules, .specificConstants []⟩
+      else
+        .ok ⟨flags, modules, .all⟩
+    | "-h" :: rest => go { flags with printHelp := true } modules rest
+    | "--help" :: rest => go { flags with printHelp := true } modules rest
+    | "--export-mdata" :: rest => go { flags with exportMData := true } modules rest
+    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules rest
+    | "--all-module-theorems" :: rest => do
+      go { flags with allModuleTheorems := true } modules rest
     | mod :: rest => do
       let .some name := Syntax.decodeNameLit ("`" ++ mod)
         | throw s!"Could not turn module name `{mod}` to an identifier"
-      go flags (modules.push name) constantExport rest
+      go flags (modules.push name) rest
 
 def usage := "usage: lean4export <modules> [-h | --help]
                    [--export-mdata] [--export-unsafe]
-                   [-m | --all-module-constants | -- <constants>]"
+                   [--all-module-theorems] [-- <constants>]"
 
 /--
 Get all suitable constants defined in a module
 -/
-def pickConstants (flags : Flags) (env : Environment) (mod: Name) : Array Name :=
+def pickConstants (env : Environment) (mod: Name) : Array Name :=
   let moduleIdx := env.getModuleIdx? mod |>.get!
 
   -- Grab all constants from the module
   let moduleData := env.header.moduleData[moduleIdx]!
   moduleData.constants
-    |>.filterMap (fun const =>
-      -- include all non-internal constants AND constants that are non-internal but private
-      let constNameWithPrivateRemoved := const.name.components.filter (· != `_private)
-      if constNameWithPrivateRemoved.any (·.isInternal) then
-        .none
-      -- omit internal constants that are partial or unsafe
-      else if const.isUnsafe && not flags.exportUnsafe then
-        .none
-      else
-        .some const.name)
+    |>.filterMap fun
+      | .thmInfo thm => .some thm.name
+      | _ => .none
 
 
 def main (args : List String) : IO Unit := do
@@ -78,13 +70,30 @@ def main (args : List String) : IO Unit := do
     if flags.printHelp then
       IO.eprintln usage
       IO.Process.exit 0
+
     let env ← importModules (imports.map ({ module := · })) {}
+
+    -- Determine what to export from the environment based on command-line options
+    let moduleTheorems : NameSet :=
+      if flags.allModuleTheorems then
+        imports.foldl (init := NameSet.empty) fun set mod =>
+          -- Get module data from environment
+          let moduleIdx := env.getModuleIdx? mod |>.get!
+          let moduleData := env.header.moduleData[moduleIdx]!
+
+          -- Read all theorems (NOTE: includes private/internal theorems)
+          let moduleTheorems := moduleData.constants
+            |>.filterMap fun
+              | .thmInfo thm => .some thm.name
+              | _ => .none
+          moduleTheorems.foldl (init := set) NameSet.insert
+      else
+        {}
     let constants := match constants with
       | .all => env.constants.toList.map Prod.fst |>.filter (Name.isInternal · |> not)
-      | .allInModules => imports.foldl (init := NameSet.empty)
-          (fun set mod => pickConstants flags env mod |>.foldl (init := set) NameSet.insert)
-          |>.toList
-      | .specificConstants c => c
+      | .specificConstants c => c ++ moduleTheorems.toList
+
+    -- Dump selected constants and all dependencies
     M.run flags env do
       initState env
       dumpMetadata

From 006dc35ba6b7da6bdf4f813e9c319d83721c7c82 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 18:11:35 -0400
Subject: [PATCH 3/9] Improve tests, readme

---
 Export.lean |  83 ++++++++++++++++++++++++++++++++-
 Main.lean   |  99 ++++++---------------------------------
 README.md   |  17 +++++--
 Test.lean   | 130 +++++++++++++++++++++++++++++++++++++++++++++++++++-
 4 files changed, 235 insertions(+), 94 deletions(-)

diff --git a/Export.lean b/Export.lean
index 51219b6..4666102 100644
--- a/Export.lean
+++ b/Export.lean
@@ -31,9 +31,9 @@ def Lean.KVMap.toJson (kvs: Lean.KVMap) : Json :=
 
 structure Flags where
   printHelp : Bool := false
-  allModuleTheorems : Bool := true
   exportMData : Bool := false
   exportUnsafe : Bool := false
+deriving Repr
 
 structure Context where
   flags : Flags
@@ -234,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
     | panic! s!"Constant {c} not found in environment."
-  if (declar.isUnsafe && !(← read).flags.exportUnsafe) || (← get).visitedConstants.contains c then
+  if (← get).visitedConstants.contains c then
     return
   modify fun st => { st with visitedConstants := st.visitedConstants.insert c }
   match declar with
@@ -435,3 +435,82 @@ def exportMetadata : Json :=
 
 def dumpMetadata : M Unit := do
   IO.println exportMetadata.compress
+
+/--
+A command-line mention of a module can instruct lean4export to load a module,
+or it can add all of the module's theorems to the root set of constants to
+export.
+-/
+structure Include where
+  name : Name
+  includeAllTheorems : Bool
+deriving Repr
+
+structure LeanExportOpts extends Flags where
+  modules : Array Include
+  constants : List Name
+deriving Repr
+
+def parseOpts : List String → Except String LeanExportOpts := go {} #[]
+where
+  go (flags : Flags) (modules : Array Include) : List String → Except String LeanExportOpts
+    | "--" :: [] =>
+      throw "The argument `--` must be followed by at least one constant"
+    | "--" :: rest => do
+      let constants ← rest.mapM fun constant => do
+        let .some name := Syntax.decodeNameLit ("`" ++ constant)
+          | throw s!"Could not turn constant `{constant}` into an identifier"
+        return name
+      return ⟨flags, modules, constants⟩
+    | [] =>
+      if modules.size = 0 && !flags.printHelp then
+        throw "At least one module must be specified"
+      else
+        return ⟨flags, modules, []⟩
+    | "-h" :: rest => go { flags with printHelp := true } modules rest
+    | "--help" :: rest => go { flags with printHelp := true } modules rest
+    | "--export-mdata" :: rest => go { flags with exportMData := true } modules rest
+    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules rest
+    | "--all-theorems" :: mod :: rest => do
+      let .some name := Syntax.decodeNameLit ("`" ++ mod)
+        | throw s!"Could not turn module name `{mod}` to an identifier"
+      go flags (modules.push ⟨name, true⟩) rest
+    | mod :: rest => do
+      let .some name := Syntax.decodeNameLit ("`" ++ mod)
+        | throw s!"Could not turn module name `{mod}` to an identifier"
+      go flags (modules.push ⟨name, false⟩) rest
+
+def LeanExportOpts.shouldExportEverything (opts : LeanExportOpts) : Bool :=
+  !opts.printHelp && opts.constants.length = 0 && opts.modules.all (not ·.includeAllTheorems)
+
+/--
+From a command line configuration, get the root set of constants that the
+export must support.
+-/
+def getRootConstants (env : Environment) (opts : LeanExportOpts) : List Name :=
+  if opts.shouldExportEverything then
+    -- Export "everything" for some value of everything
+    env.constants.toList.filterMap fun const =>
+      if const.fst.isInternal then
+        .none
+      else if !opts.exportUnsafe && const.snd.isUnsafe then
+        .none
+      else
+        .some const.fst
+
+  else
+    -- Export selected constants
+    opts.modules.filter (·.includeAllTheorems)
+      |>.map (·.name)
+      |>.foldl (β := NameSet) (init := NameSet.ofList opts.constants) (fun set mod =>
+        -- Get module data from environment
+        let moduleIdx := env.getModuleIdx? mod |>.get!
+        let moduleData := env.header.moduleData[moduleIdx]!
+
+        -- Read all theorems (NOTE: includes private/internal theorems)
+        let moduleTheorems := moduleData.constants
+          |>.filterMap fun
+            | .thmInfo thm => .some thm.name
+            | _ => .none
+        moduleTheorems.foldl (init := set) (fun set name => NameSet.insert set name))
+      |>.toList
diff --git a/Main.lean b/Main.lean
index 8224e73..500b7cf 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,102 +1,31 @@
 import Export
 open Lean
 
-/--
-Whether to export all constants, all the constants in the specified modules
-(including private and internal constants) or specific named constants.
--/
-inductive ConstantExportSetting where
-  | all : ConstantExportSetting
-  | specificConstants : List Name → ConstantExportSetting
+def usage := "Usage:
+  lean4export (-h | --help)
+  lean4export [--export-mdata] [--export-unsafe]
+              [MODULE_NAME]... [(--all-theorems MODULE_NAME)...]
+              [-- CONSTANT...]"
 
-/--
-Command line options for lean4export
--/
-structure Opts extends Flags where
-  modules : Array Name
-  constantExport : ConstantExportSetting
-
-def parseOpts : List String → Except String Opts := go {} #[]
-where
-  go (flags : Flags) (modules : Array Name) : List String → Except String Opts
-    | "--" :: rest => do
-      let constants ← rest.mapM fun constant => do
-        let .some name := Syntax.decodeNameLit ("`" ++ constant)
-          | throw s!"Could not turn constant `{constant}` into an identifier"
-        return name
-      return ⟨flags, modules, .specificConstants constants⟩
-    | [] =>
-      -- If `--all-module-theorems` is set, just include module theorems
-      if flags.allModuleTheorems then
-        .ok ⟨flags, modules, .specificConstants []⟩
-      else
-        .ok ⟨flags, modules, .all⟩
-    | "-h" :: rest => go { flags with printHelp := true } modules rest
-    | "--help" :: rest => go { flags with printHelp := true } modules rest
-    | "--export-mdata" :: rest => go { flags with exportMData := true } modules rest
-    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules rest
-    | "--all-module-theorems" :: rest => do
-      go { flags with allModuleTheorems := true } modules rest
-    | mod :: rest => do
-      let .some name := Syntax.decodeNameLit ("`" ++ mod)
-        | throw s!"Could not turn module name `{mod}` to an identifier"
-      go flags (modules.push name) rest
-
-def usage := "usage: lean4export <modules> [-h | --help]
-                   [--export-mdata] [--export-unsafe]
-                   [--all-module-theorems] [-- <constants>]"
-
-/--
-Get all suitable constants defined in a module
--/
-def pickConstants (env : Environment) (mod: Name) : Array Name :=
-  let moduleIdx := env.getModuleIdx? mod |>.get!
-
-  -- Grab all constants from the module
-  let moduleData := env.header.moduleData[moduleIdx]!
-  moduleData.constants
-    |>.filterMap fun
-      | .thmInfo thm => .some thm.name
-      | _ => .none
-
-
-def main (args : List String) : IO Unit := do
+def main (args : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
   match parseOpts args with
   | .error msg => do
     IO.eprintln s!"{msg}\n\n{usage}\n"
-    IO.Process.exit 1
-  | .ok ⟨flags, imports, constants⟩ => do
-    if flags.printHelp then
+    return 1
+  | .ok opts => do
+    if opts.printHelp then
       IO.eprintln usage
-      IO.Process.exit 0
-
-    let env ← importModules (imports.map ({ module := · })) {}
-
-    -- Determine what to export from the environment based on command-line options
-    let moduleTheorems : NameSet :=
-      if flags.allModuleTheorems then
-        imports.foldl (init := NameSet.empty) fun set mod =>
-          -- Get module data from environment
-          let moduleIdx := env.getModuleIdx? mod |>.get!
-          let moduleData := env.header.moduleData[moduleIdx]!
+      return 0
 
-          -- Read all theorems (NOTE: includes private/internal theorems)
-          let moduleTheorems := moduleData.constants
-            |>.filterMap fun
-              | .thmInfo thm => .some thm.name
-              | _ => .none
-          moduleTheorems.foldl (init := set) NameSet.insert
-      else
-        {}
-    let constants := match constants with
-      | .all => env.constants.toList.map Prod.fst |>.filter (Name.isInternal · |> not)
-      | .specificConstants c => c ++ moduleTheorems.toList
+    let env ← importModules (opts.modules.map ({ module := ·.name })) {}
+    let constants := getRootConstants env opts
 
     -- Dump selected constants and all dependencies
-    M.run flags env do
+    M.run opts.toFlags env do
       initState env
       dumpMetadata
       for c in constants do
         modify (fun st => { st with noMDataExprs := {} })
         dumpConstant c
+    return 0
diff --git a/README.md b/README.md
index fc725b8..5e259f2 100644
--- a/README.md
+++ b/README.md
@@ -20,7 +20,7 @@ We can invoke the exporter on the "top level" mathlib file and export mathlib wi
 ```sh
 lake env ../.lake/build/bin/lean4export Mathlib > out.ndjson
 ```
-This exports the contents of the given Lean module (here just the top level `Mathlib` module in the `Mathlib.lean` file), and its transitive dependencies. 
+This exports all contents of the given Lean module (here just the top level `Mathlib` module in the `Mathlib.lean` file), and all the contents of that module's transitive dependencies. 
 
 More than one module can be passed to the initial invocation by including more than one name (separated with a space).
 
@@ -30,8 +30,15 @@ The option `--export-unsafe` can be used to include unsafe declarations in the e
 
 The option `--export-mdata"` can be used to include `Expr.mdata` items in the export file, which are removed by default as they should not have an effect on type checking.
 
-By default, all constants in the environment are exported, except for those excluded by `--export-unsafe` or `--export-mdata`, are exported.
-To instead export only the constants directly mentioned in the specified modules (and their transitive dependencies), use option command `--all-module-constants`.
-Alternatively, to export specific set of constants (and their transitive dependencies), list them after the argument `--`, separated by spaces.
+The option `--help` prints usage information and then exits.
+
+The default behavior of exporting all constants can be modified by describing specific constants to export. Lean4export will import only those constants and their transitive dependencies.
+
+ * The argument `--all-theorems <ModuleName>` will include all theorems in a specific module.
+ * The argument `--` can be followed by a list of specific constants.
+
+As an example, this command will export only the constants necessary to support the theorem `EuclideanGeometry.dist_inversion_inversion` as well all the theorems in Mathlib's `Mathlib/Algebra/Module/NatInt.lean` module.
+```sh
+lake env ../.lake/build/bin/lean4export Mathlib --theorems-from Mathlib.Algebra.Module.NatInt -- EuclideanGeometry.dist_inversion_inversion
+```
 
-The option `--help` prints usage information.
\ No newline at end of file
diff --git a/Test.lean b/Test.lean
index 0394cfb..9db94dd 100644
--- a/Test.lean
+++ b/Test.lean
@@ -4,11 +4,11 @@ open Lean
 
 def run (act : M α) : MetaM Unit := do
   let env ← getEnv
-  let _ ← M.run env (do initState env; act)
+  let _ ← M.run {} env (do initState env; act)
 
 def runEmpty (act : M α) : MetaM Unit := do
   let env ← Lean.mkEmptyEnvironment
-  let _ ← M.run env (do initState env; act)
+  let _ ← M.run {} env (do initState env; act)
 
 /--
 info: {"in":1,"str":{"pre":0,"str":"foo"}}
@@ -721,3 +721,129 @@ literals
 #guard_msgs in
 #eval runParserTest do
   dumpConstant ``literals
+
+def runOpts (args : List String) : MetaM (Option (List Name) × LeanExportOpts) := do
+  let env ← getEnv
+  match parseOpts args with
+    | .error msg => throwError msg
+    | .ok opts =>
+      if opts.shouldExportEverything then
+        return ⟨.none, opts⟩
+      else
+        return ⟨.some <| getRootConstants env opts, opts⟩
+
+/-- error: Could not turn constant `bad const` into an identifier -/
+#guard_msgs in
+#eval runOpts ["--", "bad const"]
+
+/-- error: Could not turn constant `bad module` into an identifier -/
+#guard_msgs in
+#eval runOpts ["--", "bad module"]
+
+/-- error: At least one module must be specified -/
+#guard_msgs in
+#eval runOpts []
+
+/--
+info: (some [],
+ { toFlags := { printHelp := true, exportMData := false, exportUnsafe := false }, modules := #[], constants := [] })
+-/
+#guard_msgs in
+#eval runOpts ["-h"]
+
+/--
+info: (some [`PUnit],
+ { toFlags := { printHelp := false, exportMData := false, exportUnsafe := false },
+   modules := #[],
+   constants := [`PUnit] })
+-/
+#guard_msgs in
+#eval runOpts ["--", "PUnit"]
+
+/--
+info: (some [`bar, `baz, `foo],
+ { toFlags := { printHelp := false, exportMData := false, exportUnsafe := false },
+   modules := #[],
+   constants := [`foo, `bar, `baz] })
+-/
+#guard_msgs in
+#eval runOpts ["--", "foo", "bar", "baz"]
+
+/--
+info: (some [`PUnit],
+ { toFlags := { printHelp := false, exportMData := false, exportUnsafe := false },
+   modules := #[{ name := `Lean, includeAllTheorems := false }, { name := `Prelude, includeAllTheorems := false }],
+   constants := [`PUnit] })
+-/
+#guard_msgs in
+#eval runOpts ["Lean", "Prelude", "--", "PUnit"]
+
+/--
+info: (some [],
+ { toFlags := { printHelp := false, exportMData := false, exportUnsafe := false },
+   modules := #[{ name := `Lean, includeAllTheorems := true }],
+   constants := [] })
+-/
+#guard_msgs in
+#eval runOpts ["--all-theorems", "Lean"]
+
+/--
+info: (some [`Lean.DataValue.ofString.injEq,
+  `Lean.DataValue.ofInt.inj,
+  `Lean.DataValue.ofSyntax.sizeOf_spec,
+  `Lean.KVMap.mk.inj,
+  `Lean.DataValue.ofBool.sizeOf_spec,
+  `Lean.KVMap.mk.injEq,
+  `Lean.DataValue.ofSyntax.injEq,
+  `Lean.DataValue.ofNat.injEq,
+  `Lean.DataValue.ofName.injEq,
+  `Lean.DataValue.ofNat.sizeOf_spec,
+  `Lean.DataValue.ofInt.sizeOf_spec,
+  `Lean.DataValue.ofBool.inj,
+  `Lean.DataValue.ofNat.inj,
+  `Lean.DataValue.ofBool.injEq,
+  `Lean.DataValue.ofString.inj,
+  `Lean.DataValue.ofInt.injEq,
+  `Lean.KVMap.mk.sizeOf_spec,
+  `Lean.DataValue.ofSyntax.inj,
+  `Lean.DataValue.ofName.inj,
+  `Lean.DataValue.ofString.sizeOf_spec,
+  `Lean.DataValue.ofName.sizeOf_spec],
+ { toFlags := { printHelp := false, exportMData := false, exportUnsafe := false },
+   modules := #[{ name := `Lean, includeAllTheorems := false },
+                { name := `Lean.Data.KVMap, includeAllTheorems := true }],
+   constants := [] })
+-/
+#guard_msgs in
+#eval runOpts ["Lean", "--all-theorems", "Lean.Data.KVMap"]
+
+/--
+info: (some [`Lean.DataValue.ofString.injEq,
+  `Lean.DataValue.ofInt.inj,
+  `Lean.DataValue.ofSyntax.sizeOf_spec,
+  `Lean.KVMap.mk.inj,
+  `Lean.DataValue.ofBool.sizeOf_spec,
+  `Lean.KVMap.mk.injEq,
+  `Lean.DataValue.ofSyntax.injEq,
+  `Lean.DataValue.ofNat.injEq,
+  `Lean.DataValue.ofName.injEq,
+  `Lean.DataValue.ofNat.sizeOf_spec,
+  `Lean.DataValue.ofInt.sizeOf_spec,
+  `Lean.DataValue.ofBool.inj,
+  `Lean.DataValue.ofNat.inj,
+  `Lean.DataValue.ofBool.injEq,
+  `Lean.DataValue.ofString.inj,
+  `Lean.DataValue.ofInt.injEq,
+  `Lean.KVMap.mk.sizeOf_spec,
+  `Lean.DataValue.ofSyntax.inj,
+  `Lean.DataValue.ofName.inj,
+  `Lean.DataValue.ofString.sizeOf_spec,
+  `additionalConst,
+  `Lean.DataValue.ofName.sizeOf_spec],
+ { toFlags := { printHelp := false, exportMData := false, exportUnsafe := false },
+   modules := #[{ name := `Lean, includeAllTheorems := false },
+                { name := `Lean.Data.KVMap, includeAllTheorems := true }],
+   constants := [`additionalConst] })
+-/
+#guard_msgs in
+#eval runOpts ["Lean", "--all-theorems", "Lean.Data.KVMap", "--", "additionalConst"]

From 6cf134b771b3eedb147c301288264d0567f703b1 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 18:22:15 -0400
Subject: [PATCH 4/9] That comment wasn't enlightening

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

diff --git a/Main.lean b/Main.lean
index 500b7cf..73cc169 100644
--- a/Main.lean
+++ b/Main.lean
@@ -13,6 +13,7 @@ def main (args : List String) : IO UInt32 := do
   | .error msg => do
     IO.eprintln s!"{msg}\n\n{usage}\n"
     return 1
+
   | .ok opts => do
     if opts.printHelp then
       IO.eprintln usage
@@ -20,8 +21,6 @@ def main (args : List String) : IO UInt32 := do
 
     let env ← importModules (opts.modules.map ({ module := ·.name })) {}
     let constants := getRootConstants env opts
-
-    -- Dump selected constants and all dependencies
     M.run opts.toFlags env do
       initState env
       dumpMetadata
diff --git a/lakefile.toml b/lakefile.toml
index 2ec7011..9b0345e 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -8,6 +8,9 @@ name = "Export"
 [[lean_lib]]
 name = "Test"
 
+[[lean_lib]]
+name = "Foo"
+
 [[lean_exe]]
 name = "lean4export"
 root = "Main"

From e65525f90df395efaabdba27da2d9735078e8fd7 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 18:28:12 -0400
Subject: [PATCH 5/9] Refactor into more files

---
 Export.lean         | 86 +--------------------------------------------
 Export/CLIArgs.lean | 84 +++++++++++++++++++++++++++++++++++++++++++
 Export/Flags.lean   |  7 ++++
 Test.lean           |  1 +
 4 files changed, 93 insertions(+), 85 deletions(-)
 create mode 100644 Export/CLIArgs.lean
 create mode 100644 Export/Flags.lean

diff --git a/Export.lean b/Export.lean
index 4666102..775323a 100644
--- a/Export.lean
+++ b/Export.lean
@@ -1,4 +1,5 @@
 import Lean
+import Export.Flags
 import Std.Data.HashMap.Basic
 
 open Lean
@@ -29,12 +30,6 @@ def Lean.DefinitionSafety.toJson : DefinitionSafety → Json
 def Lean.KVMap.toJson (kvs: Lean.KVMap) : Json :=
   .mkObj <| kvs.entries.map (fun (k, v) => (k.toString, reprStr v))
 
-structure Flags where
-  printHelp : Bool := false
-  exportMData : Bool := false
-  exportUnsafe : Bool := false
-deriving Repr
-
 structure Context where
   flags : Flags
   env : Environment
@@ -435,82 +430,3 @@ def exportMetadata : Json :=
 
 def dumpMetadata : M Unit := do
   IO.println exportMetadata.compress
-
-/--
-A command-line mention of a module can instruct lean4export to load a module,
-or it can add all of the module's theorems to the root set of constants to
-export.
--/
-structure Include where
-  name : Name
-  includeAllTheorems : Bool
-deriving Repr
-
-structure LeanExportOpts extends Flags where
-  modules : Array Include
-  constants : List Name
-deriving Repr
-
-def parseOpts : List String → Except String LeanExportOpts := go {} #[]
-where
-  go (flags : Flags) (modules : Array Include) : List String → Except String LeanExportOpts
-    | "--" :: [] =>
-      throw "The argument `--` must be followed by at least one constant"
-    | "--" :: rest => do
-      let constants ← rest.mapM fun constant => do
-        let .some name := Syntax.decodeNameLit ("`" ++ constant)
-          | throw s!"Could not turn constant `{constant}` into an identifier"
-        return name
-      return ⟨flags, modules, constants⟩
-    | [] =>
-      if modules.size = 0 && !flags.printHelp then
-        throw "At least one module must be specified"
-      else
-        return ⟨flags, modules, []⟩
-    | "-h" :: rest => go { flags with printHelp := true } modules rest
-    | "--help" :: rest => go { flags with printHelp := true } modules rest
-    | "--export-mdata" :: rest => go { flags with exportMData := true } modules rest
-    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules rest
-    | "--all-theorems" :: mod :: rest => do
-      let .some name := Syntax.decodeNameLit ("`" ++ mod)
-        | throw s!"Could not turn module name `{mod}` to an identifier"
-      go flags (modules.push ⟨name, true⟩) rest
-    | mod :: rest => do
-      let .some name := Syntax.decodeNameLit ("`" ++ mod)
-        | throw s!"Could not turn module name `{mod}` to an identifier"
-      go flags (modules.push ⟨name, false⟩) rest
-
-def LeanExportOpts.shouldExportEverything (opts : LeanExportOpts) : Bool :=
-  !opts.printHelp && opts.constants.length = 0 && opts.modules.all (not ·.includeAllTheorems)
-
-/--
-From a command line configuration, get the root set of constants that the
-export must support.
--/
-def getRootConstants (env : Environment) (opts : LeanExportOpts) : List Name :=
-  if opts.shouldExportEverything then
-    -- Export "everything" for some value of everything
-    env.constants.toList.filterMap fun const =>
-      if const.fst.isInternal then
-        .none
-      else if !opts.exportUnsafe && const.snd.isUnsafe then
-        .none
-      else
-        .some const.fst
-
-  else
-    -- Export selected constants
-    opts.modules.filter (·.includeAllTheorems)
-      |>.map (·.name)
-      |>.foldl (β := NameSet) (init := NameSet.ofList opts.constants) (fun set mod =>
-        -- Get module data from environment
-        let moduleIdx := env.getModuleIdx? mod |>.get!
-        let moduleData := env.header.moduleData[moduleIdx]!
-
-        -- Read all theorems (NOTE: includes private/internal theorems)
-        let moduleTheorems := moduleData.constants
-          |>.filterMap fun
-            | .thmInfo thm => .some thm.name
-            | _ => .none
-        moduleTheorems.foldl (init := set) (fun set name => NameSet.insert set name))
-      |>.toList
diff --git a/Export/CLIArgs.lean b/Export/CLIArgs.lean
new file mode 100644
index 0000000..c31e29a
--- /dev/null
+++ b/Export/CLIArgs.lean
@@ -0,0 +1,84 @@
+module
+
+public import Lean
+public import Export.Flags
+open Lean
+
+/--
+A command-line mention of a module can instruct lean4export to load a module,
+or it can add all of the module's theorems to the root set of constants to
+export.
+-/
+public structure Include where
+  name : Name
+  includeAllTheorems : Bool
+deriving Repr
+
+public structure LeanExportOpts extends Flags where
+  modules : Array Include
+  constants : List Name
+deriving Repr
+
+public def parseOpts : List String → Except String LeanExportOpts := go {} #[]
+where
+  go (flags : Flags) (modules : Array Include) : List String → Except String LeanExportOpts
+    | "--" :: [] =>
+      throw "The argument `--` must be followed by at least one constant"
+    | "--" :: rest => do
+      let constants ← rest.mapM fun constant => do
+        let .some name := Syntax.decodeNameLit ("`" ++ constant)
+          | throw s!"Could not turn constant `{constant}` into an identifier"
+        return name
+      return ⟨flags, modules, constants⟩
+    | [] =>
+      if modules.size = 0 && !flags.printHelp then
+        throw "At least one module must be specified"
+      else
+        return ⟨flags, modules, []⟩
+    | "-h" :: rest => go { flags with printHelp := true } modules rest
+    | "--help" :: rest => go { flags with printHelp := true } modules rest
+    | "--export-mdata" :: rest => go { flags with exportMData := true } modules rest
+    | "--export-unsafe" :: rest => go { flags with exportUnsafe := true } modules rest
+    | "--all-theorems" :: mod :: rest => do
+      let .some name := Syntax.decodeNameLit ("`" ++ mod)
+        | throw s!"Could not turn module name `{mod}` to an identifier"
+      go flags (modules.push ⟨name, true⟩) rest
+    | mod :: rest => do
+      let .some name := Syntax.decodeNameLit ("`" ++ mod)
+        | throw s!"Could not turn module name `{mod}` to an identifier"
+      go flags (modules.push ⟨name, false⟩) rest
+
+public def LeanExportOpts.shouldExportEverything (opts : LeanExportOpts) : Bool :=
+  !opts.printHelp && opts.constants.length = 0 && opts.modules.all (not ·.includeAllTheorems)
+
+/--
+From a command line configuration, get the root set of constants that the
+export must support.
+-/
+public def getRootConstants (env : Environment) (opts : LeanExportOpts) : List Name :=
+  if opts.shouldExportEverything then
+    -- Export "everything" for some value of everything
+    env.constants.toList.filterMap fun const =>
+      if const.fst.isInternal then
+        .none
+      else if !opts.exportUnsafe && const.snd.isUnsafe then
+        .none
+      else
+        .some const.fst
+
+  else
+    -- Export selected constants
+    opts.modules.filter (·.includeAllTheorems)
+      |>.map (·.name)
+      |>.foldl (β := NameSet) (init := NameSet.ofList opts.constants) (fun set mod =>
+        -- Get module data from environment
+        let moduleIdx := env.getModuleIdx? mod |>.get!
+        let moduleData := env.header.moduleData[moduleIdx]!
+
+        -- Read all theorems (NOTE: includes private/internal theorems)
+        let moduleTheorems := moduleData.constants
+          |>.filterMap fun
+            | .thmInfo thm => .some thm.name
+            | _ => .none
+        moduleTheorems.foldl (init := set) (fun set name => NameSet.insert set name))
+      |>.toList
diff --git a/Export/Flags.lean b/Export/Flags.lean
new file mode 100644
index 0000000..4525438
--- /dev/null
+++ b/Export/Flags.lean
@@ -0,0 +1,7 @@
+module
+
+public structure Flags where
+  printHelp : Bool := false
+  exportMData : Bool := false
+  exportUnsafe : Bool := false
+deriving Repr
diff --git a/Test.lean b/Test.lean
index 9db94dd..8b4d295 100644
--- a/Test.lean
+++ b/Test.lean
@@ -1,4 +1,5 @@
 import Export
+import Export.CLIArgs
 import Export.Parse
 open Lean
 

From ffe54d8c8f7e975df38de3e91ae1447407874989 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 18:28:56 -0400
Subject: [PATCH 6/9] docstring

---
 Export/CLIArgs.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Export/CLIArgs.lean b/Export/CLIArgs.lean
index c31e29a..77f2f0a 100644
--- a/Export/CLIArgs.lean
+++ b/Export/CLIArgs.lean
@@ -52,8 +52,8 @@ public def LeanExportOpts.shouldExportEverything (opts : LeanExportOpts) : Bool
   !opts.printHelp && opts.constants.length = 0 && opts.modules.all (not ·.includeAllTheorems)
 
 /--
-From a command line configuration, get the root set of constants that the
-export must support.
+From a command line configuration, gets the root set of constants that the
+exported environment must support.
 -/
 public def getRootConstants (env : Environment) (opts : LeanExportOpts) : List Name :=
   if opts.shouldExportEverything then

From be1a1bb33c8714abc78b23b10754ffa4343ba972 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 18:29:22 -0400
Subject: [PATCH 7/9] typo

---
 lakefile.toml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/lakefile.toml b/lakefile.toml
index 9b0345e..2ec7011 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -8,9 +8,6 @@ name = "Export"
 [[lean_lib]]
 name = "Test"
 
-[[lean_lib]]
-name = "Foo"
-
 [[lean_exe]]
 name = "lean4export"
 root = "Main"

From 28fb520a65402d31bc20ca476646697f48d8795b Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 18:31:39 -0400
Subject: [PATCH 8/9] Add import

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

diff --git a/Main.lean b/Main.lean
index 73cc169..518196a 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,4 +1,5 @@
 import Export
+import Export.CLIArgs
 open Lean
 
 def usage := "Usage:

From b34b61bacb6523d469eaf7e814c6b5cf576ceab1 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Thu, 30 Apr 2026 22:08:57 -0400
Subject: [PATCH 9/9] better error message

---
 Main.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/Main.lean b/Main.lean
index 518196a..d3fa89d 100644
--- a/Main.lean
+++ b/Main.lean
@@ -5,7 +5,7 @@ open Lean
 def usage := "Usage:
   lean4export (-h | --help)
   lean4export [--export-mdata] [--export-unsafe]
-              [MODULE_NAME]... [(--all-theorems MODULE_NAME)...]
+              [MODULE_NAME...] [(--all-theorems MODULE_NAME)...]
               [-- CONSTANT...]"
 
 def main (args : List String) : IO UInt32 := do
@@ -21,7 +21,16 @@ def main (args : List String) : IO UInt32 := do
       return 0
 
     let env ← importModules (opts.modules.map ({ module := ·.name })) {}
+    let missingConstants ← opts.constants.filterM fun name => do
+      if env.constants.contains name then
+        return false
+      IO.eprintln s!"Required constant {name} not found in environment"
+      return true
+    if missingConstants.length > 0 then
+      return 1
+
     let constants := getRootConstants env opts
+
     M.run opts.toFlags env do
       initState env
       dumpMetadata