diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index a981d0a749..b8af3376f0 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -300,6 +300,28 @@ structure SetupImportsResult where
   /-- Lean plugins to load as part of the environment setup. -/
   plugins : Array System.FilePath := #[]
 
+/--
+Parses an option value from a string and inserts it into `opts`.
+The type of the option is determined from `decl`.
+-/
+def setOption (opts : Options) (decl : OptionDecl) (name : Name) (val : String)  : IO Options := do
+  match decl.defValue with
+  | .ofBool _ =>
+    match val with
+    | "true"  => return opts.insert name true
+    | "false" => return opts.insert name false
+    | _ =>
+      throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+        it must be true/false"
+  | .ofNat _ =>
+    let some val := val.toNat?
+      | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
+          it must be a natural number"
+    return opts.insert name val
+  | .ofString _ => return opts.insert name val
+  | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
+            cannot be set in the command line, use set_option command"
+
 /--
 Parses values of options registered during import and left by the C++ frontend as strings.
 Removes `weak` prefixes from both parsed and unparsed options and fails if any option names remain
@@ -322,22 +344,7 @@ If the option is defined in a library, use '-D{`weak ++ name}' to set it conditi
     let .ofString val := val
       | opts' := opts'.insert name val  -- Already parsed
 
-    match decl.defValue with
-    | .ofBool _ =>
-      match val with
-      | "true"  => opts' := opts'.insert name true
-      | "false" => opts' := opts'.insert name false
-      | _ =>
-        throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
-          it must be true/false"
-    | .ofNat _ =>
-      let some val := val.toNat?
-        | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
-            it must be a natural number"
-      opts' := opts'.insert name val
-    | .ofString _ => opts' := opts'.insert name val
-    | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
-              cannot be set in the command line, use set_option command"
+    opts' ← setOption opts' decl name val
 
   return opts'
 
diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean
index af3c89ffdb..e39a8b9f94 100644
--- a/src/Lean/Shell.lean
+++ b/src/Lean/Shell.lean
@@ -55,15 +55,15 @@ opaque displayCumulativeProfilingTimes : BaseIO Unit
 @[extern "lean_internal_has_address_sanitizer"]
 opaque Internal.hasAddressSanitizer (_ : Unit) : Bool
 
-/-- Whether Lean was built with multithread support. -/
+/-- Whether Lean was built with multithread support (i.e., `LEAN_MULTI_THREAD`). -/
 @[extern "lean_internal_is_multi_thread"]
 opaque Internal.isMultiThread (_ : Unit) : Bool
 
-/-- Whether Lean was built in debug mode. -/
+/-- Whether Lean was built in debug mode (i.e., `LEAN_DEBUG`). -/
 @[extern "lean_internal_is_debug"]
 opaque Internal.isDebug (_ : Unit) : Bool
 
-/-- Returns the mode Lean was built in. -/
+/-- Returns the mode Lean was built in (i.e., `LEAN_BUILD_TYPE`). -/
 @[extern "lean_internal_get_build_type"]
 opaque Internal.getBuildType (_ : Unit) : String
 
@@ -89,7 +89,27 @@ opaque Internal.getDefaultMaxHeartbeat (_ : Unit) : Nat
 @[extern "lean_internal_set_max_heartbeat"]
 opaque Internal.setMaxHeartbeat (max : USize) : BaseIO Unit
 
-/-- Lean equivalent of `LEAN_VERSION_STRING` / `g_short_version_string` -/
+/-- Returns whether Lean was built as verbose by default (i.e., `LEAN_DEFAULT_VERBOSE`). -/
+@[extern "lean_internal_get_default_verbose"]
+opaque Internal.getDefaultVerbose (_ : Unit) : Bool
+
+/-- Sets whether Lean aborts when a panic occurs. -/
+@[extern "lean_internal_set_exit_on_panic"]
+opaque Internal.setExitOnPanic (exit : Bool) : BaseIO Unit
+
+/-- Sets the stack size (in bytes) of a Lean thread. -/
+@[extern "lean_internal_set_thread_stack_size"]
+opaque Internal.setThreadStackSize (sz : USize) : BaseIO Unit
+
+/-- Enables debug assertions with the given tag. -/
+@[extern "lean_internal_enable_debug"]
+opaque Internal.enableDebug (tag : @& String) : BaseIO Unit
+
+/--
+Lean's short version string (i.e., what is printed by `lean --short-version`).
+
+This is the Lean equivalent of of the C++ `LEAN_VERSION_STRING` / `g_short_version_string`.
+-/
 def shortVersionString : String :=
   if version.specialDesc ≠ "" then
     s!"{versionStringCore}-{version.specialDesc}"
@@ -107,13 +127,17 @@ def versionHeader : String := Id.run do
     ver := s!"{ver}, commit {githash}"
   s!"Lean (version {ver}, {Internal.getBuildType ()})"
 
-/-- Print the Lean version header. -/
-@[export lean_display_header]
-def displayHeader : IO Unit := do
-  IO.println versionHeader
+/--
+A string containing the list of additional features Lean was built with.
+
+This is printed by `lean --features`.
+-/
+def featuresString :=
+  if Internal.hasLLVMBackend () then
+    "[LLVM]"
+  else "[]"
 
 /-- Print the Lean CLI help message. -/
-@[export lean_display_help]
 def displayHelp (useStderr : Bool) : IO Unit := do
   let out ← if useStderr then IO.getStderr else IO.getStdout
   out.putStrLn    versionHeader
@@ -129,7 +153,7 @@ def displayHelp (useStderr : Bool) : IO Unit := do
   out.putStrLn    "  -c, --c=fname          name of the C output file"
   out.putStrLn    "  -b, --bc=fname         name of the LLVM bitcode file"
   out.putStrLn    "      --stdin            take input from stdin"
-  out.putStrLn    "      --root=dir         set package root directory from which the module name\n"
+  out.putStrLn    "  -R, --root=dir         set package root directory from which the module name\n"
   out.putStrLn    "                         of the input file is calculated\n"
   out.putStrLn    "                         (default: current working directory)\n";
   out.putStrLn    "  -t, --trust=num        trust level (default: max) 0 means do not trust any macro,\n"
@@ -148,7 +172,7 @@ def displayHelp (useStderr : Bool) : IO Unit := do
   out.putStrLn    "      --load-dynlib=file load shared library to make its symbols available to the interpreter"
   out.putStrLn    "      --setup=file       JSON file with module setup data (supersedes the file's header)"
   out.putStrLn    "      --json             report Lean output (e.g., messages) as JSON (one per line)"
-  out.putStrLn    "  -E  --error=kind       report Lean messages of kind as errors"
+  out.putStrLn    "  -E, --error=kind       report Lean messages of kind as errors"
   out.putStrLn    "      --deps             just print dependencies of a Lean input"
   out.putStrLn    "      --src-deps         just print dependency sources of a Lean input"
   out.putStrLn    "      --print-prefix     print the installation prefix for Lean and exit"
@@ -170,52 +194,285 @@ private builtin_initialize maxMemory : Lean.Option Nat ←
 private builtin_initialize timeout : Lean.Option Nat ←
   Lean.Option.register `timeout {defValue := Internal.getDefaultMaxHeartbeat ()}
 
+private builtin_initialize verbose : Lean.Option Bool ←
+  Lean.Option.register `verbose {defValue := Internal.getDefaultVerbose ()}
+
+/--
+Returns the default options Lean was built with
+(i.e., those set in `stdlib_flags.h`).
+-/
+@[extern "lean_internal_get_default_options"]
+opaque Internal.getDefaultOptions (_ : Unit) : Options
+
+/--
+Returns the believer trust level of the Lean environment (i.e., `LEAN_BELIEVER_TRUST_LEVEL`).
+
+If an environment is created with a trust level greater than this, then we can add declarations
+to it without type checking them.
+-/
+@[extern "lean_internal_get_believer_trust_level"]
+opaque Internal.getBelieverTrustLevel (_ : Unit) : UInt32
+
+/-- Returns the shell's default trust level. -/
+def defaultTrustLevel : UInt32 :=
+  Internal.getBelieverTrustLevel () + 1
+
+/-- Returns the platform's native concurrency limit. -/
+@[extern "lean_internal_get_hardware_concurrency"]
+opaque Internal.getHardwareCurrency (_ : Unit) : UInt32
+
+/-- Returns the default number of threads for the shell's task manager. -/
+def defaultNumThreads : UInt32 :=
+  if Internal.isMultiThread () then
+    Internal.getHardwareCurrency ()
+  else 0
+
+structure ShellOptions where
+  leanOpts : Options := Internal.getDefaultOptions ()
+  forwardedArgs : Array String := #[]
+  component : ShellComponent := .frontend
+  printPrefix : Bool := false
+  printLibDir : Bool := false
+  useStdin : Bool := false
+  onlyDeps : Bool := false
+  onlySrcDeps : Bool := false
+  depsJson : Bool := false
+  opts : Options := {}
+  trustLevel : UInt32 := defaultTrustLevel
+  numThreads : UInt32 := defaultNumThreads
+  rootDir? : Option System.FilePath := none
+  setupFileName? : Option System.FilePath := none
+  oleanFileName? : Option System.FilePath := none
+  ileanFileName? : Option System.FilePath := none
+  cFileName? : Option System.FilePath := none
+  bcFileName? : Option System.FilePath := none
+  jsonOutput : Bool := false
+  errorOnKinds : Array Name := #[]
+  printStats : Bool := false
+  run : Bool := false
+
+@[export lean_shell_options_mk]
+def mkShellOptions (_ : Unit) : ShellOptions := {}
+
+@[export lean_shell_options_get_run]
+def ShellOptions.getRun (opts : ShellOptions) : Bool :=
+  opts.run
+
+@[export lean_shell_options_get_profiler]
+def ShellOptions.getProfiler (opts : ShellOptions) : Bool :=
+  profiler.get opts.leanOpts
+
+@[export lean_shell_options_get_num_threads]
+def ShellOptions.getNumThreads (opts : ShellOptions) : UInt32 :=
+  opts.numThreads
+
+def checkOptArg (optName : String) (optArg? : Option String) : IO String := do
+  if let some arg := optArg? then
+    return arg
+  else
+    throw <| .userError s!"argument missing for option '-{optName}'"
+
+def setConfigOption (opts : Options) (arg : String) : IO Options := do
+  let pos := arg.find '='
+  if h : pos.IsAtEnd then
+    throw <| .userError "invalid -D parameter, argument must contain '='"
+  else
+    let name := arg.sliceTo pos |>.toName
+    let val := arg.sliceFrom (pos.next h) |>.copy
+    if let some decl := (← getOptionDecls).find? name then
+      Language.Lean.setOption opts decl name val
+    else
+      -- More options may be registered by imports, so we leave validating them to the elaborator.
+      -- This (minor) duplication may be resolved later.
+      return opts.insert name val
+
+/--
+Process a command-line option parsed by the C++ shell.
+
+Runs under `IO.initializing` and without a task manager.
+-/
+@[export lean_shell_options_process]
+def ShellOptions.process (opts : ShellOptions)
+    (opt : Char) (optArg? : Option String) : EIO UInt32 ShellOptions := do
+  have : MonadLift IO (EIO UInt32) := ⟨liftIO⟩
+  match opt with
+  | 'e' => -- undocumented
+    Internal.setExitOnPanic true
+    return opts
+  | 'j' => -- `-j, --threads=num`
+    let arg ← checkOptArg "j" optArg?
+    let some numThreads := arg.toNat?
+      | throwExpectedNumeric "j"
+    if h : numThreads < UInt32.size then
+      let numThreads := UInt32.ofNatLT numThreads h
+      let forwardedArgs := opts.forwardedArgs.push s!"-j{arg}";
+      return {opts with forwardedArgs, numThreads}
+    else
+      throwTooLarge "j"
+  | 'v' => --- `-v, --version`
+    IO.println Lean.versionHeader
+    throw 0
+  | 'V' => --- `-V, --short-version`
+    IO.println Lean.shortVersionString
+    throw 0
+  | 'g' => -- `-g, --githash`
+    IO.println Lean.githash
+    throw 0
+  | 'h' => -- `-h, --help`
+    displayHelp (useStderr := false)
+    throw 0
+  | 'f' => -- `--features`
+    IO.println Lean.featuresString
+    throw 0
+  | 'c' => -- `-c, --c=fname`
+    return {opts with cFileName? := ← checkOptArg "c" optArg?}
+  | 'b' => -- `-b, --bc=fname`
+    return {opts with bcFileName? := ← checkOptArg "b" optArg?}
+  | 's' => -- `-s, --tstack=num`
+    let arg ← checkOptArg "s" optArg?
+    let some stackSize := arg.toNat?
+      | throwExpectedNumeric "s"
+    let stackSize := stackSize / 4 * 4 * 1024
+    if h : stackSize < USize.size then
+      let stackSize := USize.ofNatLT stackSize h
+      Internal.setThreadStackSize stackSize
+      let forwardedArgs := opts.forwardedArgs.push s!"-s{arg}"
+      return {opts with forwardedArgs}
+    else
+      throwTooLarge "s"
+  | 'I' => -- `-I, --stdin`
+    return {opts with useStdin := true}
+  | 'r' => -- `--run`
+    return {opts with run := true}
+  | 'o' => -- `--o, olean=fname`
+    return {opts with oleanFileName? := ← checkOptArg "o" optArg?}
+  | 'i' => -- `--i, ilean=fname`
+    return {opts with ileanFileName? := ← checkOptArg "i" optArg?}
+  | 'R' => -- `-R, --root=dir`
+    let arg ← checkOptArg "R" optArg?
+    let forwardedArgs := opts.forwardedArgs.push s!"-R{arg}"
+    return {opts with forwardedArgs, rootDir? := arg}
+  | 'M' => -- `-M, --memory=num`
+    let arg ← checkOptArg "M" optArg?
+    let some val := arg.toNat?
+      | throwExpectedNumeric "M"
+    let leanOpts := maxMemory.set opts.leanOpts val
+    let forwardedArgs := opts.forwardedArgs.push s!"-M{arg}"
+    return {opts with forwardedArgs, leanOpts}
+  | 'T' => -- `-T, --timeout=num`
+    let arg ← checkOptArg "T" optArg?
+    let some val := arg.toNat?
+      | throwExpectedNumeric "T"
+    let leanOpts := timeout.set opts.leanOpts val
+    let forwardedArgs := opts.forwardedArgs.push s!"-T{arg}"
+    return {opts with forwardedArgs, leanOpts}
+  | 't' => -- `--trust=num`
+    let arg ← checkOptArg "t" optArg?
+    let some trustLevel := arg.toNat?
+      | throwExpectedNumeric "t"
+    if h : trustLevel < UInt32.size then
+      let trustLevel := UInt32.ofNatLT trustLevel h
+      let forwardedArgs := opts.forwardedArgs.push s!"-t{arg}";
+      return {opts with forwardedArgs, trustLevel}
+    else
+      throwTooLarge "t"
+  | 'q' =>
+    return {opts with leanOpts := verbose.set opts.leanOpts false}
+  | 'd' => -- `--deps`
+    return {opts with onlyDeps := true}
+  | 'O' => -- `--src-deps`
+    return {opts with onlySrcDeps := true}
+  | 'N' => -- `--deps-json`
+    return {opts with onlyDeps := true, depsJson := true}
+  | 'J' => -- `--json`
+    return {opts with jsonOutput := true}
+  | 'a' => -- `--stats`
+    return {opts with printStats := true}
+  | 'x' =>  -- `--print-prefix`
+    return {opts with printPrefix := true}
+  | 'L' =>  -- `--print-libdir`
+    return {opts with printLibDir := true}
+  | 'D' => -- `-D name=value`
+    let arg ← checkOptArg "D" optArg?
+    let leanOpts ← setConfigOption opts.leanOpts arg
+    let forwardedArgs := opts.forwardedArgs.push s!"-D{arg}"
+    return {opts with forwardedArgs, leanOpts}
+  | 'S' => -- `--server`
+    return {opts with component := .watchdog}
+  | 'W' => -- `--worker`
+    return {opts with component := .worker}
+  | 'P' => -- `--profile`
+    return {opts with leanOpts := profiler.set opts.leanOpts true}
+  | 'B' => -- `--debug=tag`
+    if Internal.isDebug () then
+      let arg ← checkOptArg "B" optArg?
+      Internal.enableDebug arg
+      return opts
+    -- if not `LEAN_DEBUG`, fall through to unknown option
+  | 'p' => -- `--plugin=file`
+    let arg ← checkOptArg "p" optArg?
+    Lean.loadPlugin arg
+    let forwardedArgs := opts.forwardedArgs.push s!"-p{arg}"
+    return {opts with forwardedArgs}
+  | 'l' => -- `--load-dynlib=file`
+    let arg ← checkOptArg "l" optArg?
+    Lean.loadDynlib arg
+    let forwardedArgs := opts.forwardedArgs.push s!"-l{arg}"
+    return {opts with forwardedArgs}
+  | 'u' => -- `--setup=file`
+    return {opts with setupFileName? := ← checkOptArg "u" optArg?}
+  | 'E' => -- `-E, --error=kind`
+    let arg ← checkOptArg "E" optArg?
+    let errorOnKinds := opts.errorOnKinds.push arg.toName
+    return {opts with errorOnKinds}
+  | _ =>
+    pure ()
+  eprint "Unknown command line option\n"
+  displayHelp (useStderr := true)
+  throw 1
+where
+  @[inline] eprint msg := do
+    IO.eprint msg |>.catchExceptions fun _ => pure ()
+  @[inline] liftIO {α} (x : IO α) := do
+    match (← x.toBaseIO) with
+    | .ok a =>
+      return a
+    | .error e =>
+      eprint s!"error: "
+      eprint (toString e)
+      eprint "\n"
+      throw 1
+  @[inline] throwExpectedNumeric opt := do
+    eprint s!"error: expected numeric argument for option '-{opt}'\n"
+    throw 1
+  @[inline] throwTooLarge opt := do
+    eprint s!"error: argument value for '-{opt}' is too large\n"
+    throw 1
+
 @[export lean_shell_main]
-def shellMain
-    (args : List String)
-    (forwardedArgs : List String)
-    (component : ShellComponent := .frontend)
-    (printPrefix : Bool := false)
-    (printLibDir : Bool := false)
-    (useStdin : Bool := false)
-    (onlyDeps : Bool := false)
-    (onlySrcDeps : Bool := false)
-    (depsJson : Bool := false)
-    (opts : Options := {})
-    (trustLevel : UInt32 := 0)
-    (rootDir? : Option System.FilePath := none)
-    (setupFileName? : Option System.FilePath := none)
-    (oleanFileName? : Option System.FilePath := none)
-    (ileanFileName? : Option System.FilePath := none)
-    (cFileName? : Option System.FilePath := none)
-    (bcFileName? : Option System.FilePath := none)
-    (jsonOutput : Bool := false)
-    (errorOnKinds : Array Name := #[])
-    (printStats : Bool := false)
-    (run : Bool := false)
-    : IO UInt32 := do
-  if printPrefix then
+def shellMain (args : List String) (opts : ShellOptions) : IO UInt32 := do
+  if opts.printPrefix then
     IO.println (← getBuildDir)
     return 0
-  if printLibDir then
+  if opts.printLibDir then
     IO.println (← getLibDir (← getBuildDir))
     return 0
-  let maxMemory := maxMemory.get opts
+  let maxMemory := maxMemory.get opts.leanOpts
   if maxMemory != 0 then
     Internal.setMaxMemory (maxMemory.toUSize * 1024 * 1024)
-  let timeout := timeout.get opts
+  let timeout := timeout.get opts.leanOpts
   if timeout != 0 then
     Internal.setMaxHeartbeat (timeout.toUSize * 1000)
-  match component with
+  match opts.component with
   | .frontend =>
     pure ()
   | .watchdog =>
-    return ← Server.Watchdog.watchdogMain forwardedArgs
+    return ← Server.Watchdog.watchdogMain opts.forwardedArgs.toList
   | .worker =>
-    return ← Server.FileWorker.workerMain opts
-  if onlyDeps && depsJson then
+    return ← Server.FileWorker.workerMain opts.leanOpts
+  if opts.onlyDeps && opts.depsJson then
     let fns ←
-      if useStdin then
+      if opts.useStdin then
         (← IO.getStdin).lines
       else
         pure args.toArray
@@ -225,72 +482,73 @@ def shellMain
     match args with
     | fileName :: args => (some fileName, args)
     | [] => (none, args)
-  if !run && !args.isEmpty then
+  if !opts.run && !args.isEmpty then
     IO.eprintln "Expected exactly one file name"
     displayHelp (useStderr := true)
     return 1
   let fileName ←
     if let some fileName := fileName? then
       pure fileName
-    else if useStdin then
+    else if opts.useStdin then
       pure "<stdin>"
     else
       IO.eprintln "Expected exactly one file name"
       displayHelp (useStderr := true)
       return 1
   let contents ← decodeLossyUTF8 <$> do
-    if useStdin then
+    if opts.useStdin then
       (← IO.getStdin).readBinToEnd
     else
       IO.FS.readBinFile fileName
-  if onlyDeps then
+  if opts.onlyDeps then
     Elab.printImports contents fileName
     return 0
-  if onlySrcDeps then
+  if opts.onlySrcDeps then
     Elab.printImportSrcs contents fileName
     return 0
   -- Quick and dirty `#lang` support
   ---TODO: make it extensible, and add `lean4md`
   let contents ←
-    if contents.startsWith "#lang" then
+    if let some contents := contents.dropPrefix? "#lang" then
       let endLinePos := contents.find '\n'
-      let langId := String.Pos.Raw.extract contents ⟨6⟩ endLinePos.offset |>.trimAscii
+      let langId := contents.sliceTo endLinePos |>.trimAscii
       if langId == "lean4" then
         pure () -- do nothing for now
       else
         IO.eprintln s!"unknown language '{langId}'\n";
         return 1
       -- Remove up to `\n`
-      pure <| String.Pos.Raw.extract contents endLinePos.offset contents.rawEndPos
+      pure (contents.sliceFrom endLinePos).copy
     else
       pure contents
-  let setup? ← setupFileName?.mapM ModuleSetup.load
+  let setup? ← opts.setupFileName?.mapM ModuleSetup.load
   let mainModuleName ←
     if let some setup := setup? then
       pure setup.name
     else if let some fileName := fileName? then
-      try moduleNameOfFileName fileName rootDir? catch e =>
-        if oleanFileName?.isNone && cFileName?.isNone then
+      try moduleNameOfFileName fileName opts.rootDir? catch e =>
+        if opts.oleanFileName?.isNone && opts.cFileName?.isNone then
           pure `_stdin
         else
           throw e
     else
       pure `_stdin
-  let env? ← Elab.runFrontend contents opts fileName mainModuleName trustLevel
-      oleanFileName? ileanFileName? jsonOutput errorOnKinds #[] printStats setup?
+  let env? ← Elab.runFrontend contents opts.leanOpts fileName mainModuleName
+    opts.trustLevel opts.oleanFileName? opts.ileanFileName? opts.jsonOutput opts.errorOnKinds
+    #[] opts.printStats setup?
   if let some env := env? then
-    if run then
-      return ← runMain env opts args
-    if let some c := cFileName? then
+    if opts.run then
+      return ← runMain env opts.leanOpts args
+    if let some c := opts.cFileName? then
       let .ok out ← IO.FS.Handle.mk c .write |>.toBaseIO
         | IO.eprintln s!"failed to create '{c}'"
           return 1
-      profileitIO "C code generation" opts do
+      profileitIO "C code generation" opts.leanOpts do
         let data ← IO.ofExcept <| IR.emitC env mainModuleName
         out.write data.toUTF8
-    if let some bc := bcFileName? then
+    if let some bc := opts.bcFileName? then
       initLLVM
-      profileitIO "LLVM code generation" opts do
+      profileitIO "LLVM code generation" opts.leanOpts do
         emitLLVM env mainModuleName bc
   displayCumulativeProfilingTimes
   if Internal.hasAddressSanitizer () then
diff --git a/src/library/elab_environment.cpp b/src/library/elab_environment.cpp
index 49ef3e6fe0..95d3680254 100644
--- a/src/library/elab_environment.cpp
+++ b/src/library/elab_environment.cpp
@@ -64,4 +64,9 @@ extern "C" LEAN_EXPORT lean_object * lean_kernel_check(lean_object * obj_env, le
         return type_checker(env.to_kernel_env(), local_ctx(lctx)).check(expr(a)).steal();
     });
 }
+
+/* getBelieverTrustLevel (_ : Unit) : UInt32 */
+extern "C" LEAN_EXPORT uint32 lean_internal_get_believer_trust_level(obj_arg) {
+   return LEAN_BELIEVER_TRUST_LEVEL;
+}
 }
diff --git a/src/runtime/debug.cpp b/src/runtime/debug.cpp
index ee4f917100..ecd5da1bfc 100644
--- a/src/runtime/debug.cpp
+++ b/src/runtime/debug.cpp
@@ -59,6 +59,12 @@ void enable_debug(char const * tag) {
     g_enabled_debug_tags->insert(tag);
 }
 
+/* enableDebug (tag : @& String) : BaseIO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_internal_enable_debug(b_lean_obj_arg tag) {
+    enable_debug(lean_string_cstr(tag));
+    return lean_box(0);
+}
+
 void disable_debug(char const * tag) {
     if (g_enabled_debug_tags)
         g_enabled_debug_tags->erase(tag);
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index bee8738d62..c03af87615 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -106,6 +106,12 @@ extern "C" LEAN_EXPORT void lean_set_exit_on_panic(bool flag) {
     g_exit_on_panic = flag;
 }
 
+/* setExitOnPanic (exit : Bool) : BaseIO Unit */
+extern "C" LEAN_EXPORT obj_res lean_internal_set_exit_on_panic(uint8 exit) {
+    g_exit_on_panic = exit;
+    return box(0);
+}
+
 extern "C" LEAN_EXPORT void lean_set_panic_messages(bool flag) {
     g_panic_messages = flag;
 }
@@ -1014,6 +1020,11 @@ static unsigned get_lean_num_threads() {
     return hardware_concurrency();
 }
 
+/* getHardwareConcurrency (_ : Unit) : UInt32 */
+extern "C" LEAN_EXPORT uint32 lean_internal_get_hardware_concurrency(obj_arg) {
+    return hardware_concurrency();
+}
+
 extern "C" LEAN_EXPORT void lean_init_task_manager() {
     lean_init_task_manager_using(get_lean_num_threads());
 }
diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp
index 7df3d8f2f7..ba06b37d13 100644
--- a/src/runtime/thread.cpp
+++ b/src/runtime/thread.cpp
@@ -157,6 +157,12 @@ lthread::~lthread() {}
 void lthread::join() { m_imp->join(); }
 #endif
 
+/* setThreadStackSize (sz : USize) : BaseIO Unit */
+extern "C" LEAN_EXPORT lean_obj_res lean_internal_set_thread_stack_size(size_t sz) {
+    lthread::set_thread_stack_size(sz);
+    return lean_box(0);
+}
+
 LEAN_THREAD_VALUE(bool, g_finalizing, false);
 
 bool in_thread_finalization() {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 365448881a..272dd9b72f 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "util/options.h"
 #include "util/option_declarations.h"
+#include "stdlib_flags.h"
 
 #ifndef LEAN_DEFAULT_VERBOSE
 #define LEAN_DEFAULT_VERBOSE true
@@ -50,6 +51,16 @@ bool get_verbose(options const & opts) {
     return opts.get_bool(*g_verbose, LEAN_DEFAULT_VERBOSE);
 }
 
+/* getDefaultVerbose (_ : Unit) : Bool */
+extern "C" LEAN_EXPORT uint8 lean_internal_get_default_verbose(obj_arg) {
+    return LEAN_DEFAULT_VERBOSE;
+}
+
+/* getDefaultOptions (_ : Unit) : Options */
+extern "C" LEAN_EXPORT obj_res lean_internal_get_default_options(obj_arg) {
+    return get_default_options().steal();
+}
+
 options join(options const & opts1, options const & opts2) {
     kvmap r = opts2.m_value;
     for (kvmap_entry const & e : opts1.m_value) {
diff --git a/src/util/options.h b/src/util/options.h
index 75c9ea1f47..f1908f8b55 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -68,6 +68,7 @@ public:
     */
     friend options join(options const & opts1, options const & opts2);
 
+    object * steal() { return m_value.steal(); }
     object * to_obj_arg() const { return m_value.to_obj_arg(); }
 };
 
diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index 7ef4c515ad..bcf7eaf74a 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -40,7 +40,6 @@ Author: Leonardo de Moura
 #include "initialize/init.h"
 #include "library/ir_interpreter.h"
 #include "util/path.h"
-#include "stdlib_flags.h"
 #ifdef _MSC_VER
 #include <io.h>
 #define STDOUT_FILENO 1
@@ -157,33 +156,6 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
 
 using namespace lean; // NOLINT
 
-extern "C" obj_res lean_display_header();
-static void display_header() {
-    consume_io_result(lean_display_header());
-}
-
-static void display_version(std::ostream & out) {
-    out << get_short_version_string() << "\n";
-}
-
-static void display_features(std::ostream & out) {
-    out << "[";
-#if defined(LEAN_LLVM)
-    out << "LLVM";
-#endif
-    out << "]\n";
-}
-
-extern "C" obj_res lean_display_help(uint8 use_stderr);
-static void display_help(bool use_stderr) {
-    consume_io_result(lean_display_help(use_stderr));
-}
-
-static int only_src_deps = 0;
-static int print_prefix = 0;
-static int print_libdir = 0;
-static int json_output = 0;
-
 static struct option g_long_options[] = {
     {"version",      no_argument,       0, 'v'},
     {"help",         no_argument,       0, 'h'},
@@ -200,12 +172,12 @@ static struct option g_long_options[] = {
     {"stats",        no_argument,       0, 'a'},
     {"quiet",        no_argument,       0, 'q'},
     {"deps",         no_argument,       0, 'd'},
-    {"src-deps",     no_argument,       &only_src_deps, 1},
-    {"deps-json",    no_argument,       0, 'J'},
+    {"src-deps",     no_argument,       0, 'O'},
+    {"deps-json",    no_argument,       0, 'N'},
     {"timeout",      optional_argument, 0, 'T'},
     {"c",            optional_argument, 0, 'c'},
     {"bc",           optional_argument, 0, 'b'},
-    {"features",     optional_argument, 0, 'f'},
+    {"features",     no_argument,       0, 'f'},
     {"exitOnPanic",  no_argument,       0, 'e'},
 #if defined(LEAN_MULTI_THREAD)
     {"threads",      required_argument, 0, 'j'},
@@ -217,9 +189,9 @@ static struct option g_long_options[] = {
     {"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},
-    {"print-libdir", no_argument,       &print_libdir, 1},
+    {"json",         no_argument,       0, 'J'},
+    {"print-prefix", no_argument,       0, 'x'},
+    {"print-libdir", no_argument,       0, 'L'},
 #ifdef LEAN_DEBUG
     {"debug",        required_argument, 0, 'B'},
 #endif
@@ -233,90 +205,9 @@ static char const * g_opt_str =
 #endif
 ; // NOLINT
 
-options set_config_option(options const & opts, char const * in) {
-    if (!in) return opts;
-    while (*in && std::isspace(*in))
-        ++in;
-    std::string in_str(in);
-    auto pos = in_str.find('=');
-    if (pos == std::string::npos)
-        throw lean::exception("invalid -D parameter, argument must contain '='");
-    lean::name opt = lean::string_to_name(in_str.substr(0, pos));
-    std::string val = in_str.substr(pos+1);
-    auto decls = lean::get_option_declarations();
-    auto it = decls.find(opt);
-    if (it) {
-        switch (it->kind()) {
-        case lean::data_value_kind::Bool:
-            if (val == "true")
-                return opts.update(opt, true);
-            else if (val == "false")
-                return opts.update(opt, false);
-            else
-                throw lean::exception(lean::sstream() << "invalid -D parameter, invalid configuration option '" << opt
-                                      << "' value, it must be true/false");
-        case lean::data_value_kind::Nat:
-            return opts.update(opt, static_cast<unsigned>(atoi(val.c_str())));
-        case lean::data_value_kind::String:
-            return opts.update(opt, val.c_str());
-        default:
-            throw lean::exception(lean::sstream() << "invalid -D parameter, configuration option '" << opt
-                                  << "' cannot be set in the command line, use set_option command");
-        }
-    } else {
-        // More options may be registered by imports, so we leave validating them to the Lean side.
-        // This (minor) duplication will be resolved when this file is rewritten in Lean.
-        return opts.update(opt, val.c_str());
-    }
-}
-
 namespace lean {
-extern "C" obj_res lean_shell_main(
-    obj_arg  args,
-    obj_arg  forwarded_args,
-    uint8    component,
-    uint8    print_prefix,
-    uint8    print_libdir,
-    uint8    use_stdin,
-    uint8    only_deps,
-    uint8    only_src_deps,
-    uint8    deps_json,
-    obj_arg  opts,
-    uint32_t trust_level,
-    obj_arg  root_dir,
-    obj_arg  setup_file_name,
-    obj_arg  olean_filename,
-    obj_arg  ilean_filename,
-    obj_arg  c_filename,
-    obj_arg  bc_filename,
-    uint8    json_output,
-    obj_arg  error_kinds,
-    uint8    print_stats,
-    uint8    run
-);
-uint32 run_shell_main(
-    int argc, char* argv[],
-    buffer<string_ref> forwarded_args,
-    int run_server,
-    bool print_prefix,
-    bool print_libdir,
-    bool use_stdin,
-    bool only_deps,
-    bool only_src_deps,
-    bool deps_json,
-    options const & opts,
-    uint32_t trust_level,
-    optional<std::string> const & root_dir,
-    optional<std::string> const & setup_file_name,
-    optional<std::string> const & olean_file_name,
-    optional<std::string> const & ilean_file_name,
-    optional<std::string> const & c_file_name,
-    optional<std::string> const & bc_file_name,
-    bool json_output,
-    array_ref<name> const & error_kinds,
-    bool print_stats,
-    bool run
-) {
+extern "C" obj_res lean_shell_main(obj_arg args, obj_arg shell_opts);
+int run_shell_main(int argc, char* argv[], object_ref const & shell_opts) {
     list_ref<string_ref> args;
     while (argc > 0) {
         argc--;
@@ -324,45 +215,51 @@ uint32 run_shell_main(
     }
     return get_io_scalar_result<uint32>(lean_shell_main(
         args.steal(),
-        to_list_ref(forwarded_args).to_obj_arg(),
-        run_server,
-        print_prefix,
-        print_libdir,
-        use_stdin,
-        only_deps, only_src_deps, deps_json,
-        opts.to_obj_arg(),
-        trust_level,
-        root_dir ? mk_option_some(mk_string(*root_dir)) : mk_option_none(),
-        setup_file_name ? mk_option_some(mk_string(*setup_file_name)) : mk_option_none(),
-        olean_file_name ? mk_option_some(mk_string(*olean_file_name)) : mk_option_none(),
-        ilean_file_name ? mk_option_some(mk_string(*ilean_file_name)) : mk_option_none(),
-        c_file_name ? mk_option_some(mk_string(*c_file_name)) : mk_option_none(),
-        bc_file_name ? mk_option_some(mk_string(*bc_file_name)) : mk_option_none(),
-        json_output,
-        error_kinds.to_obj_arg(),
-        print_stats,
-        run
+        shell_opts.to_obj_arg()
     ));
 }
 
 extern "C" object* lean_init_search_path();
 void init_search_path() {
-    get_io_scalar_result<unsigned>(lean_init_search_path());
+    consume_io_result(lean_init_search_path());
 }
 
-extern "C" object* lean_environment_free_regions(object * env);
-void environment_free_regions(elab_environment && env) {
-    consume_io_result(lean_environment_free_regions(env.steal()));
-}
+extern "C" obj_res lean_shell_options_mk(obj_arg);
+object_ref mk_shell_options() {
+    return object_ref(lean_shell_options_mk(box(0)));
 }
 
-void check_optarg(char const * option_name) {
-    if (!optarg) {
-        std::cerr << "error: argument missing for option '-" << option_name << "'" << std::endl;
-        std::exit(1);
+extern "C" obj_res lean_shell_options_process(obj_arg shell_opts, uint32 opt, obj_arg opt_arg);
+bool process_shell_option(object_ref & shell_opts, int opt, char const * optarg, int & rc) {
+    auto optarg_ref = optarg ? mk_option_some(mk_string(optarg)) : mk_option_none();
+    auto r = lean_shell_options_process(shell_opts.steal(), opt, optarg_ref);
+    if (io_result_is_ok(r)) {
+        shell_opts = object_ref(io_result_get_value(r), true);
+        dec_ref(r);
+        return false;
+    } else {
+        rc = unbox(io_result_get_error(r));
+        dec_ref(r);
+        return true;
     }
 }
 
+extern "C" uint8 lean_shell_options_get_run(obj_arg shell_opts);
+bool get_shell_run(object_ref const & shell_opts) {
+    return lean_shell_options_get_run(shell_opts.to_obj_arg());
+}
+
+extern "C" uint8 lean_shell_options_get_profiler(obj_arg shell_opts);
+bool get_shell_profiler(object_ref const & shell_opts) {
+    return lean_shell_options_get_profiler(shell_opts.to_obj_arg());
+}
+
+extern "C" uint32 lean_shell_options_get_num_threads(obj_arg shell_opts);
+unsigned get_shell_num_threads(object_ref const & shell_opts) {
+    return lean_shell_options_get_num_threads(shell_opts.to_obj_arg());
+}
+}
+
 extern "C" object * lean_enable_initializer_execution();
 
 namespace lean {
@@ -412,21 +309,6 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
     auto init_start = std::chrono::steady_clock::now();
     lean::initializer init;
     second_duration init_time = std::chrono::steady_clock::now() - init_start;
-    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;
-    bool deps_json = false;
-    bool stats = false;
-    // 0 = don't run server, 1 = watchdog, 2 = worker
-    int run_server = 0;
-    unsigned num_threads    = 0;
-#if defined(LEAN_MULTI_THREAD)
-    num_threads = hardware_concurrency();
-#endif
 
     try {
         // Remark: This currently runs under `IO.initializing = true`.
@@ -437,167 +319,35 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
     }
     consume_io_result(lean_enable_initializer_execution());
 
-    options opts = get_default_options();
-    optional<std::string> c_output;
-    optional<std::string> llvm_output;
-    optional<std::string> root_dir;
-    buffer<string_ref> forwarded_args;
-    buffer<name> error_kinds;
-
-    while (!run) {  // stop consuming arguments after `--run`
-        int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
-        if (c == -1)
-            break; // end of command line
-        if (c == 0)
-            continue; // long-only option
-        switch (c) {
-            case 'e':
-                lean_set_exit_on_panic(true);
-                break;
-            case 'j':
-                num_threads = static_cast<unsigned>(atoi(optarg));
-                forwarded_args.push_back(string_ref("-j" + std::string(optarg)));
-                break;
-            case 'v':
-                display_header();
-                return 0;
-            case 'V':
-                display_version(std::cout);
-                return 0;
-            case 'g':
-                std::cout << LEAN_GITHASH << "\n";
-                return 0;
-            case 'h':
-                display_help(/* useStderr */ false);
-                return 0;
-            case 'f':
-                display_features(std::cout);
-                return 0;
-            case 'c':
-                check_optarg("c");
-                c_output = optarg;
-                break;
-            case 'b':
-                check_optarg("bc");
-                llvm_output = optarg;
-                break;
-            case 's':
-                lean::lthread::set_thread_stack_size(
-                        static_cast<size_t>((atoi(optarg) / 4) * 4) * static_cast<size_t>(1024));
-                forwarded_args.push_back(string_ref("-s" + std::string(optarg)));
-                break;
-            case 'I':
-                use_stdin = true;
-                break;
-            case 'r':
-                run = true;
-                break;
-            case 'o':
-                olean_fn = optarg;
-                break;
-            case 'i':
-                ilean_fn = optarg;
-                break;
-            case 'R':
-                root_dir = optarg;
-                forwarded_args.push_back(string_ref("-R" + std::string(optarg)));
-                break;
-            case 'M':
-                check_optarg("M");
-                opts = opts.update(get_max_memory_opt_name(), static_cast<unsigned>(atoi(optarg)));
-                forwarded_args.push_back(string_ref("-M" + std::string(optarg)));
-                break;
-            case 'T':
-                check_optarg("T");
-                opts = opts.update(get_timeout_opt_name(), static_cast<unsigned>(atoi(optarg)));
-                forwarded_args.push_back(string_ref("-T" + std::string(optarg)));
-                break;
-            case 't':
-                check_optarg("t");
-                trust_lvl = atoi(optarg);
-                forwarded_args.push_back(string_ref("-t" + std::string(optarg)));
-                break;
-            case 'q':
-                opts = opts.update(lean::get_verbose_opt_name(), false);
-                break;
-            case 'd':
-                only_deps = true;
-                break;
-            case 'J':
-                only_deps = true;
-                deps_json = true;
-                break;
-            case 'a':
-                stats = true;
-                break;
-            case 'D':
-                try {
-                    check_optarg("D");
-                    opts = set_config_option(opts, optarg);
-                    forwarded_args.push_back(string_ref("-D" + std::string(optarg)));
-                } catch (lean::exception & ex) {
-                    std::cerr << ex.what() << std::endl;
-                    return 1;
-                }
-                break;
-            case 'S':
-                run_server = 1;
-                break;
-            case 'W':
-                run_server = 2;
-                break;
-            case 'P':
-                opts = opts.update("profiler", true);
-                break;
-#if defined(LEAN_DEBUG)
-            case 'B':
-                check_optarg("B");
-                lean::enable_debug(optarg);
-                break;
-#endif
-            case 'p':
-                check_optarg("p");
-                lean::load_plugin(optarg);
-                forwarded_args.push_back(string_ref("--plugin=" + std::string(optarg)));
-                break;
-            case 'l':
-                check_optarg("l");
-                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)));
-                break;
-            default:
-                std::cerr << "Unknown command line option\n";
-                display_help(/* useStderr */ true);
-                return 1;
+    int rc;
+    object_ref shell_opts;
+    try {
+        shell_opts = mk_shell_options();
+        for (;;) {
+            int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
+            if (c == -1)
+                break; // end of command line
+            if (process_shell_option(shell_opts, c, optarg, rc))
+                return rc; // option processing triggered an early exit
+            if (get_shell_run(shell_opts))
+                break; // stop consuming arguments after `--run`
         }
+    } catch (lean::throwable & ex) {
+        std::cerr << "error: " << ex.what() << std::endl;
+        return 1;
     }
 
     lean::io_mark_end_initialization();
 
-    if (get_profiler(opts)) {
+    if (get_shell_profiler(shell_opts)) {
         g_lean_report_task_get_blocked_time = report_task_get_blocked_time;
         report_profiling_time("initialization", init_time);
     }
 
-    scoped_task_manager scope_task_man(num_threads);
+    scoped_task_manager scope_task_man(get_shell_num_threads(shell_opts));
 
     try {
-        return run_shell_main(
-            argc - optind, argv + optind,
-            forwarded_args, run_server, print_prefix, print_libdir,
-            use_stdin, only_deps, only_src_deps, deps_json,
-            opts, trust_lvl, root_dir, setup_fn,
-            olean_fn, ilean_fn, c_output, llvm_output,
-            json_output, error_kinds, stats, run
-        );
+        return run_shell_main(argc - optind, argv + optind, shell_opts);
     } catch (lean::throwable & ex) {
         std::cerr << ex.what() << "\n";
     } catch (std::bad_alloc & ex) {