diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index a6774aff3d..a69bcd6e5c 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -95,6 +95,22 @@ instance : FromJson Name where
 instance : ToJson Name where
   toJson n := toString n
 
+instance [FromJson α] : FromJson (NameMap α) where
+  fromJson?
+    | .obj obj => obj.foldM (init := {}) fun m k v => do
+      if k == "[anonymous]" then
+        return m.insert .anonymous (← fromJson? v)
+      else
+        let n := k.toName
+        if n.isAnonymous then
+          throw s!"expected a `Name`, got '{k}'"
+        else
+          return m.insert n (← fromJson? v)
+    | j => throw s!"expected a `NameMap`, got '{j}'"
+
+instance [ToJson α] : ToJson (NameMap α) where
+  toJson m := Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf
+
 /-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript
 cannot represent 64-bit numbers. -/
 def bignumFromJson? (j : Json) : Except String Nat := do
diff --git a/src/Lean/Data/NameMap.lean b/src/Lean/Data/NameMap.lean
index eed36180e1..67fa15bf75 100644
--- a/src/Lean/Data/NameMap.lean
+++ b/src/Lean/Data/NameMap.lean
@@ -18,6 +18,8 @@ def NameMap (α : Type) := RBMap Name α Name.quickCmp
 namespace NameMap
 variable {α : Type}
 
+instance [Repr α] : Repr (NameMap α) := inferInstanceAs (Repr (RBMap Name α Name.quickCmp))
+
 instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩
 
 instance (α : Type) : Inhabited (NameMap α) where
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 1ad2e54c58..2bcab8d314 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -145,6 +145,7 @@ def runFrontend
     (errorOnKinds : Array Name := #[])
     (plugins : Array System.FilePath := #[])
     (printStats : Bool := false)
+    (setupFileName? : Option System.FilePath := none)
     : IO (Option Environment) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
@@ -152,8 +153,28 @@ def runFrontend
   -- default to async elaboration; see also `Elab.async` docs
   let opts := Elab.async.setIfNotSet opts true
   let ctx := { inputCtx with }
+  let setup stx := do
+    if let some file := setupFileName? then
+      let setup ← ModuleSetup.load file
+      liftM <| setup.dynlibs.forM Lean.loadDynlib
+      return .ok {
+        trustLevel
+        mainModuleName := setup.name
+        isModule := setup.isModule
+        imports := setup.imports
+        plugins := plugins ++ setup.plugins
+        modules := setup.modules
+        -- override cmdline options with header options
+        opts := opts.mergeBy (fun _ _ hOpt => hOpt) setup.options.toOptions
+      }
+    else
+      return .ok {
+        imports := stx.imports
+        isModule := stx.isModule
+        mainModuleName, opts, trustLevel, plugins
+      }
   let processor := Language.Lean.process
-  let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel, plugins }) none ctx
+  let snap ← processor setup none ctx
   let snaps := Language.toSnapshotTree snap
   let severityOverrides := errorOnKinds.foldl (·.insert · .error) {}
 
diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index 1dbfbf7e94..4454bf1e69 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -10,7 +10,15 @@ import Lean.CoreM
 
 namespace Lean.Elab
 
-def headerToImports : TSyntax ``Parser.Module.header → Array Import
+abbrev HeaderSyntax := TSyntax ``Parser.Module.header
+
+def HeaderSyntax.startPos (header : HeaderSyntax) : String.Pos :=
+  header.raw.getPos?.getD 0
+
+def HeaderSyntax.isModule (header : HeaderSyntax) : Bool :=
+  !header.raw[0].isNone
+
+def HeaderSyntax.imports : HeaderSyntax → Array Import
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
     let imports := if preludeTk.isNone then #[{ module := `Init : Import }] else #[]
     imports ++ importsStx.map fun
@@ -19,17 +27,14 @@ def headerToImports : TSyntax ``Parser.Module.header → Array Import
       | _ => unreachable!
   | _ => unreachable!
 
-/--
-Elaborates the given header syntax into an environment.
+abbrev headerToImports := @HeaderSyntax.imports
 
-If `mainModule` is not given, `Environment.setMainModule` should be called manually. This is a
-backwards compatibility measure not compatible with the module system.
--/
-def processHeader (header : TSyntax ``Parser.Module.header) (opts : Options) (messages : MessageLog)
-    (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0)
-    (plugins : Array System.FilePath := #[]) (leakEnv := false) (mainModule := Name.anonymous)
+def processHeaderCore
+    (startPos : String.Pos) (imports : Array Import) (isModule : Bool)
+    (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
+    (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
+    (mainModule := Name.anonymous) (arts : NameMap ModuleArtifacts := {})
     : IO (Environment × MessageLog) := do
-  let isModule := !header.raw[0].isNone
   let level := if isModule then
     if Elab.inServer.get opts then
       .server
@@ -38,7 +43,6 @@ def processHeader (header : TSyntax ``Parser.Module.header) (opts : Options) (me
   else
     .private
   let (env, messages) ← try
-    let imports := headerToImports header
     for i in imports do
       if !isModule && i.importAll then
         throw <| .userError "cannot use `import all` without `module`"
@@ -47,15 +51,30 @@ def processHeader (header : TSyntax ``Parser.Module.header) (opts : Options) (me
       if !isModule && !i.isExported then
         throw <| .userError "cannot use `private import` without `module`"
     let env ←
-      importModules (leakEnv := leakEnv) (loadExts := true) (level := level) imports opts trustLevel plugins
+      importModules (leakEnv := leakEnv) (loadExts := true) (level := level)
+        imports opts trustLevel plugins arts
     pure (env, messages)
   catch e =>
     let env ← mkEmptyEnvironment
-    let spos := header.raw.getPos?.getD 0
-    let pos  := inputCtx.fileMap.toPosition spos
+    let pos := inputCtx.fileMap.toPosition startPos
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
   return (env.setMainModule mainModule, messages)
 
+/--
+Elaborates the given header syntax into an environment.
+
+If `mainModule` is not given, `Environment.setMainModule` should be called manually. This is a
+backwards compatibility measure not compatible with the module system.
+-/
+@[inline] def processHeader
+    (header : HeaderSyntax)
+    (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
+    (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
+    (mainModule := Name.anonymous)
+    : IO (Environment × MessageLog) := do
+  processHeaderCore header.startPos header.imports header.isModule
+    opts messages inputCtx trustLevel plugins leakEnv mainModule
+
 def parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog) := do
   let fileName := fileName.getD "<input>"
   let inputCtx := Parser.mkInputContext input fileName
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index a2a7691b25..0c1f9d1130 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -11,6 +11,7 @@ import Init.System.Promise
 import Lean.ImportingFlag
 import Lean.Data.NameTrie
 import Lean.Data.SMap
+import Lean.Setup
 import Lean.Declaration
 import Lean.LocalContext
 import Lean.Util.Path
@@ -93,18 +94,6 @@ instance : GetElem? (Array α) ModuleIdx α (fun a i => i.toNat < a.size) where
 
 abbrev ConstMap := SMap Name ConstantInfo
 
-structure Import where
-  module        : Name
-  /-- `import all`; whether to import and expose all data saved by the module. -/
-  importAll : Bool := false
-  /-- Whether to activate this import when the current module itself is imported. -/
-  isExported    : Bool := true
-  deriving Repr, Inhabited
-
-instance : Coe Name Import := ⟨({module := ·})⟩
-
-instance : ToString Import := ⟨fun imp => toString imp.module⟩
-
 /--
   A compacted region holds multiple Lean objects in a contiguous memory region, which can be read/written to/from disk.
   Objects inside the region do not have reference counters and cannot be freed individually. The contents of .olean
@@ -1794,7 +1783,35 @@ abbrev ImportStateM := StateRefT ImportState IO
 @[inline] nonrec def ImportStateM.run (x : ImportStateM α) (s : ImportState := {}) : IO (α × ImportState) :=
   x.run s
 
-partial def importModulesCore (imports : Array Import) (forceImportAll := true) :
+def ModuleArtifacts.oleanParts (arts : ModuleArtifacts) : Array System.FilePath := Id.run do
+  let mut fnames := #[]
+  -- Opportunistically load all available parts.
+  -- Producer (e.g., Lake) should limit parts to the proper import level.
+  if let some mFile := arts.olean? then
+    fnames := fnames.push mFile
+    if let some sFile := arts.oleanServer? then
+      fnames := fnames.push sFile
+      if let some pFile := arts.oleanPrivate? then
+        fnames := fnames.push pFile
+  return fnames
+
+private def findOLeanParts (mod : Name) : IO (Array System.FilePath) := do
+  let mFile ← findOLean mod
+  unless (← mFile.pathExists) do
+    throw <| IO.userError s!"object file '{mFile}' of module {mod} does not exist"
+  let mut fnames := #[mFile]
+  -- Opportunistically load all available parts.
+  -- Necessary because the import level may be upgraded a later import.
+  let sFile := OLeanLevel.server.adjustFileName mFile
+  if (← sFile.pathExists) then
+    fnames := fnames.push sFile
+    let pFile := OLeanLevel.private.adjustFileName mFile
+    if (← pFile.pathExists) then
+      fnames := fnames.push pFile
+  return fnames
+
+partial def importModulesCore
+    (imports : Array Import) (forceImportAll := true) (arts : NameMap ModuleArtifacts := {}) :
     ImportStateM Unit := go
 where go := do
   for i in imports do
@@ -1811,19 +1828,14 @@ where go := do
           if let some mod := mod.mainModule? then
             importModulesCore (forceImportAll := true) mod.imports
       continue
-    let mFile ← findOLean i.module
-    unless (← mFile.pathExists) do
-      throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist"
-    let mut fnames := #[mFile]
-    -- opportunistically load all available parts in case `importPrivate` is upgraded by a later
-    -- import
-    -- TODO: use Lake data to retrieve ultimate import level immediately
-    let sFile := OLeanLevel.server.adjustFileName mFile
-    if (← sFile.pathExists) then
-      fnames := fnames.push sFile
-      let pFile := OLeanLevel.private.adjustFileName mFile
-      if (← pFile.pathExists) then
-        fnames := fnames.push pFile
+    let fnames ←
+      if let some arts := arts.find? i.module then
+        let fnames := arts.oleanParts
+        if fnames.isEmpty then
+          findOLeanParts i.module
+        else pure fnames
+      else
+        findOLeanParts i.module
     let parts ← readModuleDataParts fnames
     -- `imports` is identical for each part
     let some (baseMod, _) := parts[0]? | unreachable!
@@ -1995,13 +2007,14 @@ as if no `module` annotations were present in the imports.
 -/
 def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0)
     (plugins : Array System.FilePath := #[]) (leakEnv := false) (loadExts := false)
-    (level := OLeanLevel.private) : IO Environment := profileitIO "import" opts do
+    (level := OLeanLevel.private) (arts : NameMap ModuleArtifacts := {})
+    : IO Environment := profileitIO "import" opts do
   for imp in imports do
     if imp.module matches .anonymous then
       throw <| IO.userError "import failed, trying to import module with anonymous name"
   withImporting do
     plugins.forM Lean.loadPlugin
-    let (_, s) ← importModulesCore (forceImportAll := level == .private) imports |>.run
+    let (_, s) ← importModulesCore (forceImportAll := level == .private) imports arts |>.run
     finalizeImport (leakEnv := leakEnv) (loadExts := loadExts) (level := level)
       s imports opts trustLevel
 
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index d448b58bd8..2f2525a304 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -283,10 +283,16 @@ simple uses, these can be computed eagerly without looking at the imports.
 structure SetupImportsResult where
   /-- Module name of the file being processed. -/
   mainModuleName : Name
+  /-- Whether the file is participating in the module system. -/
+  isModule : Bool := false
+  /-- Direct imports of the file being processed. -/
+  imports : Array Import
   /-- Options provided outside of the file content, e.g. on the cmdline or in the lakefile. -/
   opts : Options
   /-- Kernel trust level. -/
   trustLevel : UInt32 := 0
+  /-- Pre-resolved artifacts of related modules (e.g., this module's transitive imports). -/
+  modules : NameMap ModuleArtifacts := {}
   /-- Lean plugins to load as part of the environment setup. -/
   plugins : Array System.FilePath := #[]
 
@@ -367,7 +373,7 @@ General notes:
   the `sync` parameter on `parseCmd` and spawn an elaboration task when we leave it.
 -/
 partial def process
-    (setupImports : TSyntax ``Parser.Module.header → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
+    (setupImports : HeaderSyntax → ProcessingT IO (Except HeaderProcessedSnapshot SetupImportsResult))
     (old? : Option InitialSnapshot) : ProcessingM InitialSnapshot := do
   parseHeader old? |>.run (old?.map (·.ictx))
 where
@@ -453,7 +459,7 @@ where
         }
       }
 
-  processHeader (stx : TSyntax ``Parser.Module.header) (parserState : Parser.ModuleParserState) :
+  processHeader (stx : HeaderSyntax) (parserState : Parser.ModuleParserState) :
       LeanProcessingM (SnapshotTask HeaderProcessedSnapshot) := do
     let ctx ← read
     SnapshotTask.ofIO stx none (some ⟨0, ctx.input.endPos⟩) <|
@@ -471,9 +477,9 @@ where
       if !stx.raw[0].isNone && !experimental.module.get opts then
         throw <| IO.Error.userError "`module` keyword is experimental and not enabled here"
       -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
-      let (headerEnv, msgLog) ← Elab.processHeader (leakEnv := true)
-        (mainModule := setup.mainModuleName) stx opts .empty ctx.toInputContext setup.trustLevel
-        setup.plugins
+      let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
+        stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext
+        setup.trustLevel setup.plugins setup.mainModuleName setup.modules
       let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index c300ffdfb6..5984689812 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -417,6 +417,7 @@ def setupImports
 
   return .ok {
     mainModuleName := meta.mod
+    imports
     opts
     plugins := fileSetupResult.plugins
   }
diff --git a/src/Lean/Setup.lean b/src/Lean/Setup.lean
new file mode 100644
index 0000000000..34a031556c
--- /dev/null
+++ b/src/Lean/Setup.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mac Malone
+-/
+prelude
+import Lean.Data.Json
+import Lean.Util.LeanOptions
+
+/-!
+# Module Setup Information
+
+Data types used by Lean module headers and the `--setup` CLI.
+-/
+
+namespace Lean
+
+structure Import where
+  module        : Name
+  /-- `import all`; whether to import and expose all data saved by the module. -/
+  importAll : Bool := false
+  /-- Whether to activate this import when the current module itself is imported. -/
+  isExported    : Bool := true
+  deriving Repr, Inhabited, ToJson, FromJson
+
+instance : Coe Name Import := ⟨({module := ·})⟩
+
+instance : ToString Import := ⟨fun imp => toString imp.module⟩
+
+/-- Files containing data for a single module. -/
+structure ModuleArtifacts where
+  lean? : Option System.FilePath := none
+  olean? : Option System.FilePath := none
+  oleanServer? : Option System.FilePath := none
+  oleanPrivate? : Option System.FilePath := none
+  ilean? : Option System.FilePath := none
+  deriving Repr, Inhabited, ToJson, FromJson
+
+/--
+A module's setup information as described by a JSON file.
+Supercedes the module's header when the `--setup` CLI option is used.
+-/
+structure ModuleSetup where
+  /-- Name of the module. -/
+  name : Name
+  /-- Whether the module is participating in the module system. -/
+  isModule : Bool := false
+  /- The module's direct imports. -/
+  imports : Array Import := #[]
+  /-- Pre-resolved artifacts of related modules (e.g., this module's transitive imports). -/
+  modules : NameMap ModuleArtifacts := {}
+  /-- Dynamic libraries to load with the module. -/
+  dynlibs : Array System.FilePath := #[]
+  /-- Plugins to initialize with the module. -/
+  plugins : Array System.FilePath := #[]
+  /-- Additional options for the module. -/
+  options : LeanOptions := {}
+  deriving Repr, Inhabited, ToJson, FromJson
+
+/-- Load a `ModuleSetup` from a JSON file. -/
+def ModuleSetup.load (path : System.FilePath) : IO ModuleSetup := do
+  let contents ← IO.FS.readFile path
+  match Json.parse contents >>= fromJson? with
+  | .ok info => pure info
+  | .error msg => throw <| IO.userError s!"failed to load header from {path}: {msg}"
diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean
index 9fe332f7dd..cc369f172b 100644
--- a/src/Lean/Util/LeanOptions.lean
+++ b/src/Lean/Util/LeanOptions.lean
@@ -60,9 +60,11 @@ def LeanOptionValue.asCliFlagValue : (v : LeanOptionValue) → String
 
 /-- Options that are used by Lean as if they were passed using `-D`. -/
 structure LeanOptions where
-  values : RBMap Name LeanOptionValue Name.cmp
+  values : NameMap LeanOptionValue
   deriving Inhabited, Repr
 
+instance : EmptyCollection LeanOptions := ⟨⟨∅⟩⟩
+
 def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do
   let mut options := KVMap.empty
   for ⟨name, optionValue⟩ in leanOptions.values do
@@ -77,17 +79,9 @@ def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do
   return ⟨values⟩
 
 instance : FromJson LeanOptions where
-  fromJson?
-    | Json.obj obj => do
-      let values ← obj.foldM (init := RBMap.empty) fun acc k v => do
-        let optionValue ← fromJson? v
-        return acc.insert k.toName optionValue
-      return ⟨values⟩
-    | _ => Except.error "invalid LeanOptions type"
+  fromJson? j := LeanOptions.mk <$> fromJson? j
 
 instance : ToJson LeanOptions where
-  toJson options :=
-    Json.obj <| options.values.fold (init := RBNode.leaf) fun acc k v =>
-      acc.insert (cmp := compare) k.toString (toJson v)
+  toJson options := toJson options.values
 
 end Lean
diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean
index 1dbf3c8b82..ee58ebc93c 100644
--- a/src/lake/Lake/Util/Name.lean
+++ b/src/lake/Lake/Util/Name.lean
@@ -35,18 +35,6 @@ abbrev OrdNameMap α := RBArray Name α Name.quickCmp
 abbrev DNameMap α := DRBMap Name α Name.quickCmp
 @[inline] def DNameMap.empty : DNameMap α := DRBMap.empty
 
-instance [ToJson α] : ToJson (NameMap α) where
-  toJson m := Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf
-
-instance [FromJson α] : FromJson (NameMap α) where
-  fromJson? j := do
-    (← j.getObj?).foldM (init := {}) fun m k v =>
-      let k := k.toName
-      if k.isAnonymous then
-        throw "expected name"
-      else
-        return m.insert k (← fromJson? v)
-
 /-! # Name Helpers -/
 
 namespace Name
diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index ab1345c97e..308ecc0430 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -223,6 +223,7 @@ static void display_help(std::ostream & out) {
 #endif
     std::cout << "      --plugin=file      load and initialize Lean shared library for registering linters etc.\n";
     std::cout << "      --load-dynlib=file load shared library to make its symbols available to the interpreter\n";
+    std::cout << "      --setup=file       JSON file with module setup data (supersedes the file's header)\n";
     std::cout << "      --json             report Lean output (e.g., messages) as JSON (one per line)\n";
     std::cout << "  -E  --error=kind       report Lean messages of kind as errors\n";
     std::cout << "      --deps             just print dependencies of a Lean input\n";
@@ -273,6 +274,7 @@ static struct option g_long_options[] = {
 #endif
     {"plugin",       required_argument, 0, 'p'},
     {"load-dynlib",  required_argument, 0, 'l'},
+    {"setup",        required_argument, 0, 'u'},
     {"error",        required_argument, 0, 'E'},
     {"json",         no_argument,       &json_output, 1},
     {"print-prefix", no_argument,       &print_prefix, 1},
@@ -340,6 +342,7 @@ extern "C" object * lean_run_frontend(
     object * error_kinds,
     object * plugins,
     bool     print_stats,
+    object * header_file_name,
     object * w
 );
 option_ref<elab_environment> run_new_frontend(
@@ -351,7 +354,8 @@ option_ref<elab_environment> run_new_frontend(
     optional<std::string> const & ilean_file_name,
     uint8_t json_output,
     array_ref<name> const & error_kinds,
-    bool print_stats
+    bool print_stats,
+    optional<std::string> const & setup_file_name
 ) {
     return get_io_result<option_ref<elab_environment>>(lean_run_frontend(
         mk_string(input),
@@ -365,6 +369,7 @@ option_ref<elab_environment> run_new_frontend(
         error_kinds.to_obj_arg(),
         mk_empty_array(),
         print_stats,
+        setup_file_name ? mk_option_some(mk_string(*setup_file_name)) : mk_option_none(),
         io_mk_world()
     ));
 }
@@ -487,6 +492,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
     bool run = false;
     optional<std::string> olean_fn;
     optional<std::string> ilean_fn;
+    optional<std::string> setup_fn;
     bool use_stdin = false;
     unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL + 1;
     bool only_deps = false;
@@ -638,6 +644,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
                 lean::load_dynlib(optarg);
                 forwarded_args.push_back(string_ref("--load-dynlib=" + std::string(optarg)));
                 break;
+            case 'u':
+                check_optarg("u");
+                setup_fn = optarg;
+                break;
             case 'E':
                 check_optarg("E");
                 error_kinds.push_back(string_to_name(std::string(optarg)));
@@ -755,7 +765,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
 
         if (!main_module_name)
             main_module_name = name("_stdin");
-        option_ref<elab_environment> opt_env = run_new_frontend(contents, opts, mod_fn, *main_module_name, trust_lvl, olean_fn, ilean_fn, json_output, error_kinds, stats);
+        option_ref<elab_environment> opt_env = run_new_frontend(
+            contents, opts, mod_fn, *main_module_name, trust_lvl,
+            olean_fn, ilean_fn, json_output, error_kinds, stats, setup_fn
+        );
 
         if (opt_env) {
             elab_environment env = opt_env.get_val();
diff --git a/tests/pkg/setup/Dep.lean b/tests/pkg/setup/Dep.lean
new file mode 100644
index 0000000000..5d95528add
--- /dev/null
+++ b/tests/pkg/setup/Dep.lean
@@ -0,0 +1 @@
+def hello := "hello"
diff --git a/tests/pkg/setup/Test.lean b/tests/pkg/setup/Test.lean
new file mode 100644
index 0000000000..fac75d77bd
--- /dev/null
+++ b/tests/pkg/setup/Test.lean
@@ -0,0 +1 @@
+#eval hello
diff --git a/tests/pkg/setup/clean.sh b/tests/pkg/setup/clean.sh
new file mode 100755
index 0000000000..2c4fabf32b
--- /dev/null
+++ b/tests/pkg/setup/clean.sh
@@ -0,0 +1 @@
+rm -f Dep.olean
diff --git a/tests/pkg/setup/setup.json b/tests/pkg/setup/setup.json
new file mode 100644
index 0000000000..ab86b7d2a4
--- /dev/null
+++ b/tests/pkg/setup/setup.json
@@ -0,0 +1,19 @@
+{
+  "name": "Dep",
+  "isModule": false,
+  "imports": [
+    {
+      "module": "Dep",
+      "importAll": false,
+      "isExported": true
+    }
+  ],
+  "modules": {
+    "Dep": {
+      "olean": "Dep.olean"
+    }
+  },
+  "dynlibs": [],
+  "plugins": [],
+  "options": {}
+}
diff --git a/tests/pkg/setup/test.sh b/tests/pkg/setup/test.sh
new file mode 100755
index 0000000000..ff76796b2f
--- /dev/null
+++ b/tests/pkg/setup/test.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+# Test that Lean will use the specified olean from `setup.json`
+lean Dep.lean -o Dep.olean
+lean Test.lean --setup setup.json