std.progress

For saying what a program is doing: its tasks, a tree of them, each with how many of its items are done, of how many — as zig’s std.Progress has them. A program says what it starts, does and ends; where that goes is its handler’s to say: drawn, on the terminal, below what the program writes, redrawn as it goes and gone at its end, as zig draws its own; or silently, nowhere. shown takes the one the standard error is for: drawn where it is a terminal (and TERM is not dumb), else silently — so that what a program writes to a file or a pipe is what it would write without them.

Drawn, the tasks go to the world’s terminal, whose side is progress.provider.c: it puts their lines on the standard error, the newest of them every 80 ms at most — none in the first 200 ms, so that a quick command shows nothing — clears them before the program writes, and draws them again below what it wrote. A command run under a task (runUnder) that reports its own progress as zig does (ZIG_PROGRESS, zig’s protocol) has its tasks drawn under that task.

Task

data Task = MkTask Int

A task: the root, which every task is under, or one started.

root

root : Task

The task every other is under: drawn as nothing, its own the tasks at the top.

ProgressF

data ProgressF (m : Type -> Type) x
  = Start Task String Int (Task -> x)
  | Complete Task x
  | End Task x
  | RunUnder Task String (List String) (Ran -> x)

progress

progress : HFunctor

For saying what a program is doing: tasks started, completed and ended, and commands run under one, drawn where the standard error is a terminal.

start

start : {e : HFunctor}
      -> {{ev : progress <: e}}
      -> Task
      -> String
      -> Int
      -> Co e Task

A task started under parent, named, with total items to do (0: not known): in any effect the progress is in, by the evidence.

complete

complete : {e : HFunctor} -> {{ev : progress <: e}} -> Task -> Co e Unit

One more of the task’s items done.

end

end : {e : HFunctor} -> {{ev : progress <: e}} -> Task -> Co e Unit

The task done with: gone, and one more of its parent’s items done.

runUnder

runUnder : {e : HFunctor}
         -> {{ev : progress <: e}}
         -> Task
         -> String
         -> List String
         -> Co e Ran

The command run with the arguments, to its end, as std.process’s run runs it — part of the task: drawn, what the command says of its own progress, as zig does, is drawn under the task.

Shown

type Shown =
  { task : Int, parent : Int, name : String, done : Int, total : Int }

A task as it is drawn: which it is, which it is under, its name, and how many of its items are done, of how many (0: not known).

countOf

countOf : Int -> Int -> String

counted

counted : Shown -> String

under

under : Int -> List Shown -> List Shown

branch

branch : Bool -> String

stem

stem : Bool -> String

drawUnder

drawUnder : List Shown -> String -> List Shown -> List String

drawTop

drawTop : List Shown -> List Shown -> List String

draw

draw : List Shown -> List String

The lines the tasks are drawn as, as zig draws its own: those under the root at the top, each task’s own under it, in the order they were started.

>>> draw [{ task = 1, parent = 0, name = "checking modules", done = 3, total = 9 }, { task = 2, parent = 1, name = "heff.cst", done = 0, total = 0 }]
Cons "[3/9] checking modules" (Cons "└─ heff.cst" Nil)
>>> draw [{ task = 1, parent = 0, name = "building", done = 0, total = 2 }, { task = 2, parent = 1, name = "a", done = 1, total = 0 }, { task = 3, parent = 2, name = "zig cc", done = 0, total = 0 }, { task = 4, parent = 1, name = "b", done = 0, total = 0 }]
Cons "[0/2] building" (Cons "├─ [1] a" (Cons "│  └─ zig cc" (Cons "└─ b" Nil)))

Kid

data Kid = MkKid String Int Int Int

A task of a command run under a task of the program, as it reports it (zig’s std.Progress, through ZIG_PROGRESS): its name, how many of its items are done, of how many, and the index, among those it reports, of the one it is under (255: none, the first, its root).

kidTask

kidTask : Int -> Int -> Int

kidsUnder

kidsUnder : Int -> Int -> List Kid -> List Shown

rooted

rooted : Int -> Kid -> Shown -> Shown

graft

graft : Int -> List Kid -> List Shown -> List Shown

The tasks with those a command run under the task t reports (its root first) put under it.

>>> draw (graft 2 [MkKid "" 5 0 255, MkKid "Linking" 7 9 0, MkKid "a.c" 0 0 0] [{ task = 1, parent = 0, name = "x", done = 0, total = 1 }, { task = 2, parent = 1, name = "zig cc", done = 0, total = 0 }])
Cons "[0/1] x" (Cons "└─ [5] zig cc" (Cons "   ├─ [7/9] Linking" (Cons "   └─ a.c" Nil)))

Tasks

type Tasks = { next : Int, going : List Shown }

The tasks going on, in the order they were started, and the number the next one is given.

bumpOne

bumpOne : Int -> Shown -> Shown

bump

bump : Int -> List Shown -> List Shown

parentOf

parentOf : Int -> List Shown -> Int

started

started : Int -> String -> Int -> Tasks -> Tasks

ended

ended : Int -> Tasks -> Tasks

>>> draw (ended 2 (started 1 "b" 0 (started 1 "a" 0 (started 0 "x" 2 { next = 1, going = Nil })))).going
Cons "[1/2] x" (Cons "└─ b" Nil)

TerminalF

data TerminalF (m : Type -> Type) x
  = IsTerminal (Bool -> x)
  | ShowLines (List String) x
  | ShowRun String (List String) (List Kid -> List String) (Ran -> x)

terminal

terminal : HFunctor

For lines drawn on the terminal the standard error is, below what the program writes: what progress is drawn by.

isTerminal

isTerminal : {e : HFunctor} -> {{ev : terminal <: e}} -> Co e Bool

The standard error is a terminal lines may be drawn on: TERM is not dumb.

showLines

showLines : {e : HFunctor} -> {{ev : terminal <: e}} -> List String -> Co e Unit

The lines drawn, in place of those before (none: nothing drawn, at once).

showRun

showRun : {e : HFunctor}
        -> {{ev : terminal <: e}}
        -> String
        -> List String
        -> (List Kid -> List String)
        -> Co e Ran

The command run, as std.process’s run runs it, and the lines drawn meanwhile those lines makes of what it says of its own progress (if it says any: zig’s protocol, through ZIG_PROGRESS).

quietly

quietly : {m : Type -> Type}
        -> {e : HFunctor}
        -> {a : Type}
        -> {{sys : process <: e}}
        -> ProgressF m a
        -> Co e a

silently

silently : {e : HFunctor}
         -> {a : Type}
         -> {{sys : process <: e}}
         -> Co (progress <+> e) a
         -> Co e a

Progress shown nowhere: what the program does, done as if it said nothing of it.

redrawn

redrawn : {e : HFunctor}
        -> {a : Type}
        -> {{term : terminal <: e}}
        -> Tasks
        -> a
        -> Co e (Tasks, a)

drawnOp

drawnOp : {m : Type -> Type}
        -> {e : HFunctor}
        -> {a : Type}
        -> {{term : terminal <: e}}
        -> Tasks
        -> ProgressF m a
        -> Co e (Tasks, a)

drawing

drawing : (e : HFunctor) -> {{term : terminal <: e}} -> Handler (progress <+> e)

The handler drawing the tasks: a computation of it is one of the rest, given the tasks going on, giving back those going on after it (an operation of the rest is one again, its computations run with the tasks as they are).

drawn

drawn : {e : HFunctor}
      -> {a : Type}
      -> {{term : terminal <: e}}
      -> Co (progress <+> e) a
      -> Co e a

Progress drawn on the terminal: each task as it goes, and nothing at the end.

shown

shown : {e : HFunctor}
      -> {a : Type}
      -> {{sys : process <: e}}
      -> {{term : terminal <: e}}
      -> Co (progress <+> e) a
      -> Co e a

Progress drawn where the standard error is a terminal, else shown nowhere.