chore: auto pure was removed
This commit is contained in:
Leonardo de Moura
Mac
parent
0869780376
commit
8c40a31573
16 changed files with 66 additions and 66 deletions
|
|
@ -132,7 +132,7 @@ def moduleTarget
|
|||
unless upToDate do
|
||||
build
|
||||
fullTrace.writeToFile traceFile
|
||||
depTrace
|
||||
return depTrace
|
||||
|
||||
def moduleOleanAndCTarget
|
||||
(leanFile cFile oleanFile traceFile : FilePath)
|
||||
|
|
|
|||
|
|
@ -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}"
|
||||
|
|
|
|||
|
|
@ -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. -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue