src/ez/prove.bend fails

raw source on the hub · import 0x886223f5c47e4983fe57d887c034bc7f/src/ez/prove.bend as Prove

ez/prove: the proof gate. Every PROOF.bend in the tree is run through bend, all of them at once, and a proof passes only when the first line bend prints is exactly ALL PROOFS CHECK. Nothing is cached: a gate CI leans on answers for the tree in front of it, not for one it saw before.

The line is the verdict, never the exit status. Since bend 2.0.32 a file with no main is answered ALL PROOFS CHECK or SOME PROOFS FAIL, and a proof that reaches an @unsafe def or foreign code, imports included, fails and exits 1 rather than passing with a note as 2.0.31 did. The gate reads the line all the same: a status says nothing about what was checked, and only that first line says every term was proved outright.

9 imports

import Base
import 0xabe575924687afad4cee1a2c1194d639/main.bend as R
import ../share/args.bend as Args
import ../share/env.bend as Env
import ../share/cap.bend as Cap
import ./quiet.bend as Q
import ./sorted.bend as Sort
import ../ez/ends.bend as E
import ../lock/run.bend as Run

Definitions

def find.at source · line 26 · raw

@+what:String -> @+how:String -> IO(List<&2, String>)

every file of a kind in the tree, sorted, so a run's report is the same twice over. Base has no readdir, so this is find. .claude is skipped along with .ez: an agent's worktree is a whole second copy of the repo living inside it, and running its files would double the gate to check nothing new.

def find.proofs source · line 34 · raw

IO(List<&2, String>)

every proof file

def width source · line 41 · raw

IO(String)

how many bend runs may be in flight at once. Empty is the usual answer and means the effect works it out: cores, but never more of them than the memory cap divides the machine into, since each one of these may claim the whole cap. EZ_JOBS overrides it for a machine that knows better.

def fresh.dir source · line 46 · raw

@+at:String -> IO(Unit)

a directory emptied and made again, so nothing a run reads was written by the run before it

def out.at source · line 53 · raw

String

where the jobs of this run write what they print

def head.of source · line 57 · raw

@ls:List<&2, String> -> String

the first line of a run's output

def head source · line 65 · raw

@text:String -> String

the first line of some text

def verdict source · line 69 · raw

String

the one line a proof passes on

def indent.go source · line 73 · raw

@ls:List<&2, String> -> List<&2, String>

every line of a block, indented under the line that introduces it

def indent source · line 81 · raw

@text:String -> String

a block of text, indented

def cmd source · line 86 · raw

@cap:Bool -> @+gigs:String -> @+at:String -> @+path:String -> List<&2, String>

a bend on one file, inside the memory cap and with this project's BEND_LIB set for it

def cmds source · line 90 · raw

@ps:List<&2, String> -> @+cap:Bool -> @+gigs:String -> @+at:String -> List<&2, List<&2, String>>

every file's command, in the tree's order

def say source · line 100 · raw

@ok:Bool -> @+path:String -> @+text:String -> IO(Unit)

one proof's line. A proof that held says so in one line; one that did not names itself and then prints what bend said, since that is where the law that failed is named.

def count source · line 108 · raw

@ok:Bool -> @+passed:Nat -> Nat

one more proof counted, and one more pass when it held

def one source · line 113 · raw

@+path:String -> @+gigs:String -> @+output:String -> @+passed:Nat -> IO(Nat)

one proof against its answer: the run's first line, with a memory kill turned into a sentence in front of what it printed

def short source · line 123 · raw

@ps:List<&2, String> -> IO(Unit)

every proof the answers ran out before. The two lists are the same length by construction and this should never have one to report, but the alternative to saying so is a green count over fewer proofs than the tree holds.

def report source · line 133 · raw

@ps:List<&2, String> -> @as:List<&2, String> -> @+gigs:String -> @+passed:Nat -> IO(Nat)

every proof, in the tree's order however the run happened to interleave

def done source · line 147 · raw

@+passed:Nat -> @+total:Nat -> IO(Unit)

the count, and the exit status it implies. A run's last line is its verdict, and anything that failed fails the command (E.counted), or a script around it learns nothing.

def run source · line 155 · raw

IO(Unit)

ez prove: every PROOF.bend in the tree, run at once and reported in the tree's order. There is no budget: a proof that takes long is still a proof, and one that never finishes is stopped by whatever runs the gate.