chore: lake: code cleanup

* remove MTime `checkIfNewer`
* remove unnecessary `@[noinline]`
* inline `MainM` combinators

Author: tydeu

src/lake/Lake/Build/Monad.lean

@@ -78,7 +78,7 @@ where
       | e => throw e
 
 /-- The name of the Lake build lock file name (i.e., `lake.lock`). -/
-@[noinline] def lockFileName : String :=
+def lockFileName : String :=
   "lake.lock"
 
 /-- The workspace's build lock file. -/

src/lake/Lake/Build/Trace.lean

@@ -205,10 +205,6 @@ instance [GetMTime α] : ComputeTrace α IO MTime := ⟨getMTime⟩
 instance : GetMTime FilePath := ⟨getFileMTime⟩
 instance : GetMTime TextFilePath := ⟨(getFileMTime ·.path)⟩
 
-/-- Check if the info's `MTIme` is at least `depMTime`. -/
-@[inline] def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool :=
-  (return (depMTime < (← getMTime info) : Bool)).catchExceptions fun _ => pure false
-
 --------------------------------------------------------------------------------
 /-! # Lake Build Trace (Hash + MTIme) -/
 --------------------------------------------------------------------------------
@@ -260,7 +256,8 @@ That is, check if the info is newer than this input trace's modification time.
 -/
 @[inline] def checkAgainstTime [GetMTime i]
 (info : i) (self : BuildTrace) : BaseIO Bool :=
-  checkIfNewer info self.mtime
+  EIO.catchExceptions (h := fun _ => pure false) do
+    return self.mtime < (← getMTime info)
 
 /--
 Check if the info is up-to-date using a trace file.

src/lake/Lake/CLI/Main.lean

@@ -85,7 +85,7 @@ abbrev CliM := ArgsT CliStateM
 
 def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
   let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall?
-  let main := self args |>.run' {elanInstall?, leanInstall?, lakeInstall?}
+  let main := self.run' args |>.run' {elanInstall?, leanInstall?, lakeInstall?}
   let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
   main.run
 
@@ -416,4 +416,4 @@ def lake : CliM PUnit := do
         throw <| CliError.missingCommand
 
 def cli (args : List String) : BaseIO ExitCode :=
-  (lake).run args
+  inline <| (lake).run args

src/lake/Lake/Config/Module.lean

@@ -86,7 +86,7 @@ abbrev pkg (self : Module) : Package :=
   self.irPath "o"
 
 /-- Suffix for single module dynlibs (e.g., for precompilation). -/
-@[noinline] def dynlibSuffix := "-1"
+def dynlibSuffix := "-1"
 
 @[inline] def dynlibName (self : Module) : String :=
   -- NOTE: file name MUST be unique on Windows

src/lake/Lake/Util/Git.lean

@@ -11,10 +11,10 @@ namespace Lake
 
 namespace Git
 
-@[noinline] def defaultRemote :=
+def defaultRemote :=
   "origin"
 
-@[noinline] def upstreamBranch :=
+def upstreamBranch :=
   "master"
 
 /--
@@ -42,7 +42,7 @@ instance : ToString GitRepo := ⟨(·.dir.toString)⟩
 
 namespace GitRepo
 
-@[noinline] def cwd : GitRepo := ⟨"."⟩
+def cwd : GitRepo := ⟨"."⟩
 
 @[inline] def dirExists (repo : GitRepo) : BaseIO Bool :=
   repo.dir.isDir

src/lake/Lake/Util/MainM.lean

@@ -33,31 +33,31 @@ namespace MainM
 @[inline] protected def toBaseIO (self : MainM α) : BaseIO (Except ExitCode α) :=
   self.toEIO.toBaseIO
 
-protected def run (self : MainM α) : BaseIO ExitCode :=
+@[inline] protected def run (self : MainM α) : BaseIO ExitCode :=
   self.toBaseIO.map fun | Except.ok _ => 0 | Except.error rc => rc
 
 /-! # Exits -/
 
 /-- Exit with given return code. -/
-protected def exit (rc : ExitCode) : MainM α :=
+@[inline] protected def exit (rc : ExitCode) : MainM α :=
   MainM.mk <| throw rc
 
 instance : MonadExit MainM := ⟨MainM.exit⟩
 
 /-- Try this and catch exits. -/
-protected def tryCatchExit (f : ExitCode → MainM α) (self : MainM α) : MainM α :=
+@[inline] protected def tryCatchExit (f : ExitCode → MainM α) (self : MainM α) : MainM α :=
   self.toEIO.tryCatch f
 
 /-- Try this and catch error codes (i.e., non-zero exits). -/
-protected def tryCatchError (f : ExitCode → MainM α) (self : MainM α) : MainM α :=
+@[inline] protected def tryCatchError (f : ExitCode → MainM α) (self : MainM α) : MainM α :=
   self.tryCatchExit fun rc => if rc = 0 then exit 0 else f rc
 
 /-- Exit with a generic error code (i.e., 1). -/
-protected def failure : MainM α :=
+@[inline] protected def failure : MainM α :=
   exit 1
 
 /-- If this exits with an error code (i.e., not 0), perform other. -/
-protected def orElse (self : MainM α) (other : Unit → MainM α) : MainM α :=
+@[inline] protected def orElse (self : MainM α) (other : Unit → MainM α) : MainM α :=
   self.tryCatchExit fun rc => if rc = 0 then exit 0 else other ()
 
 instance : Alternative MainM where
@@ -69,14 +69,14 @@ instance : Alternative MainM where
 instance : MonadLog MainM := MonadLog.eio
 
 /-- Print out a error line with the given message and then exit with an error code. -/
-protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
+@[inline] protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
   logError msg
   exit rc
 
 instance : MonadError MainM := ⟨MainM.error⟩
 instance : MonadLift IO MainM := ⟨MonadError.runEIO⟩
 
-def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
+@[inline] def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
   liftM <| x.run <| MonadLog.eio verbosity
 
 instance : MonadLift LogIO MainM := ⟨runLogIO⟩