From 8c40a315732ff157f377d7abc2d6e3dffeb23d1a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Feb 2022 18:08:56 -0800
Subject: [PATCH] chore: auto pure was removed

---
 Lake/Build/Module.lean       |  2 +-
 Lake/Build/Monad.lean        |  2 +-
 Lake/Build/Recursive.lean    |  2 +-
 Lake/Build/Target.lean       | 14 +++++++-------
 Lake/Build/Trace.lean        | 18 +++++++++---------
 Lake/CLI/Build.lean          |  4 ++--
 Lake/CLI/Main.lean           | 12 ++++++------
 Lake/Config/Glob.lean        |  2 +-
 Lake/Config/InstallPath.lean | 16 ++++++++--------
 Lake/Config/Load.lean        |  2 +-
 Lake/Config/Resolve.lean     |  6 +++---
 Lake/Config/SearchPath.lean  |  4 ++--
 Lake/DSL/Commands.lean       |  8 ++++----
 Lake/Util/Async.lean         | 22 +++++++++++-----------
 Lake/Util/Git.lean           |  6 +++---
 Lake/Util/Log.lean           | 12 ++++++------
 16 files changed, 66 insertions(+), 66 deletions(-)

diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean
index 148d8061c0..4559095780 100644
--- a/Lake/Build/Module.lean
+++ b/Lake/Build/Module.lean
@@ -132,7 +132,7 @@ def moduleTarget
     unless upToDate do
       build
     fullTrace.writeToFile traceFile
-    depTrace
+    return depTrace
 
 def moduleOleanAndCTarget
 (leanFile cFile oleanFile traceFile : FilePath)
diff --git a/Lake/Build/Monad.lean b/Lake/Build/Monad.lean
index 302f1b6e51..347fbb9639 100644
--- a/Lake/Build/Monad.lean
+++ b/Lake/Build/Monad.lean
@@ -30,7 +30,7 @@ instance [Monad m] : MonadLake (BuildT m) where
   (·.leanTrace) <$> read
 
 def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α
-| Except.ok a => a
+| Except.ok a => pure a
 | Except.error cycle => do
   let cycle := cycle.map (s!"  {·}")
   error s!"build cycle detected:\n{"\n".intercalate cycle}"
diff --git a/Lake/Build/Recursive.lean b/Lake/Build/Recursive.lean
index 1dc51b196f..7bf90b2e23 100644
--- a/Lake/Build/Recursive.lean
+++ b/Lake/Build/Recursive.lean
@@ -82,7 +82,7 @@ abbrev RBMapT.{u,v} (k : Type u) (o : Type u) (cmp : k → k → Ordering) (m :
   StateT (RBMap k o cmp) m
 
 instance (cmp) [Monad m] : MonadStore k o (RBMapT k o cmp m) where
-  fetch? key := do (← get).find? key
+  fetch? key := return (← get).find? key
   store key obj := modify (·.insert key obj)
 
 /-- Monad transformer for an `RBMap`-based topological walk. -/
diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean
index db22255d70..4a251ef6bc 100644
--- a/Lake/Build/Target.lean
+++ b/Lake/Build/Target.lean
@@ -64,7 +64,7 @@ def buildOpaque [Await k m'] [MonadLiftT m' m] [Functor m] (self : ActiveTarget
 def mixOpaqueAsync
 [MixTrace t] [SeqWithAsync n k] [MonadLiftT n m] [Monad m]
 (t1 : ActiveTarget α k t) (t2 : ActiveTarget β k t) : m (ActiveTarget PUnit k t) := do
-  ActiveTarget.opaque <| ← liftM <| seqWithAsync mixTrace t1.task t2.task
+  pure <| ActiveTarget.opaque <| ← liftM <| seqWithAsync mixTrace t1.task t2.task
 
 section
 variable [NilTrace t] [MixTrace t]
@@ -78,16 +78,16 @@ def materializeArray [Await k n] [MonadLiftT n m] [Monad m] (targets : Array (Ac
 variable [SeqWithAsync n k] [Monad n] [MonadLiftT n m] [Monad m] [Pure k]
 
 def collectList (targets : List (ActiveTarget i k t)) : m (ActiveTarget (List i) k t) := do
-  mk (targets.map (·.info)) <| ← liftM <| foldRightListAsync mixTrace nilTrace <| targets.map (·.task)
+  pure <| mk (targets.map (·.info)) <| ← liftM <| foldRightListAsync mixTrace nilTrace <| targets.map (·.task)
 
 def collectArray (targets : Array (ActiveTarget i k t)) : m (ActiveTarget (Array i) k t) := do
-  mk (targets.map (·.info)) <| ← liftM <| foldRightArrayAsync mixTrace nilTrace <| targets.map (·.task)
+  pure <| mk (targets.map (·.info)) <| ← liftM <| foldRightArrayAsync mixTrace nilTrace <| targets.map (·.task)
 
 def collectOpaqueList (targets : List (ActiveTarget i k t)) : m (ActiveTarget PUnit k t) := do
-  opaque <| ← liftM <| foldRightListAsync mixTrace nilTrace <| targets.map (·.task)
+  pure <| opaque <| ← liftM <| foldRightListAsync mixTrace nilTrace <| targets.map (·.task)
 
 def collectOpaqueArray (targets : Array (ActiveTarget i k t)) : m (ActiveTarget PUnit k t) := do
-  opaque <| ← liftM <| foldRightArrayAsync mixTrace nilTrace <| targets.map (·.task)
+  pure <| opaque <| ← liftM <| foldRightArrayAsync mixTrace nilTrace <| targets.map (·.task)
 
 end
 end ActiveTarget
@@ -130,10 +130,10 @@ protected def async [Async m n k] (info : i) (act : m t) : Target i n k t :=
   mk info <| async act
 
 def active [Pure n] (target : ActiveTarget i k t) : Target i n k t :=
-  mk target.info <| target.task
+  mk target.info <| pure target.task
 
 protected def pure [Pure n] [Pure k] (info : i) (trace : t) : Target i n k t :=
-  mk info <| pure trace
+  mk info <| pure <| pure trace
 
 def nil [NilTrace t] [Pure n] [Pure k] : Target PUnit n k t :=
   mk () <| pure <| pure <| nilTrace
diff --git a/Lake/Build/Trace.lean b/Lake/Build/Trace.lean
index 1964bcb2e2..9164746e89 100644
--- a/Lake/Build/Trace.lean
+++ b/Lake/Build/Trace.lean
@@ -87,8 +87,8 @@ namespace Hash
 def ofNat (n : Nat) :=
   mk n.toUInt64
 
-def loadFromFile (hashFile : FilePath) : IO (Option Hash) := do
-  (← IO.FS.readFile hashFile).toNat?.map ofNat
+def loadFromFile (hashFile : FilePath) : IO (Option Hash) :=
+  return (← IO.FS.readFile hashFile).toNat?.map ofNat
 
 def nil : Hash :=
   mk <| 1723 -- same as Name.anonymous
@@ -165,14 +165,14 @@ class GetMTime (α) where
 export GetMTime (getMTime)
 instance [GetMTime α] : ComputeTrace α IO MTime := ⟨getMTime⟩
 
-def getFileMTime (file : FilePath) : IO MTime := do
-  (← file.metadata).modified
+def getFileMTime (file : FilePath) : IO MTime :=
+  return (← file.metadata).modified
 
 instance : GetMTime FilePath := ⟨getFileMTime⟩
 
 /-- Check if the info's `MTIme` is at least `depMTime`. -/
 def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : IO Bool := do
-  try (← getMTime info) >= depMTime catch _ => false
+  try pure ((← getMTime info) >= depMTime) catch _ => pure false
 
 --------------------------------------------------------------------------------
 -- # Lake Build Trace (Hash + MTIme)
@@ -213,8 +213,8 @@ def nil : BuildTrace :=
 
 instance : NilTrace BuildTrace := ⟨nil⟩
 
-def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace := do
-  mk (← computeHash info) (← getMTime info)
+def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace :=
+  return mk (← computeHash info) (← getMTime info)
 
 instance [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] : ComputeTrace i IO BuildTrace := ⟨compute⟩
 
@@ -229,7 +229,7 @@ to see if the target is up-to-date.
 -/
 def checkAgainstHash [CheckExists i]
 (info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool :=
-  hash == self.hash <&&> checkExists info
+  pure (hash == self.hash) <&&> checkExists info
 
 /--
 Check the build trace against the given target info and its trace file
@@ -242,7 +242,7 @@ def checkAgainstFile [CheckExists i] [GetMTime i]
       self.checkAgainstHash info hash
     else
       return self.mtime < (← getMTime info)
-  act.catchExceptions fun _ => false
+  act.catchExceptions fun _ => pure false
 
 def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit :=
   IO.FS.writeFile traceFile self.hash.toString
diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean
index 8452a92236..041a739b76 100644
--- a/Lake/CLI/Build.lean
+++ b/Lake/CLI/Build.lean
@@ -12,10 +12,10 @@ namespace Lake
 
 def parsePkgSpec (ws : Workspace) (spec : String) : IO Package :=
   if spec.isEmpty then
-    ws.root
+    return ws.root
   else
     match ws.packageByName? spec.toName with
-    | some pkg => pkg
+    | some pkg => return pkg
     | none => error s!"unknown package `{spec}`"
 
 def parseTargetBaseSpec (ws : Workspace) (spec : String) : IO (Package × Option Name) := do
diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean
index 6332e85b0c..aa5d980867 100644
--- a/Lake/CLI/Main.lean
+++ b/Lake/CLI/Main.lean
@@ -40,7 +40,7 @@ namespace Cli
 
 /-- Print out a line wih the given message and then exit with an error code. -/
 protected def error (msg : String) (rc : UInt32 := 1) : MainM α := do
-  IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
+  IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => pure ()
   exit rc
 
 instance : MonadError MainM := ⟨Cli.error⟩
@@ -91,10 +91,10 @@ def loadPkg (args : List String := []) : CliStateM Package := do
 
 def loadWorkspace (args : List String := []) : CliStateM Workspace := do
   let pkg ← loadPkg args
-  let ws ← Workspace.ofPackage pkg
+  let ws := Workspace.ofPackage pkg
   let packageMap ← resolveDeps ws pkg |>.run LogMethods.eio (m := IO)
   let packageMap := packageMap.insert pkg.name pkg
-  {ws with packageMap}
+  return {ws with packageMap}
 
 /-- Get the Lean installation. Error if missing. -/
 def getLeanInstall : CliStateM LeanInstall := do
@@ -129,7 +129,7 @@ def runBuildM_ (ws : Workspace) (x : BuildM α) : CliStateM PUnit :=
 def takeArg (errMsg : String := "missing argument") : CliM String := do
   match (← takeArg?) with
   | none => error errMsg
-  | some arg => arg
+  | some arg => return arg
 
 /--
 Verify that there are no CLI arguments remaining
@@ -218,8 +218,8 @@ def serve (pkg : Package) (args : Array String := #[]) : LakeT IO UInt32 := do
 
 def parseScriptSpec (ws : Workspace) (spec : String) : IO (Package × String) :=
   match spec.splitOn "/" with
-  | [script] => (ws.root, script)
-  | [pkg, script] => do (← parsePkgSpec ws pkg, script)
+  | [script] => return (ws.root, script)
+  | [pkg, script] => return (← parsePkgSpec ws pkg, script)
   | _ =>  error s!"invalid script spec '{spec}' (too many '/')"
 
 def script : (cmd : String) → CliM PUnit
diff --git a/Lake/Config/Glob.lean b/Lake/Config/Glob.lean
index 87150936fd..ef31f354db 100644
--- a/Lake/Config/Glob.lean
+++ b/Lake/Config/Glob.lean
@@ -43,7 +43,7 @@ partial def pushSubmodules
 
 def Glob.pushModules
 (dir : FilePath) (arr : Array Name) : (self : Glob) → IO (Array Name)
-| one n => #[n]
+| one n => pure #[n]
 | submodules n => pushSubmodules dir n arr
 | andSubmodules n => pushSubmodules dir n (arr.push n)
 
diff --git a/Lake/Config/InstallPath.lean b/Lake/Config/InstallPath.lean
index f9573dc0a5..449c976432 100644
--- a/Lake/Config/InstallPath.lean
+++ b/Lake/Config/InstallPath.lean
@@ -70,10 +70,10 @@ def findLeanSysroot? (lean := "lean") : BaseIO (Option FilePath) := do
       args := #["--print-prefix"]
     }
     if out.exitCode == 0 then
-      some <| FilePath.mk <| out.stdout.trim
+      pure <| some <| FilePath.mk <| out.stdout.trim
     else
-      none
-  act.catchExceptions fun _ => none
+      pure <| none
+  act.catchExceptions fun _ => pure none
 
 /--
 Construct the `LeanInstall` object for the given Lean sysroot.
@@ -104,20 +104,20 @@ where
         cmd := leanExe sysroot |>.toString,
         args := #["--githash"]
       }
-      out.stdout.trim
-    act.catchExceptions fun _ => ""
+      pure <| out.stdout.trim
+    act.catchExceptions fun _ => pure ""
   findAr := do
     if let some ar ← IO.getEnv "LEAN_AR" then
       return ar
     else
       let ar := leanArExe sysroot
-      if (← ar.pathExists) then ar else "ar"
+      if (← ar.pathExists) then pure ar else pure "ar"
   findCc := do
     if let some cc ← IO.getEnv "LEAN_CC" then
       return cc
     else
       let cc := leanCcExe sysroot
-      if (← cc.pathExists) then cc else "cc"
+      if (← cc.pathExists) then pure cc else pure "cc"
 
 /--
 Try to find the installation of the given `lean` command
@@ -178,7 +178,7 @@ def findLakeInstall? : BaseIO (Option LakeInstall) := do
   if let some home ← IO.getEnv "LAKE_HOME" then
     return some {home}
   if let Except.ok lake ← IO.appPath.toBaseIO then
-    if let some home ← lakeBuildHome? lake then
+    if let some home := lakeBuildHome? lake then
       return some {home, lake}
   return none
 
diff --git a/Lake/Config/Load.lean b/Lake/Config/Load.lean
index ab25db274c..c453cd9993 100644
--- a/Lake/Config/Load.lean
+++ b/Lake/Config/Load.lean
@@ -53,7 +53,7 @@ unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
     | [pkgDeclName] =>
       let config ← evalPackageDecl env pkgDeclName dir args leanOpts
       let scripts ← scriptAttr.ext.getState env |>.foldM (init := {})
-        fun m d => do m.insert d <| ← evalScriptDecl env d leanOpts
+        fun m d => return m.insert d <| ← evalScriptDecl env d leanOpts
       return {dir, config, scripts}
     | _ => error s!"configuration file has multiple `package` declarations"
   else
diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean
index b9dd77fd65..c3e12c2949 100644
--- a/Lake/Config/Resolve.lean
+++ b/Lake/Config/Resolve.lean
@@ -37,12 +37,12 @@ downloading and/or updating it as necessary.
 -/
 def materializeDep (ws : Workspace) (pkg : Package) (dep : Dependency) : (LogT IO) FilePath :=
   match dep.src with
-  | Source.path dir => pkg.dir / dir
+  | Source.path dir => return pkg.dir / dir
   | Source.git url rev => do
     let name := dep.name.toString (escape := false)
     let depDir := ws.packagesDir / name
     materializeGit name depDir url rev
-    depDir
+    return depDir
 
 /--
 Resolves a `Dependency` relative to the given `Package`
@@ -69,7 +69,7 @@ def resolveDeps (ws : Workspace) (pkg : Package) : (LogT IO) (NameMap Package) :
   let (res, map) ← RBTopT.run <| pkg.dependencies.forM fun dep =>
     discard <| buildRBTop (cmp := Name.quickCmp) resolve Dependency.name dep
   match res with
-  | Except.ok _ => map
+  | Except.ok _ => return map
   | Except.error cycle => do
     let cycle := cycle.map (s!"  {·}")
     error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
diff --git a/Lake/Config/SearchPath.lean b/Lake/Config/SearchPath.lean
index 9399944097..1a7517698f 100644
--- a/Lake/Config/SearchPath.lean
+++ b/Lake/Config/SearchPath.lean
@@ -33,9 +33,9 @@ def setupLeanSearchPath
 (leanInstall? : Option LeanInstall) (lakeInstall? : Option LakeInstall)
 : IO Unit := do
   let mut sp : SearchPath := []
-  if let some leanInstall ← leanInstall? then
+  if let some leanInstall := leanInstall? then
     sp := leanInstall.oleanDir :: sp
-  if let some lakeInstall ← lakeInstall? then
+  if let some lakeInstall := lakeInstall? then
     sp := lakeInstall.oleanDir :: sp
   sp ← Lean.addSearchPathFromEnv sp
   Lean.searchPathRef.set sp
diff --git a/Lake/DSL/Commands.lean b/Lake/DSL/Commands.lean
index 5fbdec5566..fb59940bf2 100644
--- a/Lake/DSL/Commands.lean
+++ b/Lake/DSL/Commands.lean
@@ -37,10 +37,10 @@ scoped syntax (name := packageDecl)
 
 def expandPackageBinders
 : (dir? : Option Syntax) → (args? : Option Syntax) → MacroM (Bool × Syntax × Syntax)
-| none,     none      => do let hole ← `(_); (false, hole, hole)
-| some dir, none      => do (true, dir, ← `(_))
-| none,     some args => do (true, ← `(_), args)
-| some dir, some args => do (true, dir, args)
+| none,     none      => do let hole ← `(_); return (false, hole, hole)
+| some dir, none      => return (true, dir, ← `(_))
+| none,     some args => return (true, ← `(_), args)
+| some dir, some args => return (true, dir, args)
 
 def mkPackageDef (id : Syntax) (defn : Syntax) (doc? : Option Syntax)
 (dir? : Option Syntax) (args? : Option Syntax) (wds? : Option Syntax) : MacroM Syntax := do
diff --git a/Lake/Util/Async.lean b/Lake/Util/Async.lean
index f8d795b2fc..a0dce44fde 100644
--- a/Lake/Util/Async.lean
+++ b/Lake/Util/Async.lean
@@ -180,7 +180,7 @@ instance : BindAsync BaseIO (EIOTask ε) where
 instance : BindAsync BaseIO OptionIOTask where
   bindAsync ka f := BaseIO.bindTask ka.run fun
     | some a => f a
-    | none => pure none
+    | none => pure (pure none)
 
 instance [BindAsync n k] : BindAsync (ReaderT ρ n) k where
   bindAsync ka f := fun r => bindAsync ka fun a => f a r
@@ -193,13 +193,13 @@ instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (ExceptT ε k) where
 instance [BindAsync n k] [Pure n] [Pure k] : BindAsync n (OptionT k) where
   bindAsync ka f := cast (by delta OptionT; rfl) <| bindAsync ka.run fun
     | some a => f a
-    | none => pure none
+    | none => pure (pure none)
 
 instance : ApplicativeAsync Id Task where
   seqWithAsync f ka kb := ka.bind fun a => kb.bind fun b => pure <| f a b
 
 instance : ApplicativeAsync BaseIO BaseIOTask where
-  seqWithAsync f ka kb := BaseIO.bindTask ka fun a => BaseIO.bindTask kb fun b => pure <| f a b
+  seqWithAsync f ka kb := BaseIO.bindTask ka fun a => BaseIO.bindTask kb fun b => pure <| pure <| f a b
 
 instance [ApplicativeAsync n k] : ApplicativeAsync n (ExceptT ε k) where
   seqWithAsync f ka kb :=
@@ -230,12 +230,12 @@ def seqLeftList1Async [SeqLeftAsync n k] [Monad n] (last : (k α)) : (tasks : Li
 
 /-- Combine all (a)synchronous tasks in a `List` from right to left into a single task. -/
 def seqLeftListAsync [SeqLeftAsync n k] [Monad n] [Pure k] : (tasks : List (k PUnit)) → n (k PUnit)
-| [] => return ()
+| [] => return (pure ())
 | t::ts => seqLeftList1Async t ts
 
 /-- Combine all (a)synchronous tasks in a `List` from left to right into a single task. -/
 def seqRightListAsync [SeqRightAsync n k] [Monad n] [Pure k] : (tasks : List (k PUnit)) → n (k PUnit)
-| [] => return ()
+| [] => return (pure ())
 | t::ts => ts.foldlM seqRightAsync t
 
 /-- Combine all (a)synchronous tasks in a `Array` from right to left into a single task. -/
@@ -243,14 +243,14 @@ def seqLeftArrayAsync [SeqLeftAsync n k] [Monad n] [Pure k] (tasks : Array (k PU
   if h : 0 < tasks.size then
     tasks.pop.foldrM seqLeftAsync (tasks.get ⟨tasks.size - 1, Nat.sub_lt h (by decide)⟩)
   else
-    return ()
+    return (pure ())
 
 /-- Combine all (a)synchronous tasks in a `Array` from left to right into a single task. -/
 def seqRightArrayAsync [SeqRightAsync n k] [Monad n] [Pure k] (tasks : Array (k PUnit)) : n (k PUnit) :=
   if h : 0 < tasks.size then
     tasks.foldlM seqRightAsync (tasks.get ⟨0, h⟩)
   else
-    return ()
+    return (pure ())
 
 -- ## Folding (A)synchronous Tasks
 
@@ -258,16 +258,16 @@ variable [SeqWithAsync n k] [Monad n] [Pure k]
 
 /-- Fold a `List` of (a)synchronous tasks from right to left (i.e., a right fold) into a single task. -/
 def foldLeftListAsync (f : α → β → β) (init : β) (tasks : List (k α)) : n (k β) :=
-  tasks.foldrM (seqWithAsync f) init
+  tasks.foldrM (seqWithAsync f) (pure init)
 
 /-- Fold an `Array` of (a)synchronous tasks from right to left (i.e., a right fold) into a single task. -/
 def foldLeftArrayAsync (f : α → β → β) (init : β) (tasks : Array (k α)) : n (k β) :=
-  tasks.foldrM (seqWithAsync f) init
+  tasks.foldrM (seqWithAsync f) (pure init)
 
 /-- Fold a `List` of (a)synchronous tasks from left to right (i.e., a left fold) into a single task. -/
 def foldRightListAsync (f : β → α → β) (init : β) (tasks : List (k α)) : n (k β) :=
-  tasks.foldlM (seqWithAsync f) init
+  tasks.foldlM (seqWithAsync f) (pure init)
 
 /-- Fold an `Array` of (a)synchronous tasks from left to right (i.e., a left fold) into a single task. -/
 def foldRightArrayAsync (f : β → α → β) (init : β) (tasks : Array (k α)) : n (k β) :=
-  tasks.foldlM (seqWithAsync f) init
+  tasks.foldlM (seqWithAsync f) (pure init)
diff --git a/Lake/Util/Git.lean b/Lake/Util/Git.lean
index 287dc4ddef..f1f236c136 100644
--- a/Lake/Util/Git.lean
+++ b/Lake/Util/Git.lean
@@ -46,7 +46,7 @@ def checkoutDetach (hash : String) (repo : Option FilePath := none)  :=
 
 def parseRevision (rev : String) (repo : Option FilePath := none) : IO String := do
   let rev ← captureGit #["rev-parse", "-q", "--verify", rev] repo
-  rev.trim -- remove newline at end
+  pure rev.trim -- remove newline at end
 
 def headRevision (repo : Option FilePath := none) : IO String :=
   parseRevision "HEAD" repo
@@ -62,5 +62,5 @@ def latestOriginRevision (branch : Option String) (repo : Option FilePath := non
 def revisionExists (rev : String) (repo : Option FilePath := none) : IO Bool := do
   try
     discard <| parseRevision (rev ++ "^{commit}") repo
-    true
-  catch _ => false
+    pure true
+  catch _ => pure false
diff --git a/Lake/Util/Log.lean b/Lake/Util/Log.lean
index eacacbae3b..abf4c93bd4 100644
--- a/Lake/Util/Log.lean
+++ b/Lake/Util/Log.lean
@@ -40,14 +40,14 @@ def nop [Pure m] : LogMethods m :=
 instance [Pure m] : Inhabited (LogMethods m) := ⟨LogMethods.nop⟩
 
 def io [MonadLiftT BaseIO m] : LogMethods m where
-  logInfo msg := IO.println msg |>.catchExceptions fun _ => ()
-  logWarning msg := IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => ()
-  logError msg := IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
+  logInfo msg := IO.println msg |>.catchExceptions fun _ => pure ()
+  logWarning msg := IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => pure ()
+  logError msg := IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => pure ()
 
 def eio [MonadLiftT BaseIO m] : LogMethods m where
-  logInfo msg := IO.eprintln s!"info: {msg}" |>.catchExceptions fun _ => ()
-  logWarning msg := IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => ()
-  logError msg := IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => ()
+  logInfo msg := IO.eprintln s!"info: {msg}" |>.catchExceptions fun _ => pure ()
+  logWarning msg := IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => pure ()
+  logError msg := IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => pure ()
 
 def lift [MonadLiftT m n] (self : LogMethods m) : LogMethods n where
   logInfo msg := liftM <| self.logInfo msg