Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Commit 76c30b7

Browse files
committed
fix: properly catch CLI errors
1 parent 0de8d7c commit 76c30b7

File tree

2 files changed

+7
-12
lines changed

2 files changed

+7
-12
lines changed

Diff for: Lake/CLI/Main.lean

+6-11
Original file line numberDiff line numberDiff line change
@@ -356,16 +356,11 @@ def processArgs : CliM PUnit := do
356356
end Cli
357357

358358
open Cli in
359-
def CliM.run (self : CliM α) (args : List String) : IO UInt32 := do
359+
def CliM.run (self : CliM α) (args : List String) : BaseIO UInt32 := do
360360
let (leanInstall?, lakeInstall?) ← findInstall?
361-
match (← self args |>.run' {leanInstall?, lakeInstall?} |>.toIO') with
362-
| Except.ok res =>
363-
match res with
364-
| Except.ok _ => return 0
365-
| Except.error err =>
366-
error err.toString
367-
return 1
368-
| Except.error rc => return rc
369-
370-
def cli (args : List String) : IO UInt32 :=
361+
let main := self args |>.run' {leanInstall?, lakeInstall?}
362+
let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
363+
main.run
364+
365+
def cli (args : List String) : BaseIO UInt32 :=
371366
Cli.processArgs.run args

Diff for: Lake/Util/MainM.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ namespace MainM
3232
@[inline] protected def toBaseIO (self : MainM α) : BaseIO (Except ExitCode α) :=
3333
self.toEIO.toBaseIO
3434

35-
protected def run (self : MainM PUnit) : BaseIO ExitCode :=
35+
protected def run (self : MainM α) : BaseIO ExitCode :=
3636
self.toBaseIO.map fun | Except.ok _ => 0 | Except.error rc => rc
3737

3838
-- # Exits

0 commit comments

Comments
 (0)