def Lake.mkCmdLog (args : IO.Process.SpawnArgs) : String

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.logOutput {m : Type → Type u_1} [Monad m] (out : IO.Process.Output) (log : String → m PUnit) : m Unit

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.rawProc (args : IO.Process.SpawnArgs) (quiet : Bool := false) (input? : Option String := none) : LogIO IO.Process.Output

Equations

• One or more equations did not get rendered due to their size.

def Lake.proc (args : IO.Process.SpawnArgs) (quiet : Bool := false) (input? : Option String := none) : LogIO Unit

Equations

• One or more equations did not get rendered due to their size.

def Lake.captureProc' (args : IO.Process.SpawnArgs) : LogIO IO.Process.Output

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Lake.captureProc (args : IO.Process.SpawnArgs) : LogIO String

Equations

• Lake.captureProc args = do let __do_lift ← Lake.captureProc' args pure __do_lift.stdout.trimAscii.copy

def Lake.captureProc? (args : IO.Process.SpawnArgs) : BaseIO (Option String)

Equations

• One or more equations did not get rendered due to their size.

def Lake.testProc (args : IO.Process.SpawnArgs) : BaseIO Bool

Equations

• One or more equations did not get rendered due to their size.