diff --git a/Lake/Cli.lean b/Lake/Cli.lean index 73aae003eb..e90faf3337 100644 --- a/Lake/Cli.lean +++ b/Lake/Cli.lean @@ -41,13 +41,13 @@ structure CliState where abbrev CliM := CliT <| StateT CliState <| EIO UInt32 -namespace CliM +namespace Cli open CliT -- ## Basic Actions -/-- Perform an IO action and silently exit with code 1 if it errors. -/ -def runIO' (x : IO α) (rc : UInt32 := 1): CliM α := +/-- Perform an IO action and silently exit with the given code (default: 1) if it errors. -/ +def runIO' (x : IO α) (rc : UInt32 := 1) : CliM α := x.toEIO fun e => rc /-- Exit the CLI with given return code (i.e., throw it). -/ @@ -211,10 +211,13 @@ def verifyInstall : CliM PUnit := do output s!"Lake:\n{repr <| ← getLakeInstall?}" verifyLeanVersion +/-- Exit code to return if `print-paths` cannot find the config file. -/ +def noConfigFileCode : UInt32 := 2 + /-- Build a list of imports of the package and print the `.olean` and source directories of every used package. - If no configuration file exists, exit silently with code 2. + If no configuration file exists, exit silently with `noConfigFileCode` (i.e, 2). The `print-paths` command is used internally by Lean 4 server. -/ @@ -222,7 +225,7 @@ def printPaths (imports : List String := []) : CliM PUnit := do let erc := 2 let (leanInstall, lakeInstall) ← getInstall let configFile := (← getRootDir) / (← getConfigFile) - if (← runIO' configFile.pathExists erc) then + if (← runIO' configFile.pathExists noConfigFileCode) then let pkg ← loadPkg (← getSubArgs) runIO do let pkgs ← pkg.buildImportsAndDeps imports |>.runIn { @@ -237,7 +240,7 @@ def printPaths (imports : List String := []) : CliM PUnit := do ("srcPath", toJson <| List.toArray <| pkgs.map (·.srcDir.toString)) ] else - exit erc + exit noConfigFileCode def command : (cmd : String) → CliM PUnit | "new" => do noArgsRem <| runIO <| new (← takeArg) @@ -265,7 +268,10 @@ def processArgs : CliM PUnit := do else if (← getWantsHelp) then output usage else error "expected command" -def run (self : CliM α) (args : List String) : IO UInt32 := do +end Cli + +open Cli in +def CliM.run (self : CliM α) (args : List String) : IO UInt32 := do let (leanInstall?, lakeInstall?) ← findInstall? let initSt := {leanInstall?, lakeInstall?} let methods := { @@ -276,7 +282,5 @@ def run (self : CliM α) (args : List String) : IO UInt32 := do | Except.ok _ => pure 0 | Except.error rc => pure rc -end CliM - def cli (args : List String) : IO UInt32 := - CliM.processArgs.run args + Cli.processArgs.run args diff --git a/Lake/CliT.lean b/Lake/CliT.lean index f6a03aea25..058cfe4eb9 100644 --- a/Lake/CliT.lean +++ b/Lake/CliT.lean @@ -83,11 +83,11 @@ def consArg (arg : String) : CliT m PUnit := /-- Get the methods of this CLI. -/ def getMethods : CliT m (CliMethods m) := - read >>= (·.get) + (·.get) <$> read /-- Change the methods of this CLI. -/ -def adaptMethods (f : CliMethods m → CliMethods m) (x : CliT m α) : CliT m α := - ReaderT.adapt (fun ref => CliMethodsRef.mk <| f ref.get) x +def adaptMethods (f : CliMethods m → CliMethods m') (self : CliT m α) : CliT m α := + ReaderT.adapt (fun ref => CliMethodsRef.mk <| f ref.get) self /-- Process a short option (ex. `-x` or `--`). -/ def shortOption (opt : Char) : CliT m PUnit :=