HepLean Documentation

Lake.Util.Proc

source
def Lake.mkCmdLog (args : IO.Process.SpawnArgs) :
String
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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.
    Instances For
      source
      @[inline]
      def Lake.rawProc (args : IO.Process.SpawnArgs) (quiet : Bool := false) :
      Lake.LogIO IO.Process.Output
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lake.proc (args : IO.Process.SpawnArgs) (quiet : Bool := false) :
        Lake.LogIO Unit
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Lake.captureProc (args : IO.Process.SpawnArgs) :
          Lake.LogIO String
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lake.captureProc? (args : IO.Process.SpawnArgs) :
            BaseIO (Option String)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Lake.testProc (args : IO.Process.SpawnArgs) :
              BaseIO Bool
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For