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.
12	import Base
13	import 0xead4c7939c9eaca8d47da53b4496b731/main.bend as R
14	import ../share/args.bend as Args
15	import ../share/env.bend as Env
16	import ../share/cap.bend as Cap
17	import ./quiet.bend as Q
18	import ./sorted.bend as Sort
19	import ../ez/ends.bend as E
20	import ../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.
26	def 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
34	def 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.
41	def 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
46	def 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
53	def out.at() -> String:
54	  ".ez/run/prove"
55	
56	# the first line of a run's output
57	def 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
65	def head(text: String) -> String:
66	  head.of(String.lines(text))
67	
68	# the one line a proof passes on
69	def verdict() -> String:
70	  "ALL PROOFS CHECK"
71	
72	# every line of a block, indented under the line that introduces it
73	def 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
81	def 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
86	def 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
90	def 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.
100	def 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
108	def 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
113	def 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.
123	def 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
133	def 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.
147	def 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.
155	def 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))