src/ez/prove.bend
ezx@1.6.0.0 · 166 lines · 0 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.3.0.0/main.bend as R
14import ezx@1.6.0.0/src/share/args.bend as Args
15import ezx@1.6.0.0/src/share/env.bend as Env
16import ezx@1.6.0.0/src/share/cap.bend as Cap
17import ezx@1.6.0.0/src/ez/quiet.bend as Q
18import ezx@1.6.0.0/src/ez/sorted.bend as Sort
19import ezx@1.6.0.0/src/ez/ends.bend as E
20import ezx@1.6.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))