src/ez/prove.bend

ezx@1.11.0.0 · 166 lines · 19 definitions

1# ez/prove: the proof gate. Every PROOF.bend in the tree is run through `bend`,
2# all of them at once, and a proof passes only when the first line bend prints
3# is exactly `ALL PROOFS CHECK`. Nothing is cached: a gate CI leans on answers
4# for the tree in front of it, not for one it saw before.
5#
6# The line is the verdict, never the exit status. Since bend 2.0.32 a file
7# with no main is answered `ALL PROOFS CHECK` or `SOME PROOFS FAIL`, and a
8# proof that reaches an `@unsafe` def or foreign code, imports included, fails
9# and exits 1 rather than passing with a note as 2.0.31 did. The gate reads
10# the line all the same: a status says nothing about what was checked, and
11# only that first line says every term was proved outright.
12import Base
13import snap@1.4.0.0/main.bend as R
14import ezx@1.11.0.0/src/share/args.bend as Args
15import ezx@1.11.0.0/src/share/env.bend as Env
16import ezx@1.11.0.0/src/share/cap.bend as Cap
17import ezx@1.11.0.0/src/ez/quiet.bend as Q
18import ezx@1.11.0.0/src/ez/sorted.bend as Sort
19import ezx@1.11.0.0/src/ez/ends.bend as E
20import ezx@1.11.0.0/src/lock/run.bend as Run
21
22# every file of a kind in the tree, sorted, so a run's report is the same twice
23# over. Base has no readdir, so this is `find`. `.claude` is skipped along with
24# `.ez`: an agent's worktree is a whole second copy of the repo living inside
25# it, and running its files would double the gate to check nothing new.
26def find.at(+what: String, +how: String) -> IO(List<&2, String>):
27  do IO<List<&2, String>>:
28    out : String <- R.exec(["find", ".", how, what,
29      "-not", "-path", "./.ez/*",
30      "-not", "-path", "./.git/*", "-not", "-path", "./.claude/*"])
31    return Sort.sort(Args.nonempty(String.lines(R.text(out))))
32
33# every proof file
34def find.proofs() -> IO(List<&2, String>):
35  find.at("PROOF.bend", "-name")
36
37# how many `bend` runs may be in flight at once. Empty is the usual answer and
38# means the effect works it out: cores, but never more of them than the memory
39# cap divides the machine into, since each one of these may claim the whole
40# cap. EZ_JOBS overrides it for a machine that knows better.
41def width() -> IO(String):
42  Env.var("EZ_JOBS", "")
43
44# a directory emptied and made again, so nothing a run reads was written by the
45# run before it
46def fresh.dir(+at: String) -> IO(Unit):
47  do IO<Unit>:
48    _rm : String <- R.exec(["rm", "-rf", at])
49    _mk : String <- R.exec(["mkdir", "-p", at])
50    return Unit{}
51
52# where the jobs of this run write what they print
53def out.at() -> String:
54  ".ez/run/prove"
55
56# the first line of a run's output
57def head.of(ls: List<&2, String>) -> String:
58  match ls:
59    case []:
60      ""
61    case h <> _t:
62      h
63
64# the first line of some text
65def head(text: String) -> String:
66  head.of(String.lines(text))
67
68# the one line a proof passes on
69def verdict() -> String:
70  "ALL PROOFS CHECK"
71
72# every line of a block, indented under the line that introduces it
73def indent.go(ls: List<&2, String>) -> List<&2, String>:
74  match ls:
75    case []:
76      []
77    case h <> t:
78      ("    " ++ h ++ "\n") <> indent.go(t)
79
80# a block of text, indented
81def indent(text: String) -> String:
82  String.concat(indent.go(String.lines(text)))
83
84# a `bend` on one file, inside the memory cap and with this project's BEND_LIB
85# set for it
86def cmd(cap: Bool, +gigs: String, +at: String, +path: String) -> List<&2, String>:
87  Cap.argv(cap, gigs, at, ["bend", path])
88
89# every file's command, in the tree's order
90def cmds(ps: List<&2, String>, +cap: Bool, +gigs: String, +at: String) -> List<&2, List<&2, String>>:
91  match ps:
92    case Nil{}:
93      Nil{}
94    case Con{+h, t}:
95      cmd(cap, gigs, at, h) <> cmds(t, cap, gigs, at)
96
97# one proof's line. A proof that held says so in one line; one that did not
98# names itself and then prints what bend said, since that is where the law
99# that failed is named.
100def say(ok: Bool, +path: String, +text: String) -> IO(Unit):
101  match ok:
102    case True{}:
103      IO.print("ok: " ++ path)
104    case False{}:
105      IO.write("FAIL: " ++ path ++ "\n" ++ indent(text))
106
107# one more proof counted, and one more pass when it held
108def count(ok: Bool, +passed: Nat) -> Nat:
109  Bool.pick(Nat, ok, (1n + passed : Nat), passed)
110
111# one proof against its answer: the run's first line, with a memory kill turned
112# into a sentence in front of what it printed
113def one(+path: String, +gigs: String, +output: String, +passed: Nat) -> IO(Nat):
114  do IO<Nat>:
115    +text : String <- IO.pure(String, R.text(output))
116    +ok : Bool <- IO.pure(Bool, String.eq(head(text), verdict()))
117    say(ok, path, Cap.why(output, gigs) ++ Q.chomp(text))
118    return count(ok, passed)
119
120# every proof the answers ran out before. The two lists are the same length by
121# construction and this should never have one to report, but the alternative
122# to saying so is a green count over fewer proofs than the tree holds.
123def short(ps: List<&2, String>) -> IO(Unit):
124  match ps:
125    case Nil{}:
126      IO.pure(Unit, Unit{})
127    case Con{+h, t}:
128      do IO<Unit>:
129        IO.print("FAIL: " ++ h ++ ": the run never answered for it")
130        short(t)
131
132# every proof, in the tree's order however the run happened to interleave
133def report(ps: List<&2, String>, as: List<&2, String>, +gigs: String, +passed: Nat) -> IO(Nat):
134  match ps as:
135    case Con{+h, pt} Con{+x, xt}:
136      do IO<Nat>:
137        next : Nat <- one(h, gigs, x, passed)
138        report(pt, xt, gigs, next)
139    case rest _x:
140      do IO<Nat>:
141        short(rest)
142        return passed
143
144# the count, and the exit status it implies. A run's last line is its verdict,
145# and anything that failed fails the command (`E.counted`), or a script around
146# it learns nothing.
147def done(+passed: Nat, +total: Nat) -> IO(Unit):
148  do IO<Unit>:
149    IO.print("PASS: " ++ Nat.show(passed) ++ " / " ++ Nat.show(total))
150    Run.end(E.counted(passed, total))
151
152# `ez prove`: every PROOF.bend in the tree, run at once and reported in the
153# tree's order. There is no budget: a proof that takes long is still a proof,
154# and one that never finishes is stopped by whatever runs the gate.
155def run() -> IO(Unit):
156  do IO<Unit>:
157    +cap : Bool <- Cap.ok()
158    Cap.warn(cap)
159    +g : String <- Cap.gb()
160    +at : String <- Env.lib()
161    +jobs : String <- width()
162    +ps : List<&2, String> <- find.proofs()
163    fresh.dir(out.at())
164    as : List<&2, String> <- R.par(cmds(ps, cap, g, at), jobs, g, out.at(), "0")
165    +passed : Nat <- report(ps, as, g, 0n)
166    done(passed, List.length(&2, String, ps))