diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index bba4a18e8453..9dab31af5098 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -566,3 +566,5 @@ public def help : (cmd : String) → String
 | "lean"                => helpLean
 | "translate-config"    => helpTranslateConfig
 | _                     => usage
+
+@[simp] public theorem help_empty : help "" = usage := by rfl
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index 50a65987805f..7fdf03da5617 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -144,11 +144,15 @@ abbrev CliMainM := ExceptT CliError MainM
 abbrev CliStateM := StateT LakeOptions CliMainM
 abbrev CliM := ArgsT CliStateM
 
-def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
+@[inline] def CliMainM.run (self : CliMainM α) : BaseIO ExitCode := do
+  MainM.run <| (ExceptT.run self) >>= fun | .ok a => pure a | .error e => error e.toString
+
+@[inline] def CliStateM.run (self : CliStateM α) (args : List String) : BaseIO ExitCode := do
   let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
-  let main := self.run' args |>.run' {args, elanInstall?, leanInstall?, lakeInstall?}
-  let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
-  main.run
+  StateT.run' self {args, elanInstall?, leanInstall?, lakeInstall?} |>.run
+
+@[inline] def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
+  StateT.run' self args |>.run args
 
 def CliStateM.runLogIO (x : LogIO α) : CliStateM α := do
   MainM.runLogIO x (← get).toLogConfig
@@ -160,154 +164,192 @@ def CliStateM.runLoggerIO (x : LoggerIO α) : CliStateM α := do
 
 instance (priority := low) : MonadLift LoggerIO CliStateM := ⟨CliStateM.runLoggerIO⟩
 
+def CliStateM.runIO (x : IO α) : CliStateM α := do
+  MainM.runLogIO x (← get).toLogConfig
+
+instance (priority := low) : MonadLift IO CliStateM := ⟨CliStateM.runIO⟩
+
+@[inline] def throwMissingArg (arg : String) : CliM α := do
+  throw <| CliError.missingArg arg
+
+instance : MonadThrowExpectedArg CliM := ⟨throwMissingArg⟩
+
+@[inline] def throwMissingOptArg (arg : String) : OptT CliStateM α := do
+  throw <| CliError.missingOptArg (← getOpt).copy arg
+
+instance : MonadThrowExpectedArg (OptT CliStateM) := ⟨throwMissingOptArg⟩
+
 /-! ## Argument Parsing -/
 
-def takeArg (arg : String) : CliM String := do
-  match (← takeArg?) with
-  | none => throw <| CliError.missingArg arg
-  | some arg => pure arg
+instance [Pure m] : MonadParseArg FilePath m :=
+  ⟨(pure <| FilePath.mk ·.copy)⟩
+
+@[inline] def parseOptArgUsing
+  (descr : String) (f : String.Slice → Option α) (arg : String.Slice)
+: OptT CliStateM α := do
+  if let some a := f arg then
+    return a
+  else
+    throw <| CliError.invalidOptArg (← getOpt).copy descr
 
-def takeOptArg (opt arg : String) : CliM String := do
-  match (← takeArg?) with
-  | none => throw <| CliError.missingOptArg opt arg
-  | some arg => pure arg
+instance : MonadParseArg Nat (OptT CliStateM) where
+  parseArg := parseOptArgUsing "natural number" (·.toNat?)
 
-@[inline] def takeOptArg' (opt arg : String) (f : String → Option α)  : CliM α := do
-  if let some a :=  f (← takeOptArg opt arg) then return a
-  throw <| CliError.invalidOptArg opt arg
+instance : MonadParseArg LogLevel (OptT CliStateM) where
+  parseArg := parseOptArgUsing "log level" LogLevel.ofString?
 
 /--
 Verify that there are no CLI arguments remaining
 before running the given action.
 -/
 def noArgsRem (act : CliStateM α) : CliM α := do
-  let args ← getArgs
-  if args.isEmpty then act else
-    throw <| CliError.unexpectedArguments args
+  match (← getArgs) with
+  | [] => act
+  | args => throw <| CliError.unexpectedArguments args
 
 /-! ## Option Parsing -/
 
-def getWantsHelp : CliStateM Bool :=
+@[inline] def getWantsHelp : CliStateM Bool :=
   (·.wantsHelp) <$> get
 
-def setConfigOpt (kvPair : String) : CliM PUnit :=
+def setConfigOpt (kvPair : String.Slice) : CliStateM PUnit :=
   let pos := kvPair.find '='
   let (key, val) :=
     if h : pos.IsAtEnd then
       (kvPair.toName, "")
     else
-      (kvPair.extract kvPair.startPos pos |>.toName, kvPair.extract (pos.next h) kvPair.endPos)
+      (kvPair.sliceTo pos |>.toName, kvPair.sliceFrom (pos.next h) |>.copy)
   modifyThe LakeOptions fun opts =>
     {opts with configOpts := opts.configOpts.insert key val}
 
-def lakeShortOption : (opt : Char) → CliM PUnit
-| 'q' => modifyThe LakeOptions ({· with verbosity := .quiet})
-| 'v' => modifyThe LakeOptions ({· with verbosity := .verbose})
-| 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
-| 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
-| 'o' => do let outputsFile? ← takeOptArg "-o" "path"; modifyThe LakeOptions ({· with outputsFile?})
-| 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
-| 'U' => do
-  logWarning "the '-U' shorthand for '--update' is deprecated"
-  modifyThe LakeOptions ({· with updateDeps := true})
-| 'R' => modifyThe LakeOptions ({· with reconfigure := true})
-| 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
-| 'H' => modifyThe LakeOptions ({· with trustHash := false})
-| 'J' => modifyThe LakeOptions ({· with outFormat := .json})
-| opt => throw <| CliError.unknownShortOption opt
-
 /-- Returns an error if the string is not valid GitHub repository name. -/
 -- Limitations derived from https://github.com/dead-claudia/github-limits
-def validateRepo? (repo : String) : Option String := Id.run do
+def validateRepo? (repo : String.Slice) : Option String := Id.run do
   unless repo.all isValidRepoChar do
     return "invalid characters in repository name"
-  match repo.split '/' |>.toStringList with
-  | [owner, name] =>
-    if owner.length > 39 then
-      return "invalid repository name; owner must be at most 390 characters long"
-    if name.length > 100 then
-      return "invalid repository name; owner must be at most 100 characters long"
-  | _ => return "invalid repository name; must contain exactly one '/'"
+  if let [owner, name] := repo.split '/' |>.toList then
+    if owner.chars.count > 39 then
+      return "invalid repository name; owner must be at most 39 characters long"
+    if name.chars.count > 100 then
+      return "invalid repository name; name must be at most 100 characters long"
+  else
+    return "invalid repository name; must contain exactly one '/'"
   return none
 where
   /-- Returns whether `c` is a valid character in GitHub repository name -/
   isValidRepoChar (c : Char) : Bool :=
     c.isAlphanum || c == '-' || c == '_' || c == '.' || c == '/'
 
-def lakeLongOption : (opt : String) → CliM PUnit
-| "--quiet"       => modifyThe LakeOptions ({· with verbosity := .quiet})
-| "--verbose"     => modifyThe LakeOptions ({· with verbosity := .verbose})
-| "--update"      => modifyThe LakeOptions ({· with updateDeps := true})
-| "--keep-toolchain" => modifyThe LakeOptions ({· with updateToolchain := false})
-| "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
-| "--old"         => modifyThe LakeOptions ({· with oldMode := true})
-| "--text"        => modifyThe LakeOptions ({· with outFormat := .text})
-| "--json"        => modifyThe LakeOptions ({· with outFormat := .json})
-| "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
-| "--no-cache"    => modifyThe LakeOptions ({· with noCache := true})
-| "--try-cache"   => modifyThe LakeOptions ({· with noCache := false})
-| "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
-| "--offline"     => modifyThe LakeOptions ({· with offline := true})
-| "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
-| "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
-| "--force-download" => modifyThe LakeOptions ({· with forceDownload := true})
-| "--scope" => do
-  let scope ← takeOptArg "--scope" "cache scope"
-  modifyThe LakeOptions ({· with scope? := some scope, repoScope := false})
-| "--repo" => do
-  let repo ← takeOptArg "--repo" "GitHub repository"
-  if let some e := validateRepo? repo then error e
-  modifyThe LakeOptions ({· with scope? := some repo, repoScope := true})
-| "--platform" => do
-  let platform ← takeOptArg "--platform" "cache platform"
-  if platform.length > 100 then
-    error "invalid platform; platform is expected to be at most 100 characters long"
-  modifyThe LakeOptions ({· with platform? := some platform})
-| "--toolchain" => do
-  let toolchain ← takeOptArg "--toolchain" "cache toolchain"
-  let toolchain := if toolchain.isEmpty then toolchain else normalizeToolchain toolchain
-  if toolchain.length > 256 then
-    error "invalid toolchain version; toolchain is expected to be at most 256 characters long"
-  modifyThe LakeOptions ({· with toolchain? := some toolchain})
-| "--rev" => do
-  let rev ← takeOptArg "--rev" "Git revision"
-  modifyThe LakeOptions ({· with rev? := some rev})
-| "--max-revs" => do
-  let some n ← (·.toNat?) <$> takeOptArg "--max-revs" "number of revisions"
-    | error "argument to `--max-revs` should be a natural number"
-  modifyThe LakeOptions ({· with maxRevs := n})
-| "--log-level"   => do
-  let outLv ← takeOptArg' "--log-level" "log level" LogLevel.ofString?
-  modifyThe LakeOptions ({· with outLv? := outLv})
-| "--fail-level"  => do
-  let failLv ← takeOptArg' "--fail-level" "log level" LogLevel.ofString?
-  modifyThe LakeOptions ({· with failLv})
-| "--ansi"        => modifyThe LakeOptions ({· with ansiMode := .ansi})
-| "--no-ansi"     => modifyThe LakeOptions ({· with ansiMode := .noAnsi})
-| "--packages"    => do
-  let file ← takeOptArg "--packages" "package overrides file"
-  let overrides ← Manifest.loadEntries file
-  modifyThe LakeOptions fun opts =>
-    {opts with packageOverrides := opts.packageOverrides ++ overrides}
-| "--dir"         => do
-  let rootDir ← takeOptArg "--dir" "path"
-  modifyThe LakeOptions ({· with rootDir})
-| "--file"        => do
-  let configFile ← takeOptArg "--file" "path"
-  modifyThe LakeOptions ({· with configFile})
-| "--help"        => modifyThe LakeOptions ({· with wantsHelp := true})
-| "--"            => do
-  let subArgs ← takeArgs
-  modifyThe LakeOptions ({· with subArgs})
-| opt             =>  throw <| CliError.unknownLongOption opt
-
-def lakeOption :=
+def lakeShortOption : ShortOptHandler CliStateM := .ofM do
+  match (← getOptChar) with
+  | 'q' => modifyThe LakeOptions ({· with verbosity := .quiet})
+  | 'v' => modifyThe LakeOptions ({· with verbosity := .verbose})
+  | 'd' => do
+    let rootDir ← takeOptArg "path"
+    modifyThe LakeOptions ({· with rootDir})
+  | 'f' => do
+    let configFile ← takeOptArg "path"
+    modifyThe LakeOptions ({· with configFile})
+  | 'o' => do
+    let outputsFile ← takeOptArg "path"
+    modifyThe LakeOptions ({· with outputsFile? := some outputsFile})
+  | 'K' => do setConfigOpt (← takeOptArg "key-value pair")
+  | 'U' => do
+    logWarning "the '-U' shorthand for '--update' is deprecated"
+    modifyThe LakeOptions ({· with updateDeps := true})
+  | 'R' => modifyThe LakeOptions ({· with reconfigure := true})
+  | 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
+  | 'H' => modifyThe LakeOptions ({· with trustHash := false})
+  | 'J' => modifyThe LakeOptions ({· with outFormat := .json})
+  | opt => throw <| CliError.unknownShortOption opt
+
+def lakeLongOption : LongOptHandler CliStateM := .ofM do
+  match (← getOpt).copy with
+  | "--quiet"       => modifyThe LakeOptions ({· with verbosity := .quiet})
+  | "--verbose"     => modifyThe LakeOptions ({· with verbosity := .verbose})
+  | "--update"      => modifyThe LakeOptions ({· with updateDeps := true})
+  | "--keep-toolchain" => modifyThe LakeOptions ({· with updateToolchain := false})
+  | "--reconfigure" => modifyThe LakeOptions ({· with reconfigure := true})
+  | "--old"         => modifyThe LakeOptions ({· with oldMode := true})
+  | "--text"        => modifyThe LakeOptions ({· with outFormat := .text})
+  | "--json"        => modifyThe LakeOptions ({· with outFormat := .json})
+  | "--no-build"    => modifyThe LakeOptions ({· with noBuild := true})
+  | "--no-cache"    => modifyThe LakeOptions ({· with noCache := true})
+  | "--try-cache"   => modifyThe LakeOptions ({· with noCache := false})
+  | "--rehash"      => modifyThe LakeOptions ({· with trustHash := false})
+  | "--offline"     => modifyThe LakeOptions ({· with offline := true})
+  | "--wfail"       => modifyThe LakeOptions ({· with failLv := .warning})
+  | "--iofail"      => modifyThe LakeOptions ({· with failLv := .info})
+  | "--force-download" => modifyThe LakeOptions ({· with forceDownload := true})
+  | "--scope" => do
+    let scope ← takeOptArg "cache scope"
+    modifyThe LakeOptions ({· with scope? := some scope.copy, repoScope := false})
+  | "--repo" => do
+    let repo ← takeOptArg "GitHub repository"
+    if let some e := validateRepo? repo then error e
+    modifyThe LakeOptions ({· with scope? := some repo.copy, repoScope := true})
+  | "--platform" => do
+    let platform ← takeOptArg "cache platform"
+    let platform := platform.copy
+    if platform.length > 100 then
+      error "invalid platform; platform is expected to be at most 100 characters long"
+    modifyThe LakeOptions ({· with platform? := some platform})
+  | "--toolchain" => do
+    let toolchain ← takeOptArg "cache toolchain"
+    let toolchain := if toolchain.isEmpty then "" else normalizeToolchain toolchain
+    if toolchain.length > 256 then
+      error "invalid toolchain version; toolchain is expected to be at most 256 characters long"
+    modifyThe LakeOptions ({· with toolchain? := some toolchain})
+  | "--rev" => do
+    let rev ← takeOptArg "Git revision"
+    modifyThe LakeOptions ({· with rev? := some rev.copy})
+  | "--max-revs" => do
+    let maxRevs ← takeOptArg "number of revisions"
+    modifyThe LakeOptions ({· with maxRevs})
+  | "--log-level"   => do
+    let outLv ← takeOptArg "log level"
+    modifyThe LakeOptions ({· with outLv? := some outLv})
+  | "--fail-level"  => do
+    let failLv ← takeOptArg "log level"
+    modifyThe LakeOptions ({· with failLv})
+  | "--ansi"        => modifyThe LakeOptions ({· with ansiMode := .ansi})
+  | "--no-ansi"     => modifyThe LakeOptions ({· with ansiMode := .noAnsi})
+  | "--packages"    => do
+    let file ← takeOptArg "package overrides file"
+    let overrides ← Manifest.loadEntries (FilePath.mk file.copy)
+    modifyThe LakeOptions fun opts =>
+      {opts with packageOverrides := opts.packageOverrides ++ overrides}
+  | "--dir"         => do
+    let rootDir ← takeOptArg "path"
+    modifyThe LakeOptions ({· with rootDir := FilePath.mk rootDir.copy})
+  | "--file"        => do
+    let configFile ← takeOptArg "path"
+    modifyThe LakeOptions ({· with configFile := FilePath.mk configFile.copy})
+  | "--help"        => modifyThe LakeOptions ({· with wantsHelp := true})
+  | "--"            => do
+    let subArgs ← takeArgs
+    modifyThe LakeOptions ({· with subArgs})
+  | opt             =>  throw <| CliError.unknownLongOption opt
+
+def lakeOption : OptHandler CliStateM :=
   option {
     short := lakeShortOption
     long := lakeLongOption
     longShort := shortOptionWithArg lakeShortOption
   }
 
+def processLakeOptions : CliM PUnit := fun args => do
+  let args ← collectArgs args lakeOption -- specializes `collectArgs`
+  return (⟨⟩, args.toList)
+
+def processLeadingLakeOptions : CliM PUnit := fun args => do
+  let args ← processLeadingOptions args lakeOption -- specializes `processLeadingOptions`
+  return (⟨⟩, args)
+
+theorem run_processLeadingLakeOptions {as} :
+  StateT.run processLeadingLakeOptions as = (⟨(), ·⟩) <$> processLeadingOptions as lakeOption
+:= by rfl
+
 /-! ## Actions -/
 
 /-- Verify the Lean version Lake was built with matches that of the give Lean installation. -/
@@ -374,9 +416,9 @@ namespace cache
   if pkg.isPlatformIndependent then "" else platform
 
 protected def get : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
-  let mappings? ← takeArg?
+  let mappings? : Option FilePath ← takeArg?
   noArgsRem do
   let cfg ← mkLoadConfig opts
   let ws ← loadWorkspace cfg
@@ -472,8 +514,8 @@ where
     return map
 
 protected def put : CliM PUnit := do
-  processOptions lakeOption
-  let file ← takeArg "mappings"
+  processLakeOptions
+  let file : FilePath ← takeArg "mappings"
   let opts ← getThe LakeOptions
   let some scope := opts.scope?
     | error "the `--scope` or `--repo` option must be set for `cache put`"
@@ -513,8 +555,8 @@ where
     To use `cache put`, these environment variables must be set to non-empty strings."
 
 protected def add : CliM PUnit := do
-  processOptions lakeOption
-  let file ← takeArg "mappings"
+  processLakeOptions
+  let file : FilePath ← takeArg "mappings"
   let pkg? ← takeArg?
   let opts ← getThe LakeOptions
   noArgsRem do
@@ -544,7 +586,7 @@ def cacheCli : (cmd : String) → CliM PUnit
 namespace script
 
 protected def list : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let config ← mkLoadConfig (← getThe LakeOptions)
   noArgsRem do
     let ws ← loadWorkspace config
@@ -553,7 +595,7 @@ protected def list : CliM PUnit := do
         IO.println script.name
 
 protected nonrec def run : CliM PUnit := do
-  processLeadingOptions lakeOption  -- between `lake [script] run` and `<name>`
+  processLeadingLakeOptions  -- between `lake [script] run` and `<name>`
   let config ← mkLoadConfig (← getThe LakeOptions)
   let ws ← loadWorkspace config
   if let some spec ← takeArg? then
@@ -566,7 +608,7 @@ protected nonrec def run : CliM PUnit := do
     exit 0
 
 protected def doc : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let spec ← takeArg "script name"
   let config ← mkLoadConfig (← getThe LakeOptions)
   noArgsRem do
@@ -591,21 +633,21 @@ def scriptCli : (cmd : String) → CliM PUnit
 /-! ### `lake` CLI -/
 
 protected def new : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let name ← takeArg "package name"
   let (tmp, lang) ← parseTemplateLangSpec <| ← takeArgD ""
   noArgsRem do new name tmp lang (← opts.computeEnv) opts.rootDir opts.offline
 
 protected def init : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let name := ← takeArgD "."
   let (tmp, lang) ← parseTemplateLangSpec <| ← takeArgD ""
   noArgsRem do init name tmp lang (← opts.computeEnv) opts.rootDir opts.offline
 
 protected def build : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let ws ← loadWorkspace config
@@ -618,12 +660,12 @@ protected def build : CliM PUnit := do
   ws.runBuild (buildSpecs specs) buildConfig
 
 protected def checkBuild : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
   noArgsRem do exit <| if pkg.defaultTargets.isEmpty then 1 else 0
 
 protected def query : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let ws ← loadWorkspace config
@@ -635,7 +677,7 @@ protected def query : CliM PUnit := do
   results.forM (IO.println ·)
 
 protected def queryKind : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let ws ← loadWorkspace config
@@ -655,21 +697,21 @@ protected def queryKind : CliM PUnit := do
     | none => error "build failed"
 
 protected def resolveDeps : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   noArgsRem do
   discard <| loadWorkspace config
 
 protected def update : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let config ← mkLoadConfig opts
   let toUpdate := (← getArgs).foldl (·.insert <| stringToLegalOrSimpleName ·) {}
   updateManifest config toUpdate
 
 protected def pack : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let file? ← takeArg?
   noArgsRem do
   let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
@@ -677,7 +719,7 @@ protected def pack : CliM PUnit := do
   ws.root.pack file
 
 protected def unpack : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let file? ← takeArg?
   noArgsRem do
   let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
@@ -685,7 +727,7 @@ protected def unpack : CliM PUnit := do
   ws.root.unpack file
 
 protected def upload : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let tag ← takeArg "release tag"
   noArgsRem do
   let ws ← loadWorkspace (← mkLoadConfig (← getThe LakeOptions))
@@ -693,7 +735,7 @@ protected def upload : CliM PUnit := do
 
 protected def cache : CliM PUnit := do
   if let some cmd ← takeArg? then
-    processLeadingOptions lakeOption -- between `lake cache <cmd>` and args
+    processLeadingLakeOptions -- between `lake cache <cmd>` and args
     if (← getWantsHelp) then
       IO.println <| helpCache cmd
     else
@@ -702,7 +744,7 @@ protected def cache : CliM PUnit := do
     throw <| CliError.missingCommand
 
 protected def setupFile : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let loadConfig ← mkLoadConfig opts
   let buildConfig := mkBuildConfig opts
@@ -717,7 +759,7 @@ protected def setupFile : CliM PUnit := do
   exit <| ← setupFile loadConfig filePath header buildConfig
 
 protected def test : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let ws ← loadWorkspace (← mkLoadConfig opts)
   noArgsRem do
@@ -725,12 +767,12 @@ protected def test : CliM PUnit := do
   exit <| ← x.run (mkLakeContext ws)
 
 protected def checkTest : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
   noArgsRem do exit <| if pkg.testDriver.isEmpty then 1 else 0
 
 protected def lint : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let ws ← loadWorkspace (← mkLoadConfig opts)
   noArgsRem do
@@ -738,12 +780,12 @@ protected def lint : CliM PUnit := do
   exit <| ← x.run (mkLakeContext ws)
 
 protected def checkLint : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let pkg ← loadPackage (← mkLoadConfig (← getThe LakeOptions))
   noArgsRem do exit <| if pkg.lintDriver.isEmpty then 1 else 0
 
 protected def clean : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let config ← mkLoadConfig (← getThe LakeOptions)
   let ws ← loadWorkspace config
   let pkgSpecs ← takeArgs
@@ -758,7 +800,7 @@ protected def clean : CliM PUnit := do
 
 protected def script : CliM PUnit := do
   if let some cmd ← takeArg? then
-    processLeadingOptions lakeOption -- between `lake script <cmd>` and args
+    processLeadingLakeOptions -- between `lake script <cmd>` and args
     if (← getWantsHelp) then
       IO.println <| helpScript cmd
     else
@@ -767,7 +809,7 @@ protected def script : CliM PUnit := do
     throw <| CliError.missingCommand
 
 protected def serve : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let args := opts.subArgs.toArray
   let config ← mkLoadConfig opts
@@ -799,7 +841,7 @@ protected def exe : CliM PUnit := do
   exit <| ← (Lake.env exeFile.toString args.toArray).run <| mkLakeContext ws
 
 protected def lean : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let leanFile ← takeArg "Lean file"
   let opts ← getThe LakeOptions
   noArgsRem do
@@ -808,7 +850,7 @@ protected def lean : CliM PUnit := do
   exit rc
 
 protected def translateConfig : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let cfg ← mkLoadConfig opts
   let lang ← parseLangSpec (← takeArg "configuration language")
@@ -840,7 +882,7 @@ structure ReservoirConfig where
   deriving Lean.ToJson
 
 protected def reservoirConfig : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let cfg ← mkLoadConfig opts
   let _ ← id do
@@ -872,7 +914,7 @@ protected def reservoirConfig : CliM PUnit := do
   IO.println (toJson cfg).pretty
 
 protected def versionTags : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   let opts ← getThe LakeOptions
   let cfg ← mkLoadConfig opts
   noArgsRem do
@@ -883,7 +925,7 @@ protected def versionTags : CliM PUnit := do
       IO.println tag
 
 protected def selfCheck : CliM PUnit := do
-  processOptions lakeOption
+  processLakeOptions
   noArgsRem do verifyInstall (← getThe LakeOptions)
 
 protected def help : CliM PUnit := do
@@ -932,19 +974,46 @@ def lake : CliM PUnit := do
   match (← getArgs) with
   | [] => IO.println usage
   | ["--version"] => IO.println uiVersionString
-  | _ => -- normal CLI
-    processLeadingOptions lakeOption -- between `lake` and command
-    if let some cmd ← takeArg? then
-      processLeadingOptions lakeOption -- between `lake <cmd>` and args
-      if (← getWantsHelp) then
-        IO.println <| help cmd
-      else
-        lakeCli cmd
+  | _ => go -- normal CLI
+where @[inline] go := do
+  processLeadingLakeOptions -- between `lake` and command
+  if let some cmd ← takeArg? then
+    processLeadingLakeOptions -- between `lake <cmd>` and args
+    if (← getWantsHelp) then
+      IO.println <| help cmd
     else
-      if (← getWantsHelp) then
-        IO.println usage
-      else
-        throw <| CliError.missingCommand
+      lakeCli cmd
+  else
+    if (← getWantsHelp) then
+      IO.println usage
+    else
+      throw <| CliError.missingCommand
 
 public def cli (args : List String) : BaseIO ExitCode :=
-  inline <| (lake).run args
+  (lake).run args
+
+/- CLI sanity check -/
+
+theorem run_lake_cons_of_ne_version (h : a ≠ "--version") :
+  StateT.run lake (a :: as) = StateT.run lake.go (a :: as)
+:= by
+  simp only [lake, StateT.run_bind, ArgsT.run_getArgs, pure_bind]
+  split
+  · contradiction
+  · next h_eq => simp [h] at h_eq
+  · rfl
+
+theorem cli_of_isArg (h : IsArg cmd) :
+  cli [cmd] = (StateT.run' (lakeCli cmd) []).run [cmd]
+:= by
+  have ne_version : cmd ≠ "--version" := h.ne_of_isOpt (by decide)
+  simp only [cli, CliM.run, CliStateM.run, StateT.run'_eq]
+  simp only [run_lake_cons_of_ne_version ne_version, lake.go, getWantsHelp]
+  simp [processLeadingOptions_cons_of_isArg h, run_processLeadingLakeOptions, parseArg]
+
+theorem cli_help :
+  cli ["help"] = (CliStateM.runIO <| IO.println usage).run ["help"]
+:= by
+  have isArg_help : IsArg "help" := by decide
+  have lakeCli_help : lakeCli "help" = lake.help := by rfl
+  simp [cli_of_isArg isArg_help, lakeCli_help, lake.help, monadLift, MonadLift.monadLift]
diff --git a/src/lake/Lake/Util/Cli.lean b/src/lake/Lake/Util/Cli.lean
index 3a07c0edf333..da950efd8d63 100644
--- a/src/lake/Lake/Util/Cli.lean
+++ b/src/lake/Lake/Util/Cli.lean
@@ -6,185 +6,772 @@ Authors: Mac Malone
 module
 
 prelude
-import Init.Data.Array.Basic
-public import Init.Data.String.TakeDrop
-import Init.Data.String.Slice
-public import Init.Data.String.Search
+public import Init.Data.String.Slice
+import Init.Data.String.Search
+import Init.Data.String.TakeDrop
 
-namespace Lake
+set_option doc.verso true
+set_option linter.missingDocs true
+
+/-! # Lake's CLI API
 
-/-!
-Defines the abstract CLI interface for Lake.
+The abstract API used by Lake to parse command line arguments.
 -/
 
-/-! # Types -/
+namespace Lake
+
+/-! ## Argument-related Types -/
+
+/-- A command line argument. -/
+@[expose] -- for codegen
+public def Arg := String
+
+/-- Type class for monads equipped with an command line argument. -/
+public abbrev MonadArg (m) := MonadReaderOf Arg m
 
-@[expose]  -- for codegen
-public def ArgList := List String
+/-- A List of command line arguments. -/
+@[expose] public def ArgList := List String
 
-@[inline] public def ArgList.mk (args : List String) : ArgList :=
-  args
+public noncomputable instance : SizeOf ArgList := inferInstanceAs (SizeOf (List String))
 
+/-- Type class for monads equipped with a command line argument list. -/
+public class MonadArgs (m : Type → Type v) where
+  /-- Returns the remaining argument list. -/
+  getArgs : m (List String)
+  /-- Removes and returns the head of the remaining argument list (or {lean}`none` if empty). -/
+  takeArg? : m (Option String)
+  /-- Removes and returns  the remaining argument list, leaving only an empty list. -/
+  takeArgs : m (List String)
+
+export MonadArgs (getArgs takeArgs)
+
+public instance [MonadLift m n] [MonadArgs m] : MonadArgs n where
+  getArgs := liftM (m := m) getArgs
+  takeArg? := liftM (m := m) MonadArgs.takeArg?
+  takeArgs := liftM (m := m) takeArgs
+
+@[always_inline]
+public instance  [MonadStateOf ArgList m] : MonadArgs m where
+  getArgs := get
+  takeArg? := modifyGet fun | [] => (none, []) | arg :: args => (some arg, args)
+  takeArgs := modifyGet fun args => (args, [])
+
+/-- A monad transformer to equip a monad with a command-line argument list. -/
+@[expose] -- for codegen
 public abbrev ArgsT := StateT ArgList
 
-@[inline] public def ArgsT.run (args : List String) (self : ArgsT m α) : m (α × List String) :=
+namespace ArgsT
+
+/--
+Executes an action in the underlying monad {lean}`m` with the added state of a command-line
+argument list. It returns the monadic value paired with the final argument list.
+-/
+public abbrev run (self : ArgsT m α) (args : List String) : m (α × List String) :=
   StateT.run self args
 
-@[inline] public def ArgsT.run' [Functor m] (args : List String) (self : ArgsT m α) : m α :=
+/--
+Executes an action in the underlying monad {lean}`m` with the added state of a command-line
+argument list. It returns the monadic value, discarding any remaining arguments list.
+-/
+public abbrev run' [Functor m] (self : ArgsT m α) (args : List String) : m α :=
   StateT.run' self args
 
-public structure OptionHandlers (m : Type u → Type v) (α : Type u) where
-  /-- Process a long option (ex. `--long` or `"--long foo bar"`). -/
-  long : String → m α
-  /-- Process a short option (ex. `-x` or `--`). -/
-  short : Char → m α
-  /-- Process a long short option (ex. `-long`, `-xarg`, `-xyz`). -/
-  longShort : String → m α
+@[simp] public theorem run_getArgs {as : List String} [Monad m]  :
+  StateT.run (σ := ArgList) (m := m) getArgs as = pure (as, as)
+:= by rfl
+
+@[simp] public theorem run_takeArgs {as : List String} [Monad m] :
+  StateT.run (σ := ArgList) (m := m) takeArgs as = pure (as, [])
+:= by rfl
+
+end ArgsT
+
+/-- A monad transformer to equip a monad with a state that monotonically non-increasing in size. -/
+@[expose] -- for codegen
+public def MonoStateT (σ : Type u) [SizeOf σ] (m : Type max u v → Type w) (α : Type v) :=
+  (s : σ) → m (α × {s' : σ // sizeOf s' ≤ sizeOf s})
+
+namespace MonoStateT
+
+/-- Construct the monad transformer from its functional definition. -/
+@[inline] public def mk
+  [SizeOf σ] (fn : (s : σ) → m (α × {s' : σ // sizeOf s' ≤ sizeOf s}))
+: MonoStateT σ m α := fn
+
+/--
+Executes an action from a monad with added state in the underlying monad {lean}`m`.
+Given an initial state {lean}`init : σ`, it returns a value paired with the final state,
+which is guaranteed to be a most the size of the initial state.
+-/
+@[inline] public def run
+  [SizeOf σ] (init : σ) (self : MonoStateT σ m α)
+: m (α × {s' : σ // sizeOf s' ≤ sizeOf init}) := self init
+
+@[inline, always_inline, inherit_doc Pure.pure]
+public protected def pure [SizeOf σ] [Pure m] (a : α) : MonoStateT σ m α :=
+  fun args => pure ⟨a, ⟨args, Nat.le_refl _⟩⟩
+
+public instance [SizeOf σ] [Pure m] : Pure (MonoStateT σ m) := ⟨MonoStateT.pure⟩
+
+@[inline, always_inline, inherit_doc Bind.bind]
+public protected def bind
+  [SizeOf σ] [Monad m] (x : MonoStateT σ m α) (f : α → MonoStateT σ m β)
+: MonoStateT σ m β :=
+  fun si => bind (x si) fun ⟨a, ⟨sa, ha⟩⟩ => bind (f a sa) fun (b, ⟨sb, hb⟩) =>
+    pure ⟨b, ⟨sb, Nat.le_trans hb ha⟩⟩
+
+public instance [SizeOf σ] [Monad m] : Bind (MonoStateT σ m) := ⟨MonoStateT.bind⟩
+public instance [SizeOf σ] [Monad m] : Monad (MonoStateT σ m) := {}
+
+/-- Runs an action from the underlying monad in the monad with state. The state is not modified. -/
+@[always_inline, inline, expose]
+public protected def lift [SizeOf σ] [Monad m] (t : m α) : MonoStateT σ m α :=
+  fun s => do let a ← t; pure (a, ⟨s, Nat.le_refl _⟩)
+
+public instance [SizeOf σ] [Monad m] : MonadLift m (MonoStateT σ m) := ⟨MonoStateT.lift⟩
+
+@[always_inline]
+public instance [SizeOf σ] [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (MonoStateT σ m) where
+  throw    := MonoStateT.lift ∘ throwThe ε
+  tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
+
+/--
+Applies a function to the current state that both computes a new state and
+a value. The new state replaces the current state, and the value is returned.
+-/
+public protected def modifyGet
+  [SizeOf σ] [Monad m] (f : (s : σ) → (α × {s' : σ // sizeOf s' ≤ sizeOf s}))
+: MonoStateT σ m α := fun s => pure (f s)
+
+/-- Retrieves the current value of the monad's mutable state. -/
+@[inline, always_inline]
+public protected def get [SizeOf σ] [Pure m] : MonoStateT σ m σ :=
+  fun s => pure ⟨s, ⟨s, Nat.le_refl _⟩⟩
+
+end MonoStateT
+
+/-- A monad transformer to equip a monad with a monotonically non-increasing argument list. -/
+public abbrev MonoArgsT (m : Type → Type v) := MonoStateT ArgList m
+
+namespace MonoArgsT
+
+@[inline, always_inline, inherit_doc MonadArgs.getArgs]
+public protected def get [Pure m] : MonoArgsT m (List String) :=
+  MonoStateT.get
+
+@[inline, always_inline, inherit_doc MonadArgs.takeArg?]
+public protected def takeArg? [Monad  m] : MonoArgsT m (Option String) :=
+  MonoStateT.modifyGet fun
+    | [] => (none, ⟨[], Nat.le_refl _⟩)
+    | arg :: args => (some arg, ⟨args, mono_cons⟩)
+where
+  mono_cons {a} {as : List String} : sizeOf as ≤ sizeOf (a :: as) := by simp
+
+@[inline, always_inline, inherit_doc MonadArgs.takeArgs]
+public protected def takeArgs [Monad  m] : MonoArgsT m (List String) :=
+   MonoStateT.modifyGet fun args => (args, ⟨[], mono_nil⟩)
+where
+  mono_nil {as : List String} : sizeOf ([] : List String) ≤ sizeOf as := by
+    cases as
+    · simp
+    · simp only [List.nil.sizeOf_spec, List.cons.sizeOf_spec]
+      omega
+
+public instance [Monad m] : MonadArgs (MonoArgsT m) where
+  getArgs := MonoArgsT.get
+  takeArg? := MonoArgsT.takeArg?
+  takeArgs :=  MonoArgsT.takeArgs
+
+end MonoArgsT
+
+/-! ## Monadic Argument Parsing Utilities -/
+
+/-- Type class for parsing command line arguments. -/
+public class MonadParseArg (α : Type u) (m : Type u → Type v) where
+  /-- Parse a command line argument {lean}`arg` into the type {lean}`α`. -/
+  parseArg (arg : String.Slice) : m α
+
+export MonadParseArg (parseArg)
+
+public instance [MonadLift m n] [MonadParseArg α  m] : MonadParseArg α n where
+  parseArg arg := liftM (m := m) <| parseArg arg
+
+public instance [Pure m] : MonadParseArg String m := ⟨(pure ·.copy)⟩
+@[default_instance] public instance [Pure m] : MonadParseArg String.Slice m := ⟨(pure ·)⟩
+
+/-- Type class for indicating a missing argument. -/
+public class MonadThrowExpectedArg  (m : Type u → Type v) where
+  /-- Throw an error indicating a missing argument described by {lean}`descr`. -/
+  throwExpectedArg {α} (descr : String) : m α
+
+export MonadThrowExpectedArg (throwExpectedArg)
+
+public instance [MonadLift m n] [MonadThrowExpectedArg m] : MonadThrowExpectedArg n where
+  throwExpectedArg descr := liftM (m := m) <| throwExpectedArg descr
+
+/--
+Removes and returns the head of the remaining argument list, parsing the argument into {lean}`α`.
+
+If no argument is available, returns {lean}`none`.
+-/
+@[inline] public def takeArg?
+  [Monad m] [MonadArgs m] [MonadParseArg α m]
+: m (Option α) := do
+  if let some arg ← MonadArgs.takeArg? then
+    return some (← parseArg arg)
+  else
+    return none
+
+@[simp] public theorem ArgsT.run_takeArg?_nil
+  [Monad m] [LawfulMonad m] {_ : MonadParseArg α (ArgsT m)} :
+  StateT.run (σ := ArgList) (m := m) takeArg? [] = pure ((none : Option α), [])
+:= by simp [takeArg?, MonadArgs.takeArg?]
+
+@[simp] public theorem ArgsT.run_takeArg?_cons
+  [Monad m] [LawfulMonad m] [MonadParseArg α (ArgsT m)] :
+  StateT.run (σ := ArgList) (m := m) (α := Option α) takeArg? (a :: as) =
+  StateT.run (σ := ArgList) (some <$> parseArg a) as
+:= by simp [takeArg?, MonadArgs.takeArg?]
+
+/--
+Removes and returns the head of the remaining argument list, parsing the argument into {lean}`α`.
+
+If no argument is available, returns {lean}`default`.
+-/
+@[inline] public def takeArgD
+  [Monad m] [MonadArgs m] [MonadParseArg α m] (default : α)
+: m α := return (← takeArg?).getD default
+
+@[simp] public theorem takeArgD_eq_getD_takeArg?
+  [Monad m] [LawfulMonad m] [MonadArgs m] [MonadParseArg α m] :
+  takeArgD (α := α) (m := m) d = (·.getD d) <$> takeArg?
+:= by simp [takeArgD]
+
+/--
+Removes and returns the head of the remaining argument list, parsing the argument into {lean}`α`.
+
+If no argument is available,, errors using {name}`throwExpectedArg` with {lean}`descr`.
+-/
+@[inline] public def takeArg
+  [Monad m] [MonadArgs m] [MonadParseArg α m] [MonadThrowExpectedArg m] (descr : String)
+: m α := do
+  if let some arg ← MonadArgs.takeArg? then
+    parseArg arg
+  else
+    throwExpectedArg descr
+
+@[simp] public theorem ArgsT.run_takeArg_nil
+  [Monad m] [LawfulMonad m] [MonadParseArg α (ArgsT m)] [MonadThrowExpectedArg m] :
+  StateT.run (σ := ArgList) (m := m) (α := α) (takeArg d) [] =
+  ((·, [])) <$> throwExpectedArg (m := m) d
+:= by simp [takeArg, MonadArgs.takeArg?, throwExpectedArg]
+
+@[simp] public theorem ArgsT.run_takeArg_cons
+  [Monad m] [LawfulMonad m] [MonadParseArg α (ArgsT m)] {_ : MonadThrowExpectedArg m} :
+  StateT.run (σ := ArgList) (m := m) (α := α) (takeArg d) (a :: as) =
+  StateT.run (σ := ArgList) (parseArg a) as
+:= by simp [takeArg, MonadArgs.takeArg?]
+
+/-! ## Argument Handler Type -/
+
+/-- A monadic callback for an arbitrary command line argument. -/
+@[expose] -- for codegen
+public def ArgHandler (m : Type → Type v) :=
+  (arg : String) → (args : List String) → m {remArgs : List String // sizeOf remArgs ≤ sizeOf args}
+
+/-- Get the current command line argument of the context (e.g., in an {name}`ArgHandler`). -/
+@[inline] public def getArg [MonadArg m] : m String :=
+  read
+
+/-- A monad transformer to equip a monad with a command line argument. -/
+public abbrev ArgT (m) := ReaderT Arg <| MonoArgsT m
+
+/--
+Construct an argument handler from a monadic action.
+
+The argument under analysis is available via {name}`getArg`. Further arguments are available
+through {name}`getArgs` and can be modify through the various {name}`MonadArgs` utilities
+(e.g., {name}`takeArg`).
+-/
+@[inline] public def ArgHandler.ofM [Monad m] (x : ArgT m Unit) : ArgHandler m :=
+  fun arg args => (·.2) <$> x arg args
+
+/-! ## Argument Predicates -/
+
+/--
+{lean}`IsOpt arg` holds if {lean}`arg` is an command line option.
+That is, {lean}`arg` is of the form `-(.+)`.
+-/
+public structure IsOpt (arg : String) : Prop where
+  startPos_ne_endPos : arg.startPos ≠ arg.endPos
+  get_startPos : arg.startPos.get startPos_ne_endPos = '-'
+  next_startPos_ne_endPos : arg.startPos.next startPos_ne_endPos ≠ arg.endPos
+
+/--
+{lean}`IsArg arg` holds if {lean}`arg` is a non-option command-line argument
+That is, it is not empty and is not of the form `-(.+)`.
+-/
+public structure IsArg (arg : String) : Prop where
+  ne_empty : arg ≠ ""
+  not_isOpt : ¬ IsOpt arg
+
+namespace IsOpt
+
+/-- A decision procedure for determining if {lean}`arg` is an option. -/
+@[reducible, expose] public def dec (arg : String) : Decidable (IsOpt arg) :=
+  if h0 : arg.startPos = arg.endPos then
+    isFalse fun ⟨_, _, _⟩ => by contradiction
+  else
+    if hc : arg.startPos.get h0 = '-' then
+      if h1 : arg.startPos.next h0 = arg.endPos then
+        isFalse fun ⟨_, _, _⟩ => by contradiction
+      else
+        isTrue ⟨h0, hc, h1⟩
+    else
+      isFalse fun ⟨_, _, _⟩ => by contradiction
+
+public instance instDecidable {arg : String} : Decidable (IsOpt arg) := dec arg
+
+public theorem ne_empty {arg} (h : IsOpt arg) : arg ≠ "" :=
+  String.startPos_eq_endPos_iff.subst h.startPos_ne_endPos
+
+public theorem not_isArg {arg} (h : IsOpt arg) : ¬ IsArg arg :=
+  fun h' => h'.not_isOpt h
+
+public theorem ne_of_isArg (ha : IsOpt a) (hb : IsArg b) : a ≠ b :=
+  fun heq => ha.not_isArg.elim (heq ▸ hb)
 
-/-! # Utilities -/
+public theorem offset_next_startPos (h : IsOpt a) :
+  (a.startPos.next h.startPos_ne_endPos).offset = ⟨1⟩
+:= by simp [String.Pos.Raw.ext_iff, h.get_startPos, Char.utf8Size]
 
-variable [Monad m] [MonadStateOf ArgList m]
+/--
+The position in {lean}`arg` after the initial {lit}`-`
+(e.g., {lit}`x` in {lit}`-x` or {lit}`-` in {lit}`--long`).
+-/
+@[inline] public def shortPos (h : IsOpt arg) : arg.Pos :=
+  arg.pos ⟨1⟩ <| by
+    rw [← h.offset_next_startPos]
+    apply String.Pos.isValid
+
+public theorem shortPos_eq (h : IsOpt arg) :
+  h.shortPos = arg.startPos.next h.startPos_ne_endPos
+:= by simp [shortPos, String.Pos.ext_iff, -String.Pos.offset_next, h.offset_next_startPos]
+
+public theorem shortPos_ne_endPos (h : IsOpt arg) : h.shortPos ≠ arg.endPos := by
+  rw [shortPos_eq]
+  exact h.next_startPos_ne_endPos
+
+/-- The character in {lean}`arg` after the initial {lit}`-`. -/
+@[inline] public def shortChar (h : IsOpt arg) : Char :=
+  h.shortPos.get h.shortPos_ne_endPos
+
+/-- The position in {lean}`arg` after {lean}`shortChar` (e.g., {lit}`y` in {lit}`-xy`). -/
+@[inline] public def afterShortPos (h : IsOpt arg) : arg.Pos :=
+  h.shortPos.next h.shortPos_ne_endPos
+
+public theorem afterShortPos_eq (h : IsOpt arg) :
+  h.afterShortPos = h.shortPos.next h.shortPos_ne_endPos
+:= by rfl
+
+/-- The first two characters of {lean}`arg` (e.g., {lit}`-x` in {lit}`-x=arg`). -/
+@[inline] public def shortOpt (h : IsOpt arg) : String.Slice :=
+  arg.sliceTo h.afterShortPos
+
+public theorem shortOpt_eq (h : IsOpt arg) :
+  h.shortOpt = arg.sliceTo h.afterShortPos
+:= by rfl
+
+/-- The remainder of {lean}`arg` after {lean}`shortChar` (e.g., {lit}`=arg` in {lit}`-x=arg`). -/
+@[inline] public def shortTail (h : IsOpt arg) : String.Slice :=
+  arg.sliceFrom h.afterShortPos
+
+public theorem shortTail_eq (h : IsOpt arg) :
+  h.shortTail = arg.sliceFrom h.afterShortPos
+:= by rfl
+
+end IsOpt
+
+namespace IsArg
+
+/-- A decision procedure for determining if {lean}`arg` is an non-option command line argument. -/
+@[reducible, expose] public def dec (arg : String) : Decidable (IsArg arg) :=
+  if h0 : arg.startPos = arg.endPos then
+    isFalse fun h => h.ne_empty (String.startPos_eq_endPos_iff.mp h0)
+  else
+    have ne_empty := String.startPos_eq_endPos_iff.subst h0
+    if hc : arg.startPos.get h0 = '-' then
+      if h1 : arg.startPos.next h0 = arg.endPos then
+        isTrue ⟨ne_empty, fun h => h.next_startPos_ne_endPos h1⟩
+      else
+        isFalse fun h => h.not_isOpt ⟨h0, hc, h1⟩
+    else
+      isTrue ⟨ne_empty, fun h => hc h.get_startPos⟩
+
+public instance instDecidable {arg : String} : Decidable (IsArg arg) := dec arg
+
+public theorem ne_of_isOpt (ha : IsArg a) (hb : IsOpt b) : a ≠ b :=
+  fun heq => ha.not_isOpt.elim (heq ▸ hb)
+
+public theorem startPos_ne_endPos (h : IsArg a) : a.startPos ≠ a.endPos :=
+  String.startPos_eq_endPos_iff.symm.subst h.ne_empty
+
+theorem startPos_wf (h : IsArg a) :
+  ¬ (a.startPos.get h.startPos_ne_endPos = '-' ∧ ¬ a.startPos.next h.startPos_ne_endPos = a.endPos)
+:= by
+  intro h'
+  refine h.not_isOpt.elim ⟨?_, h'.1, h'.2⟩
+  simpa using h.ne_empty
+
+end IsArg
+
+/-! ## Option-related Types -/
+
+/-- A command line option. -/
+@[expose] -- for codegen
+public def Opt := String.Slice
+
+/-- Type class for monads equipped with an command line option. -/
+public abbrev MonadOpt (m) := MonadReaderOf Opt m
+
+/-- An optional command line option argument. -/
+@[expose] -- for codegen
+public def OptArg := Option String.Slice
+
+/-- Type class for monads equipped with an optional command line option argument. -/
+public abbrev MonadOptArg (m) := MonadReaderOf OptArg m
+
+/-- A monad transformer to equip a monad with a command line option and optional argument. -/
+public abbrev OptT (m) := ReaderT Opt <| ReaderT OptArg <| MonoArgsT m
+
+/-- The character of a command line short option (e.g., {lit}`x` of {lit}`-x`). -/
+@[expose] -- for codegen
+public def OptChar := Char
+
+/-- Type class for monads equipped with a command line short option. -/
+public abbrev MonadOptChar (m) := MonadReaderOf OptChar m
+
+/-! ## Monadic Option Utilities -/
+
+/-- Get the command line option of the current context (e.g., in an option handler). -/
+@[inline] public def getOpt [MonadOpt m] : m String.Slice :=
+  read
+
+/--
+Get the character of the command line short option of the current context
+(e.g., in an option handler).
+-/
+@[inline] public def getOptChar [MonadOptChar m] : m Char :=
+  read
+
+/-- Get the option argument (if any). -/
+@[inline] def getOptArg? [MonadOptArg m] : m (Option String.Slice) :=
+  read
+
+/--
+Returns the option argument or, if {lean}`none`, removes and returns
+the head of the remaining argument list.
+
+Parses the argument into {lean}`α`.
+If no argument is available, errors using {name}`throwExpectedArg` with {lean}`descr`.
+-/
+@[inline] public def takeOptArg
+  [Monad m] [MonadOptArg m] [MonadArgs m]
+  [MonadParseArg α m] [MonadThrowExpectedArg m]
+  (descr : String)
+: m α := do
+  if let some arg ← getOptArg? then
+    parseArg arg
+  else if let some arg ← takeArg? then
+    parseArg arg
+  else
+    throwExpectedArg descr
+
+/-! ## Option Handler Types -/
+
+/-- A monadic callback for an arbitrary option (e.g., short or long). -/
+@[expose] -- for codegen
+public def OptHandler (m : Type → Type v) :=
+  (arg : String) → IsOpt arg →
+  (args : List String) → m {remArgs : List String // sizeOf remArgs ≤ sizeOf args}
+
+/-- A monad transformer to equip a monad with a long option and optional argument. -/
+public abbrev LongOptT (m) := OptT m
+
+/-- A monadic callback for a long option (e.g., {lit}`--long` or {lit}`--long=arg`). -/
+@[expose] -- for codegen
+public def LongOptHandler (m : Type → Type v) :=
+  (opt : String.Slice) → (optArg? : Option String.Slice) →
+  (args : List String) → m {remArgs : List String // sizeOf remArgs ≤ sizeOf args}
+
+/--
+Construct an long option handler from a monadic action.
 
-/-- Get the remaining argument list. -/
-@[inline] public def getArgs : m (List String) :=
-  get
+The name of the option (e.g., {lit}`-long` or {lit}`--long`) is available via {name}`getOpt`.
+An argument for the option (e.g., {lit}`arg` in {lit}`--long=arg` or {lit}`--long arg`) can be
+accessed through {name}`takeArg?`.
+-/
+@[inline] public def LongOptHandler.ofM [Monad m] (x : LongOptT m Unit) : LongOptHandler m :=
+  fun opt optArg? args => (·.2) <$> x opt optArg? args
+
+/-- A monadic callback for a short option (e.g., {lit}`-x` or {lit}`-x=arg`). -/
+@[expose] -- for codegen
+public def ShortOptHandler (m : Type → Type v) :=
+  (optChar : Char) → (opt : String.Slice) → (optArg? : Option String.Slice) →
+  (args : List String) → m {remArgs : List String // sizeOf remArgs ≤ sizeOf args}
+
+/-- A monad transformer to equip a monad with a short option and optional argument. -/
+public abbrev ShortOptT (m) := ReaderT OptChar <| OptT m
+
+/--
+Construct an short option handler from a monadic action.
+
+The name of the option (e.g., {lit}`-x`) is available via {name}`getOpt`, and
+the character of the option (e.g., {lit}`x` in {lit}`-x`) is available via {name}`getOptChar`,
 
-/-- Replace the argument list. -/
-@[inline] public def setArgs (args : List String) : m PUnit :=
-  set (ArgList.mk args)
+An argument for the option (e.g., {lit}`arg` in {lit}`-x=arg` or {lit}`-x arg`) can be accessed
+through  {name}`takeOptArg`.
+-/
+@[inline] public def ShortOptHandler.ofM [Monad m] (x : ShortOptT m Unit) : ShortOptHandler m :=
+  fun optChar opt optArg? args => (·.2) <$> x optChar opt optArg? args
+
+/-- A monadic callback for a long short option (e.g., {lit}`-long` or {lit}`-long=short`). -/
+@[expose] -- for codegen
+public def LongShortOptHandler (m : Type → Type v)  :=
+  OptHandler m
 
-/-- Take the head of the remaining argument list (or none if empty). -/
-@[inline] public def takeArg? : m (Option String) :=
-  modifyGet fun | [] => (none, []) | arg :: args => (some arg, args)
+/-- Constructs a long short option handler from a generic option handler. -/
+@[inline] public def LongShortOptHandler.ofOptHandler (handler : OptHandler m) : LongShortOptHandler m :=
+  handler
 
-/-- Take the head of the remaining argument list (or `default` if none). -/
-@[inline] public def takeArgD (default : String) : m String :=
-  modifyGet fun | [] => (default, []) | arg :: args => (arg, args)
+public instance : Coe (OptHandler m) (LongShortOptHandler m) := ⟨.ofOptHandler⟩
 
-/-- Take the remaining argument list, leaving only an empty list. -/
-@[inline] public def takeArgs : m (List String) :=
-  modifyGet fun args => (args, [])
+/-- Handlers for each kind of option. -/
+public structure OptHandlers (m : Type → Type v) where
+  /-- Process a long option (e.g., {lit}`--long` or {lit}`"--long foo bar"`). -/
+  long : LongOptHandler m
+  /-- Process a short option (e.g., {lit}`-x` or {lit}`--`). -/
+  short : ShortOptHandler m
+  /-- Process a long short option (e.g., {lit}`-long`, {lit}`-xarg`, or {lit}`-xyz`). -/
+  longShort : LongShortOptHandler m
 
-/-- Add a string to the head of the remaining argument list. -/
-@[inline] public def consArg (arg : String) : m PUnit :=
-  modify fun args => arg :: args
+/-! ## Option Handlers -/
 
-/-- Process a short option of the form `-x=arg`. -/
-@[inline] public def shortOptionWithEq (handle : Char → m α) (opt : String) : m α := do
-  consArg (opt.drop 3).copy; handle (String.Pos.Raw.get opt ⟨1⟩)
+/--
+Process a short option of the form {lit}`-xarg`.
 
-/-- Process a short option of the form `"-x arg"`. -/
-@[inline] public def shortOptionWithSpace (handle : Char → m α) (opt : String) : m α := do
-  consArg <| opt.drop 2 |>.trimAsciiStart |>.copy; handle (String.Pos.Raw.get opt ⟨1⟩)
+Can be used as the handler for {lean}`OptHandlers.longShort`.
+-/
+@[inline] public def shortOptionWithArg (handler : ShortOptHandler m) : OptHandler m := fun _ h =>
+  handler h.shortChar h.shortOpt (some h.shortTail)
 
-/-- Process a short option of the form `-xarg`. -/
-@[inline] public def shortOptionWithArg (handle : Char → m α) (opt : String) : m α := do
-  consArg (opt.drop 2).copy; handle (String.Pos.Raw.get opt ⟨1⟩)
+/--
+Process a multiple short options grouped together
+(e.g., {lit}`-xyz` as {lit}`x`, {lit}`y`, {lit}`z`).
 
-/-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/
-@[inline] public def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
-  let rec loop (p : String.Pos.Raw) := do
-    if h : p.atEnd opt then
-      return
+Can be used as the handler for {lean}`OptHandlers.longShort`.
+-/
+@[inline] public def multiShortOption
+  [SeqRight m] (handler : ShortOptHandler m)
+: OptHandler m := fun arg h args =>
+  let rec @[specialize handler] loop (p : arg.Pos) (h : ¬ p.IsAtEnd) :=
+    let p' := p.next h
+    let optChar := p.get h
+    let r := handler optChar s!"-{optChar}" none args
+    if h' : p'.IsAtEnd then
+      r
     else
-      handle (p.get' opt h)
-      loop (p.next' opt h)
-  termination_by opt.utf8ByteSize - p.byteIdx
-  decreasing_by
-    simp [String.Pos.Raw.atEnd] at h
-    apply Nat.sub_lt_sub_left h
-    exact String.Pos.Raw.byteIdx_lt_byteIdx_next opt p
-  loop ⟨1⟩
-
-/-- Splits a long option of the form `"--long foo bar"` into `--long` and `"foo bar"`. -/
-@[inline] public def longOptionOrSpace (handle : String → m α) (opt : String) : m α :=
-  let pos := opt.find ' '
-  if h : pos = opt.endPos then
-    handle opt
-  else do
-    consArg <| opt.extract (pos.next h) opt.endPos
-    handle <| opt.extract opt.startPos pos
-
-/-- Splits a long option of the form `--long=arg` into `--long` and `arg`. -/
-@[inline] public def longOptionOrEq (handle : String → m α) (opt : String) : m α :=
-  let pos := opt.find '='
-  if h : pos = opt.endPos then
-    handle opt
-  else do
-    consArg <| opt.extract (pos.next h) opt.endPos
-    handle <| opt.extract opt.startPos pos
-
-/-- Process a long option  of the form `--long`, `--long=arg`, `"--long arg"`. -/
-@[inline] public def longOption (handle : String → m α) : String → m α :=
-  longOptionOrEq <| longOptionOrSpace handle
-
-/-- Process a short option of the form `-x`, `-x=arg`, `-x arg`, or `-long`. -/
-@[inline] public def shortOption
-  (shortHandle : Char → m α) (longHandle : String → m α)
-  (opt : String)
-: m α :=
-  if opt.length == 2 then -- `-x`
-    shortHandle (String.Pos.Raw.get opt ⟨1⟩)
+      r *> loop p' h'
+  termination_by p
+  loop h.shortPos h.shortPos_ne_endPos
+
+@[inline] private def splitLongOption
+  {arg : String} (sepPos : arg.Pos) (args : List String)
+  (longHandler : LongOptHandler m)
+  (noSepHandler : ArgHandler m)
+: m {remArgs : List String // sizeOf remArgs ≤ sizeOf args} :=
+  if h : sepPos = arg.endPos then
+    noSepHandler arg args
+  else
+    let optArg := arg.sliceFrom (sepPos.next h)
+    let opt := arg.sliceTo sepPos
+    longHandler opt (some optArg) args
+
+/--
+Processes a command line argument as a long option with possible option argument after a ` `
+(e.g., {lit}`-long`, {lit}`--long`, or {lit}`"--long arg"`).
+
+
+Parses a command line argument of the form {lit}`"-opt foo bar"` into the long option
+{lit}`-opt` with the option argument {lit}`"foo bar"` and processes it with {lean}`handler`.
+
+If a space is present (e.g., {lit}`-opt foo  bar`), the argument will be split around it.
+{lean}`handler` will be invoked with the option {lit}`-opt` and the option argument {lit}`opt`.
+Otherwise, the argument is passed to {lean}`handler` as an option with no option argument.
+
+Can be used as the handler for {lean}`OptHandlers.longShort`.
+-/
+@[inline] public def longOptionOrSpace (handler : LongOptHandler m) : OptHandler m := fun arg _ args =>
+  splitLongOption (arg.find ' ') args handler fun arg => handler arg.toSlice none
+
+/--
+Processes a command line argument as a long option with possible option argument after an `=`
+(e.g., {lit}`-long`, {lit}`-long`, or {lit}`--long=arg`).
+
+If an equal sign is present (e.g., {lit}`-opt=foo bar`), the argument will be split around it.
+{lean}`handler` will be invoked with the option {lit}`-opt` and the option argument {lit}`foo bar`.
+Otherwise, the argument is passed to {lean}`handler` as an option with no option argument.
+
+Can be used as the handler for {lean}`OptHandlers.longShort`.
+-/
+@[inline] public def longOptionOrEq (handler : LongOptHandler m) : OptHandler m := fun arg _ args =>
+  splitLongOption (arg.find '=') args handler fun arg => handler arg.toSlice none
+
+/--
+Processes a command line argument as a long option with a possible option argument
+(e.g., {lit}`-long`, {lit}`--long`, {lit}`--long=arg`, or {lit}`"--long arg"`).
+
+Can be used as the handler for {lean}`OptHandlers.longShort`.
+-/
+@[inline] def longOption (handler : LongOptHandler m) : OptHandler m := fun arg _ args =>
+  splitLongOption (arg.find ' ') args handler fun arg args =>
+    splitLongOption (arg.find '=') args handler fun arg =>
+      handler arg.toSlice none
+
+/-- Processes a short option of the form {lit}`-x`, {lit}`-x=arg`, {lit}`-x arg`, or {lit}`-long`. -/
+@[inline] def shortOption
+  (shortHandler : ShortOptHandler m) (longHandler : LongShortOptHandler m)
+: OptHandler m := fun arg h =>
+  if h' : h.afterShortPos.IsAtEnd then -- `-x`
+    shortHandler h.shortChar h.shortOpt none
   else -- `-c(.+)`
-    match String.Pos.Raw.get opt ⟨2⟩ with
+    let c := h.afterShortPos.get h'
+    let nextPos := h.afterShortPos.next h'
+    match c with
     | '=' => -- `-x=arg`
-      shortOptionWithEq shortHandle opt
+      shortHandler h.shortChar h.shortOpt (some <| arg.sliceFrom nextPos)
     | ' ' => -- `"-x arg"`
-      shortOptionWithSpace shortHandle opt
+      shortHandler h.shortChar h.shortOpt (some <| arg.sliceFrom nextPos |>.trimAsciiStart)
     | _   => -- `-long`
-      longHandle opt
+      longHandler arg h
 
 /--
-Process an option, short or long, using the given handlers.
-An option is an argument of length > 1 starting with a dash (`-`).
+Processes an option, short or long, using the given handlers.
+An option is an argument of length > 1 starting with a dash ({lit}`-`).
 An option may consume additional elements of the argument list.
 -/
-@[inline] public def option (handlers : OptionHandlers m α) (opt : String) : m α :=
-  if String.Pos.Raw.get opt ⟨1⟩ == '-' then -- `--(.*)`
-    longOption handlers.long opt
+@[inline] public def option (handlers : OptHandlers m) : OptHandler m := fun arg h =>
+  if h.shortChar = '-' then -- `--(.*)`
+    longOption handlers.long arg h
   else
-    shortOption handlers.short handlers.longShort opt
+    shortOption handlers.short handlers.longShort arg h
+
+/-! ## Argument Processors -/
 
-/-- Process the head argument of the list using `handle` if it is an option. -/
-public def processLeadingOption (handle : String → m PUnit) : m PUnit := do
-  match (← getArgs) with
-  | [] => pure ()
-  | arg :: args =>
-    if arg.length > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
-      setArgs args
-      handle arg
+/-- Process the head argument of the list using {lean}`handler` if it is an option. -/
+@[inline] public def processLeadingOption
+  [Monad m] (args : List String) (handler : OptHandler m)
+: m (List String) :=
+  if let arg :: remArgs := args then
+    if h : IsOpt arg then -- `-(.+)`
+      handler arg h remArgs
+    else
+      pure args
+  else
+    pure args
 
 /--
 Process the leading options of the remaining argument list.
 Consumes empty leading arguments in the argument list.
 -/
-public partial def processLeadingOptions (handle : String → m PUnit) : m PUnit := do
-  if let arg :: args ← getArgs then
-    let len := arg.length
-    if len > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
-      setArgs args
-      handle arg
-      processLeadingOptions handle
-    else if len == 0 then -- skip empty leading args
-      setArgs args
-      processLeadingOptions handle
-
-/-- Process every option and collect the remaining arguments into an `Array`. -/
-public partial def collectArgs
-  (option : String → m PUnit) (args : Array String := #[])
-: m (Array String) := do
-  if let some arg ← takeArg? then
-    let len := arg.length
-    if len > 1 && String.Pos.Raw.get arg 0 == '-' then -- `-(.+)`
-      option arg
-      collectArgs option args
-    else if len == 0 then -- skip empty args
-      collectArgs option args
+@[specialize handler]
+public def processLeadingOptions
+  [Monad m] (args : List String) (handler : OptHandler m)
+: m (List String) := do
+  if let a :: as := args then
+    if h0 : a.startPos.IsAtEnd then -- skip empty leading args
+      processLeadingOptions as handler
+    else if h : a.startPos.get h0 = '-' ∧ ¬ (a.startPos.next h0).IsAtEnd then -- `-(.+)`
+      let ⟨as, _⟩ ← handler a ⟨h0, h.1, h.2⟩ as
+      processLeadingOptions as handler
     else
-      collectArgs option (args.push arg)
+      return args
   else
-    pure args
+    return args
+termination_by args
+
+@[simp] public theorem processLeadingOptions_nil [Monad m] :
+  processLeadingOptions (m := m) [] f = pure []
+:= by unfold processLeadingOptions; simp
+
+@[simp] public theorem processLeadingOptions_cons_empty [Monad m] :
+  processLeadingOptions (m := m) ("" :: as) f = processLeadingOptions as f
+:= by conv => {lhs; unfold processLeadingOptions}; simp
+
+public theorem processLeadingOptions_cons_of_isOpt [Monad m] (h : IsOpt a) :
+  processLeadingOptions (m := m) (a :: as) f =
+    f a h as >>= fun as => processLeadingOptions as f
+:= by
+  conv => lhs; unfold processLeadingOptions
+  simp [h.ne_empty, h.get_startPos, h.next_startPos_ne_endPos]
+
+public theorem processLeadingOptions_cons_of_isArg [Monad m] (h : IsArg a) :
+  processLeadingOptions (m := m) (a :: as) f = pure (a :: as)
+:= by
+  conv => lhs; unfold processLeadingOptions
+  simp [h.ne_empty, h.startPos_wf]
+
+/-- Process every argument in the command line argument list. -/
+@[inline] public def processArgs
+  [Monad m] (args : List String) (optHandler : OptHandler m) (argHandler : ArgHandler m)
+: m PUnit :=
+  let rec @[specialize optHandler argHandler] loop args := do
+    if let a :: as := args then
+      if h0 : a.startPos.IsAtEnd then -- skip empty args
+        loop as
+      else if h : a.startPos.get h0 = '-' ∧ ¬ (a.startPos.next h0).IsAtEnd then -- `-(.+)`
+        let ⟨as, _⟩ ← optHandler a ⟨h0, h.1, h.2⟩ as
+        loop as
+      else
+        let ⟨as, _⟩ ← argHandler a as
+        loop as
+  termination_by args
+  loop args
+
+@[simp] public theorem processArgs_nil [Monad m] :
+  processArgs (m := m) [] optH argH = pure ()
+:= by unfold processArgs processArgs.loop; simp
+
+@[simp] public theorem processArgs_cons_empty [Monad m] :
+  processArgs (m := m) ("" :: as) optH argH = processArgs as optH argH
+:= by
+  unfold processArgs
+  conv => lhs; unfold processArgs.loop
+  simp
+
+public theorem processArgs_cons_of_isOpt [Monad m] (h : IsOpt a) :
+  processArgs (m := m) (a :: as) optH argH =
+    optH a h as >>= fun as => processArgs as optH argH
+:= by
+  unfold processArgs
+  conv => lhs; unfold processArgs.loop
+  simp [h.ne_empty, h.get_startPos, h.next_startPos_ne_endPos]
+
+public theorem processArgs_cons_of_isArg [Monad m] (h : IsArg a) :
+  processArgs (m := m) (a :: as) optH argH =
+    argH a as >>= fun as => processArgs as optH argH
+:= by
+  unfold processArgs
+  conv => lhs; unfold processArgs.loop
+  simp [h.ne_empty, h.startPos_wf]
+
+@[inline] def OptHandler.lift [MonadLift m n] (self : OptHandler m) : OptHandler n :=
+  fun arg h args => liftM (self arg h args)
 
-/-- Process every option in the argument list. -/
-@[inline] public def processOptions (handle : String → m PUnit) : m PUnit := do
-  setArgs (← collectArgs handle).toList
+/-- Process every option in {lean}`args` and collect the remaining arguments into an {name}`Array`. -/
+@[inline] public def collectArgs
+  [Monad m] (args : List String) (handler : OptHandler m)
+: m (Array String) :=
+  (·.2) <$> StateT.run (s := #[]) do
+    processArgs args handler.lift fun arg args s =>
+      pure (⟨args, Nat.le_refl ..⟩, s.push arg)
diff --git a/src/lake/Lake/Util/Date.lean b/src/lake/Lake/Util/Date.lean
index 0b811c1d3e01..a87478c40cb4 100644
--- a/src/lake/Lake/Util/Date.lean
+++ b/src/lake/Lake/Util/Date.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.Ord.Basic
+public import Init.Data.String.Defs
 import Lake.Util.String
 import Init.Data.String.Search
 
@@ -54,10 +55,9 @@ public def ofValid? (year month day : Nat) : Option Date := do
   guard (IsValidMonth month ∧ IsValidDay year month day)
   return {year, month, day}
 
-public def ofString? (t : String) : Option Date := do
-  match t.split '-' |>.toList with
-  | [y,m,d] =>
-    ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?)
+public def ofString? (s : String.Slice) : Option Date := do
+  match s.split '-' |>.toList with
+  | [y,m,d] => ofValid? (← y.toNat?) (← m.toNat?) (← d.toNat?)
   | _ => none
 
 public protected def toString (d : Date) : String :=
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index 257b81dc7281..7911d90af3a0 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -6,6 +6,7 @@ Authors: Mac Malone
 module
 
 prelude
+public import Lean.Data.Trie
 public import Lean.Data.Json
 public import Lake.Util.Error
 public import Lake.Util.EStateT
@@ -96,13 +97,18 @@ public def LogLevel.ansiColor : LogLevel → String
 | .warning => "33"
 | .error => "31"
 
-public def LogLevel.ofString? (s : String) : Option LogLevel :=
-  match s.toLower with
-  | "trace" => some .trace
-  | "info" | "information" => some .info
-  | "warn" | "warning" => some .warning
-  | "error" => some .error
-  | _ => none
+@[inline] public def LogLevel.ofString? (s : String.Slice) : Option LogLevel :=
+  trie.matchPrefix s.str s.startInclusive.offset s.endExclusive.offset.byteIdx <|
+    String.byteIdx_rawEndPos ▸ String.Pos.Raw.le_iff.mp s.endExclusive.isValid.le_rawEndPos
+where trie :=
+  let add sym lv t := t.insert sym lv
+  (∅ : Lean.Data.Trie LogLevel)
+  |> add "trace"        .trace
+  |> add "info"         .info
+  |> add "information"  .info
+  |> add "warn"         .warning
+  |> add "warning"      .warning
+  |> add "error"        .error
 
 public protected def LogLevel.toString : LogLevel → String
 | .trace => "trace"
diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean
index f298f7dcd677..ebae1108634e 100644
--- a/src/lake/Lake/Util/MainM.lean
+++ b/src/lake/Lake/Util/MainM.lean
@@ -8,6 +8,7 @@ module
 prelude
 public import Lake.Util.Log
 public import Lake.Util.Exit
+import all Init.System.ST
 
 namespace Lake
 
@@ -21,6 +22,12 @@ public instance : Monad MainM := inferInstanceAs (Monad (EIO ExitCode))
 public instance : MonadFinally MainM := inferInstanceAs (MonadFinally (EIO ExitCode))
 public instance : MonadLift BaseIO MainM := inferInstanceAs (MonadLift BaseIO (EIO ExitCode))
 
+/- Adaption of `LawfulMonad` for `EST` from batteries. -/
+public instance : LawfulMonad MainM := .mk' _
+  (id_map := fun x => funext fun v => by dsimp [Functor.map, EST.bind]; cases x v <;> rfl)
+  (pure_bind := fun x f => rfl)
+  (bind_assoc := fun f g x => funext fun v => by dsimp [Bind.bind, EST.bind]; cases f v <;> rfl)
+
 namespace MainM
 
 /-! # Basics -/
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index 4e1e52a18d03..bdca29a6242c 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@@ -22,32 +22,41 @@ open System Lean
 
 namespace Lake
 
+private theorem le_next_of_le
+  {s : String.Slice} {iniPos p : s.Pos} {h} (iniPos_le : iniPos ≤ p)
+: iniPos ≤ p.next h :=
+  have le_of_lt {a b : s.Pos} : a < b → a ≤ b := by
+    simpa [String.Slice.Pos.le_iff, String.Slice.Pos.lt_iff] using String.Pos.Raw.le_of_lt
+  have le_trans {a b c : s.Pos} : a ≤ b → b ≤ c → a ≤ c := by
+    simpa [String.Slice.Pos.le_iff] using String.Pos.Raw.le_trans
+  le_trans iniPos_le (le_of_lt p.lt_next)
+
 /-! ## Parser Utils -/
 
+abbrev ParseM (s : String.Slice) (α) :=
+   EStateM String s.Pos α
+
 /--
 Parses version components separated by a `.` from the head of the string.
 
 Components are composed of alphanumerics or a `*`.
 -/
-@[inline] def parseVerComponents
-  (s : String)
-: EStateM String s.Pos (Array String.Slice) :=
-  fun p => go #[] p p (String.Pos.le_refl _)
+@[inline] def parseVerComponents (s : String.Slice) : ParseM s (Array String.Slice) :=
+  fun p => go #[] p p p.le_refl
 where
   go cs iniPos p (iniPos_le : iniPos ≤ p) :=
-    if h : p = s.endPos then
-      let c := String.Slice.mk s iniPos p iniPos_le
+    if h : p.IsAtEnd then
+      let c := s.slice iniPos p iniPos_le
       .ok (cs.push c) p
     else
       let c := p.get h
       if c == '.' then
-        let c := String.Slice.mk s iniPos p iniPos_le
+        let c := s.slice iniPos p iniPos_le
         go (cs.push c) (p.next h) (p.next h) (Nat.le_refl _)
       else if c.isAlphanum || c == '*' then
-        go cs iniPos (p.next h)
-          (String.Pos.le_trans iniPos_le (String.Pos.le_of_lt p.lt_next))
+        go cs iniPos (p.next h) (le_next_of_le iniPos_le)
       else
-        let c := String.Slice.mk s iniPos p iniPos_le
+        let c := s.slice iniPos p iniPos_le
         .ok (cs.push c) p
   termination_by p
 
@@ -78,47 +87,46 @@ private def parseVerComponent {σ} (what : String) (s? : Option String.Slice) :
       | throw s!"invalid {what} version: expected numeral or wildcard, got '{s.copy}'"
     return .nat n
 
-def parseSpecialDescr? (s : String) : EStateM String s.Pos (Option String) := do
+def parseSpecialDescr? (s : String.Slice) : ParseM s (Option String.Slice) := do
   let p ← get
-  if h : p = s.endPos then
+  if h : p.IsAtEnd then
     return none
   else
     let c := p.get h
     if c == '-' then
       let p := p.next h
-      let p' := nextUntilWhitespace p
+      let ⟨p', h⟩ := nextUntilWhitespace p p p.le_refl
       set p'
-      let specialDescr := s.extract p p'
+      let specialDescr := s.slice p p' h
       return some specialDescr
     else
       return none
 where
-  nextUntilWhitespace p :=
-    if h : p = s.endPos then
-      p
+  nextUntilWhitespace p iniPos (iniPos_le : iniPos ≤ p) :=
+    if h : p.IsAtEnd then
+      Subtype.mk p iniPos_le
     else if (p.get h).isWhitespace then
-      p
+      Subtype.mk p iniPos_le
     else
-      nextUntilWhitespace (p.next h)
+      nextUntilWhitespace (p.next h) iniPos (le_next_of_le iniPos_le)
   termination_by p
 
-private def parseSpecialDescr (s : String) : EStateM String s.Pos String := do
+private def parseSpecialDescr (s : String.Slice) : ParseM s String := do
   let some specialDescr ← parseSpecialDescr? s
     | return ""
   if specialDescr.isEmpty then
     throw "invalid version: '-' suffix cannot be empty"
-  return specialDescr
+  return specialDescr.copy
 
 private def runVerParse
-  (s : String) (x : (s : String) → EStateM String s.Pos α)
-  (startPos := s.startPos) (endPos := s.endPos)
+  (s : String.Slice) (x : (s : String.Slice) → ParseM s α)
 : Except String α :=
-  match x s startPos with
+  match x s s.startPos with
   | .ok v p =>
-    if p = endPos then
+    if p.IsAtEnd then
       return v
     else
-      let tail := p.offset.extract s endPos.offset
+      let tail := s.sliceFrom p
       throw s!"unexpected characters at end of version: {tail}"
   | .error e _ => throw e
 
@@ -138,7 +146,7 @@ public instance : LE SemVerCore := leOfOrd
 public instance : Min SemVerCore := minOfLe
 public instance : Max SemVerCore := maxOfLe
 
-def parseM (s : String) : EStateM String s.Pos SemVerCore := do
+def parseM (s : String.Slice) : ParseM s SemVerCore := do
   try
     let cs ← parseVerComponents s
     if h : cs.size = 3 then
@@ -202,12 +210,12 @@ public instance : LE StdVer := leOfOrd
 public instance : Min StdVer := minOfLe
 public instance : Max StdVer := maxOfLe
 
-public def parseM (s : String) : EStateM String s.Pos StdVer := do
+def parseM (s : String.Slice) : ParseM s StdVer := do
   let core ← SemVerCore.parseM s
   let specialDescr ← parseSpecialDescr s
   return {toSemVerCore := core, specialDescr}
 
-@[inline] public def parse (s : String) : Except String StdVer := do
+@[inline] public def parse (s : String.Slice) : Except String StdVer := do
   runVerParse s parseM
 
 public protected def toString (ver : StdVer) : String :=
@@ -218,7 +226,7 @@ public protected def toString (ver : StdVer) : String :=
 
 public instance : ToString StdVer := ⟨StdVer.toString⟩
 public instance : ToJson StdVer := ⟨(·.toString)⟩
-public instance : FromJson StdVer := ⟨(do StdVer.parse <| ← fromJson? ·)⟩
+public instance : FromJson StdVer := ⟨(StdVer.parse =<< String.toSlice <$> fromJson? ·)⟩
 
 end StdVer
 
@@ -251,21 +259,20 @@ namespace ToolchainVer
 
 public instance : Coe LeanVer ToolchainVer := ⟨ToolchainVer.release⟩
 
-public def ofString (ver : String) : ToolchainVer := Id.run do
+public def ofString (ver : String.Slice) : ToolchainVer := Id.run do
   let colonPos := ver.find ':'
   let (origin, tag) :=
     if h : ¬colonPos.IsAtEnd then
-      let pos := colonPos.next h
-      (ver.extract ver.startPos colonPos, ver.extract pos ver.endPos)
+      (ver.sliceTo colonPos, ver.sliceFrom <| colonPos.next h)
     else
       ("", ver)
   let noOrigin := origin.isEmpty
-  if tag.startsWith "v" then
-    if let .ok ver := StdVer.parse (tag.drop 1).copy then
-      if noOrigin|| origin == defaultOrigin then
+  if let some ver := tag.dropPrefix? "v" then
+    if let .ok ver := StdVer.parse ver then
+      if noOrigin || origin == defaultOrigin then
         return .release ver
   else if let some date := tag.dropPrefix? "nightly-" then
-    if let some date := Date.ofString? date.toString then
+    if let some date := Date.ofString? date then
       if noOrigin then
         return .nightly date
       else if let some suffix := origin.dropPrefix? defaultOrigin then
@@ -278,7 +285,7 @@ public def ofString (ver : String) : ToolchainVer := Id.run do
   else if let .ok ver := StdVer.parse ver then
     if noOrigin || origin == defaultOrigin then
       return .release ver
-  return .other ver
+  return .other ver.copy
 
 /-- Parse a toolchain from a `lean-toolchain` file. -/
 public def ofFile? (toolchainFile : FilePath) : IO (Option ToolchainVer) := do
@@ -296,7 +303,7 @@ public def ofFile? (toolchainFile : FilePath) : IO (Option ToolchainVer) := do
 
 public instance : ToString ToolchainVer := ⟨ToolchainVer.toString⟩
 public instance : ToJson ToolchainVer := ⟨(·.toString)⟩
-public instance : FromJson ToolchainVer := ⟨(ToolchainVer.ofString <$> fromJson? ·)⟩
+public instance : FromJson ToolchainVer := ⟨(ToolchainVer.ofString <$> String.toSlice <$> fromJson? ·)⟩
 
 public def blt (a b : ToolchainVer) : Bool :=
   match a, b with
@@ -323,7 +330,7 @@ public instance decLe (a b : ToolchainVer) : Decidable (a ≤ b) :=
 end ToolchainVer
 
 /-- Converts a toolchain version to its normal form (e.g., with an origin). -/
-public def normalizeToolchain (s : String) : String :=
+public def normalizeToolchain (s : String.Slice) : String :=
   ToolchainVer.ofString s |>.toString
 
 /-! ## DecodeVersion -/
@@ -335,7 +342,7 @@ public class DecodeVersion (α : Type u) where
 export DecodeVersion (decodeVersion)
 
 public instance : DecodeVersion SemVerCore := ⟨SemVerCore.parse⟩
-@[default_instance] public instance : DecodeVersion StdVer := ⟨StdVer.parse⟩
+@[default_instance] public instance : DecodeVersion StdVer := ⟨(StdVer.parse ·)⟩
 public instance : DecodeVersion ToolchainVer := ⟨(pure <| ToolchainVer.ofString ·)⟩
 
 /-! ## VerRange -/
@@ -346,17 +353,19 @@ deriving Repr, Inhabited
 
 namespace ComparatorOp
 
-def parseM
-  (s : String)
-: EStateM String s.Pos ComparatorOp := fun p =>
-  if let some (tk, op) := trie.matchPrefix s p.offset then
+def parseM (s : String.Slice) : ParseM s ComparatorOp := do
+  let p ← get
+  let r? := trie.matchPrefix s.str p.offset s.endExclusive.offset.byteIdx <|
+    String.byteIdx_rawEndPos ▸ String.Pos.Raw.le_iff.mp s.endExclusive.isValid.le_rawEndPos
+  if let some (tk, op) := r? then
     let p' := p.offset + tk
-    if h : p'.IsValid s then
-      .ok op (.mk p' h)
+    if h : p'.IsValidForSlice s then
+      set (s.pos p' h)
+      return op
     else
-      .error "(internal) comparison operator parse produced invalid position" p
+      throw "(internal) comparison operator parse produced invalid position"
   else
-    .error "expected comparison operator" p
+    throw "expected comparison operator"
 where trie :=
   let add sym cmp t := t.insert sym (sym, cmp)
   (∅ : Lean.Data.Trie (String × ComparatorOp))
@@ -370,9 +379,9 @@ where trie :=
   |> add "!=" .ne
   |> add "≠"  .ne
 
-public def ofString? (s : String) : Option ComparatorOp :=
+public def ofString? (s : String.Slice) : Option ComparatorOp :=
   match parseM s s.startPos with
-  | .ok op p => if p = s.endPos then some op else none
+  | .ok op p => if p.IsAtEnd then some op else none
   | .error .. => none
 
 public protected def toString (self : ComparatorOp) : String :=
@@ -403,14 +412,14 @@ public def wild : VerComparator :=
 
 public instance : Inhabited VerComparator := ⟨.wild⟩
 
-def parseM (s : String) : EStateM String s.Pos VerComparator := do
+def parseM (s : String.Slice) : ParseM s VerComparator := do
   let op ← ComparatorOp.parseM s
   let core ← SemVerCore.parseM s
   if let some specialDescr ← parseSpecialDescr? s then
-    if  specialDescr.isEmpty then
+    if specialDescr.isEmpty then
       return {ver := .ofSemVerCore core, op, includeSuffixes := true}
     else
-      return {ver := .mk core specialDescr, op}
+      return {ver := .mk core specialDescr.copy, op}
   else
     return {ver := .ofSemVerCore core, op}
 
@@ -480,65 +489,62 @@ where
       ands.foldl (init := ands[0].toString) (start := 1) fun s v =>
         s!"{s}, {v}"
 
-partial def parseM (s : String) : EStateM String s.Pos VerRange := do
-  let clauses ← go true #[] #[]
-  return {toString := s, clauses}
+partial def parseM (s : String.Slice) : ParseM s (Array (Array VerComparator)) := do
+  go true #[] #[]
 where
-  go needsRange ors (ands : Array VerComparator) p :=
-    if h : p = s.endPos then
+  go needsRange ors (ands : Array VerComparator) := do
+    let p ← get
+    if h : p.IsAtEnd then
       if needsRange || ands.size == 0 then
-        .error "expected version range" p
+        throw "expected version range"
       else
-        .ok (ors.push ands) p
+        return ors.push ands
     else
       let c := p.get h
       if c.isAlphanum || c == '*' then
-        match parseWild s ands p with
-        | .ok ands p =>
-          go false ors ands p
-        | .error e p => .error e p
+        let cs ← parseVerComponents s
+        if (← get).get?.any (· == '-') then
+          throw s!"invalid wildcard range: wildcard versions do not support suffixes"
+        let ands ← parseWildComponents cs ands
+        go false ors ands
       else if c == '^' then
-        match parseCaret s ands (p.next h) with
-        | .ok ands p =>
-          go false ors ands p
-        | .error e p => .error e p
+        set (p.next h)
+        let ands ← parseCaret s ands
+        go false ors ands
       else if c == '~' then
-        match parseTilde s ands (p.next h) with
-        | .ok ands p =>
-          go false ors ands p
-        | .error e p => .error e p
+        set (p.next h)
+        let ands ← parseTilde s ands
+        go false ors ands
       else if c.isWhitespace then
-        go needsRange ors ands (p.next h)
+        set (p.next h)
+        go needsRange ors ands
       else if c == ',' then
         if needsRange then
-          .error "expected version range" p
+          throw "expected version range"
         else
-          go true ors ands (p.next h)
+          set (p.next h)
+          go true ors ands
       else if c == '|' then
-        let p := p.next h
-        if h : p = s.endPos then
-          .error "expected '|' after first '|'" p
-        else if p.get h = '|' then
+        let p' := p.next h; set p'
+        if h : p'.IsAtEnd then
+          throw "expected '|' after first '|'"
+        else if p'.get h = '|' then
           if ands.size = 0 then
-            .error "expected version range" p
+            throw "expected version range"
           else
-            go true (ors.push ands) #[] (p.next h)
+            set (p'.next h)
+            go true (ors.push ands) #[]
         else
-          .error "expected '|' after first '|'" p
+          throw "expected '|' after first '|'"
       else
-        match VerComparator.parseM s p with
-        | .ok cmp p =>
-          go false ors (ands.push cmp) p
-        | .error e p => .error e p
+        let cmp ← VerComparator.parseM s
+        go false ors (ands.push cmp)
   @[inline] appendRange ands minVer maxVer (specialDescr := "") :=
     let minVer := StdVer.mk minVer specialDescr
     let maxVer := StdVer.ofSemVerCore maxVer
     ands.push {op := .ge, ver := minVer} |>.push {op := .lt, ver := maxVer, includeSuffixes := true}
-  parseWild (s : String) ands : EStateM String s.Pos _ := do
-    let cs ← parseVerComponents s
-    if (← get).get?.any (· == '-') then
-      throw s!"invalid wildcard range: wildcard versions do not support suffixes"
-    else if cs.size = 0 ∨ cs.size > 3 then
+  parseWildComponents {σ} (cs : Array String.Slice) ands : EStateM String σ  _ := do
+    if cs.size = 0 ∨ cs.size > 3 then
       throw s!"invalid wildcard range: incorrect number of components: got {cs.size}, expected 1-3"
     else
       let major? ← parseVerComponent "major" cs[0]?
@@ -559,7 +565,7 @@ where
           otherwise, use '≥' to support it and future versions"
       | _, _, _ =>
         return ands.push .wild
-  parseCaret (s : String) ands : EStateM String s.Pos _ := do
+  parseCaret (s : String.Slice) ands : ParseM s _ := do
     let cs ← parseVerComponents s
     let specialDescr ← parseSpecialDescr s
     if h : cs.size = 1 then
@@ -588,7 +594,7 @@ where
         return appendRange ands {major, minor, patch}  {major := major + 1} specialDescr
     else
       throw s!"invalid caret range: incorrect number of components: got {cs.size}, expected 1-3"
-  parseTilde (s : String) ands : EStateM String s.Pos _ := do
+  parseTilde (s : String.Slice) ands : ParseM s _ := do
     let cs ← parseVerComponents s
     let specialDescr ← parseSpecialDescr s
     if h : cs.size = 1 then
@@ -607,7 +613,8 @@ where
       throw s!"invalid tilde range: incorrect number of components: got {cs.size}, expected 1-3"
 
 @[inline] public def parse (s : String) : Except String VerRange := do
-  runVerParse s parseM
+  let clauses ← runVerParse s parseM
+  return {toString := s, clauses}
 
 public def test (self : VerRange) (ver : StdVer) : Bool :=
   self.clauses.any (·.all (·.test ver))
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index c94b666025c9..9896cbacd494 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -221,7 +221,7 @@ ENDFOREACH(T)
 # toolchain: requires elan to download toolchain
 # online: downloads remote repositories
 file(GLOB_RECURSE LEANLAKETESTS
-  #"${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh"
+  "${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh"
   "${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
   if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")
diff --git a/tests/lake/tests/api/vers.lean b/tests/lake/tests/api/vers.lean
index cc0f8c50a268..a38a34d8ead8 100644
--- a/tests/lake/tests/api/vers.lean
+++ b/tests/lake/tests/api/vers.lean
@@ -14,11 +14,11 @@ def checkParse (ver expected : String) : IO Unit :=  do
 
 def checkMatch (range : String) (accepts rejects : Array String) : IO Unit :=  do
   let range ← IO.ofExcept <| VerRange.parse range
-  accepts.forM fun s => do
+  for s in accepts do
     let ver ← IO.ofExcept <| StdVer.parse s
     unless range.test ver do
       throw <| IO.userError s!"invalid reject: expected\n  '{range}'\nto accept\n  '{s}'"
-  rejects.forM fun s => do
+  for s in rejects do
     let ver ← IO.ofExcept <| StdVer.parse s
     if range.test ver then
       throw <| IO.userError s!"invalid accept: expected\n  '{range}'\nto reject\n  '{s}'"
diff --git a/tests/lake/tests/logLevel/lakefile.lean b/tests/lake/tests/logLevel/lakefile.lean
index 12dea7a38057..cc37718edfe5 100644
--- a/tests/lake/tests/logLevel/lakefile.lean
+++ b/tests/lake/tests/logLevel/lakefile.lean
@@ -7,7 +7,7 @@ package test
 Test logging in Lake CLI
 -/
 
-def cfgLogLv? := (get_config? log).bind LogLevel.ofString?
+def cfgLogLv? := (get_config? log).bind (LogLevel.ofString? ·)
 
 meta if cfgLogLv?.isSome then
   run_cmd Lean.log "bar" cfgLogLv?.get!.toMessageSeverity