Skip to content

README.md

Latest commit

 

History

History
504 lines (475 loc) · 31.1 KB

README.md

File metadata and controls

504 lines (475 loc) · 31.1 KB
Raw

bolt

The linter, written in Bend over the syntax/ tree and binder, and the one binary (main.bend) that is also bolt check and bolt lsp (lsp/). It enforces what the checker does not: comments, unused names, the binder-vs-def trap, leftover holes, whitespace, recursion that is strict where it should stop early or quadratic where it should be linear, unary Nat blowups, silent wrong answers (Map.put, \033, unreachable arms), foreign defs missing a lane, and laws that reach every def (IO included). Install: bend main.bend -o bin/bolt.bin at the repo root (README.md there).

bolt                every .bend file under the current directory
bolt a.bend b.bend  the files given
bolt check a.bend   the checker's errors, in the same shape
bolt lsp            the language server
bolt help           usage

Each finding is one line, path:line:col: level: CODE: message, with line and column 1-based so a terminal can jump to it; then clean or the counts. CODE is the rule's stable id (S003 is wrap). In an editor the same finding is source bolt(style:wrap) and code S003. A path that cannot be read, a missing file or a directory named on the command line, is a read finding (Cannot read this file.), graded with correctness. The exit code is 1 when anything was an error. nix profile install github:Emerging-Patterns/bolt is what puts it on the PATH as bolt.

bolt.bend

What bolt enforces, and how hard, is the project's to say, in a bolt.bend at its root. Each file is graded by the nearest bolt.bend above it (its directory, then each parent up to /), so a monorepo can set one at the top and a project can override below. A relative path is resolved against the working directory first, so the same file is graded the same way whether bolt runs from the project root, a subdirectory or elsewhere. The file is plain Bend that bend can check: a def a setting, its body one string, "off", "warn" or "error".

# every rule an error
def correctness() -> String:
  "error"
def style() -> String:
  "error"
# but width is advice here
def space() -> String:
  "warn"

A group sets every rule in it; a rule set by name wins over its group; an unset group has its default. The groups:

group rules default
correctness hole pick put arms escape twice strings chars foreign setting error
suspicious unused strict eager concat fuel index table hoist ring rewalk unit fromrev (scan, thunk: opt-in) warn
style doc space wrap param noqa warn
laws coverage closed unsafe (trace: opt-in) warn
pedantic tail off

The stable codes, assigned once (do not renumber):

code rule code rule code rule
C001 retired U001 unused S001 doc
C002 hole U002 strict S002 space
C003 pick U003 eager S003 wrap
C004 put U004 concat S004 param
C005 arms U005 retired S005 noqa
C006 escape U006 fuel L001 coverage
C007 twice U007 index L002 closed
C008 strings U008 table L003 unsafe
C009 chars U009 hoist L004 retired
C010 foreign U010 ring L005 trace
C011 setting U011 rewalk P001 tail
U012 unit
U013 scan
U014 retired
U015 thunk
U016 fromrev

Letters: C correctness, U suspicious, S style, L laws, P pedantic.

pedantic is advice that is noisy on idiomatic code: off until a project asks for it. L004 was quantify, the opt-in strict mode of closed; closed is strict itself now, and L004 is never reused. U014 was argv, a check on IO.args() readers, retired before its first release: every reader already drops the program, and it could not tell one that does from one that does not. U014 is never reused either. trace is opt-in: it is in laws, but no group setting reaches it; only def trace() in a bolt.bend turns it on. scan and thunk are opt-in the same way, in suspicious: only def scan() or def thunk() turns each on. An unknown level word grades as an error, so a typo shows. A bolt.bend is read, never linted. A setting whose name is no rule's slug and no group sets nothing, so setting (C011) reports it. Without one, the defaults apply. This repo's bolt.bend sets every group to error: the gate must see clean.

Suppressing a finding

A comment on a finding's own line that names its code silences it, as in ruff:

def run(args: List<String>) -> IO(Unit):  # noqa: L001 IO entry point

The comment is #, any spaces, noqa:, then one or more codes split by commas (spaces around them allowed), then any text. Codes are the stable ids above, case-sensitive, and a comment may name several (# noqa: U002, U003). Only a real comment counts, as the lexer reads it: noqa inside a string literal is text. The filter runs once every rule has run, the project rules (coverage, unsafe, trace) included, and a silenced finding is neither printed nor counted, so it changes neither the summary nor the exit code. No rule reads the comments: what each rule finds is the same with or without them. The editor applies the same filter.

A noqa comment that silences nothing is itself a finding, noqa (S005): a bare # noqa, which names no code, and each code that silences nothing on its line, an unknown code included. A project rule's code is judged only when bolt lints the whole tree; over files named on the line, and in the editor, those rules see only part of the laws, so their silence proves nothing. noqa runs last, and no comment silences it (# noqa: S005 is itself reported). Like any rule, def noqa() -> String: "off" in a bolt.bend turns it off.

Rules

Each rule is a module under rules/<group>/ with check(src) -> List<Finding>, listed in rules.bend: the directory a rule sits in is the group it belongs to. Adding a rule is adding a file, a line in rules.bend, and a row in codes.bend (the stable code). A project rule has check(ds) -> List<Finding> instead and sees every file the linter read at once, as digests (rules.bend's project).

A rule is handed a Src, not the text: the path, the text, and the file's tokens, tree, binder and outline, each read once for the whole set. A tree parse of a 156 KB file costs 1.5 s here, so twenty rules that each parsed the text made the linter twenty times slower than it is now. A project rule is handed one Digest a file instead: its phases use the whole list several times, and a + reuse copies what it is given, so handing them the parsed Src duplicated every tree (100 files cost 362 s, growing faster than the count; 28 s now). The digest carries only what those rules ask: the paths, the top-level defs and types, what the laws name, the imports and the @unsafe defs. What the rules share, rules/calls.bend (the recursion rules), rules/tokens.bend, rules/imports.bend and rules/digest.bend, sits beside the groups. The cost rules built on rules/calls.bend (pick, strict, eager, tail, concat, index, table, hoist, ring, rewalk, unit, scan, thunk) skip what never runs: a law file, a proof file, and a def that is a proof wherever it is, one that returns a proof (-> {a == b : T}) or one written with no type at all (def f(x, y):, no : among its parameters and no ->), which is how Bend fills the law named f.

  • doc — every top-level def, type and law has a comment block right above it: column-0 # lines with no blank line before the item, or before a run of column-0 @ lines (@unsafe) right above it. A block of bare # lines counts. Helpers (dotted names like show.go) ride on their parent's, main needs none, PROOF.bend fills laws that LAWS.bend documents, and a test (under tests/) is documented by its header and its check names.

  • unused — a name bound by a let, a do-bind, a lambda or as a parameter is never used. Exempt: pattern binders (naming every field of Tok{k, t, l, c} reads better than _), names starting with _, erased parameters (-x), a law's for names, and every parameter of a foreign def, one whose body's first statement is import (its C and JS read them), wherever its header's -> and return type fall. A name read in a dependent arrow's types (@+x: U32 -> S) is a use.

  • hole — a TODO hole left in code, the one bend counts in "1 TODO found." / "N TODOs found." (under SOME PROOFS FAIL, exit 1): ? and then TODO, with spaces, newlines or comments allowed between (?TODO, ? TODO). ?todo and ?TODO_later are other names, a type error to bend, and are not reported. LAWS.bend is exempt: its laws are open claims by convention, filled by PROOF.bend.

  • space — trailing whitespace, a tab, or a line over 120 wide. Width counts a string literal as two characters: a long fixture or message does not make a line hard to read, code does. A comment counts at its full width. #| trailers are data and exempt from the width only: trailing whitespace on a #| line is still reported. A tab is reported anywhere, inside a string literal too.

  • wrap — a def header's shape. A one-line header over 120 wide must break, counted the same way as space (a string literal is two characters), except that a comment counts nothing. The header is the text through its :; a comment after it is not part of it, so def u(aa: U32) -> U32: # note is a one-line header. A header breaks when a line break of its own is in it; one inside a string literal belongs to the string. A one-line header that fits stays one line however many parameters it has. A header that breaks puts ( at the end of the first line and one parameter on each following line, then ) and the return type on a line of their own after the last parameter. Several parameters on a line, a parameter left on the ( line, a parameter split across lines, a ) on the last parameter's line (bb: U32) -> U32:), a ) with no -> right after it on its line (the return type on a line of its own; a def that fills a law has no return type, so ): ends it), or a parameter list across lines with no parameter in it (def none( then ) -> U32:: join it onto one line), is a finding.

  • param — a parameter name shorter than 2 characters. A single uppercase letter is a type parameter (A, T), and a bare parameter or one typed Quant is a quantity. Locals, patterns and a law's for names are not parameters. A PROOF.bend's parameters are the names its law bound.

  • noqa — a noqa comment that silences nothing (see "Suppressing a finding"): a bare # noqa, or a code it names that no finding of its file on its line has, an unknown code included, one finding per code, at the comment. It reads the other rules' graded findings, so it runs after them and after the filter, and nothing silences it. A project rule's code is judged only over the whole tree.

  • pick — a def calls itself in a branch of a Bool.pick. Bool.pick is a function: both branches run whatever the condition. In both branches, two recursive calls a step is 2^n work (a per-token scan took 20 s this way and 20 ms as one pass); in one branch, the call runs even when the condition says stop, so a search never exits early. Bind the call once above the pick (+more = go(rest)) and pick between x <> more and more, or hand a helper that matches on the Bool. A self-call is the def's name followed by (..), so a parameter named like the def is not one. A pick nested in a branch of one already reported is not reported again. Law files, proof files and defs that are proofs (they return a proof, or have no type) are exempt.

  • strict — a self-call inside Bool.and/Bool.or, or either side of &&/||, matched by exactly those texts (a qualified Base.Bool.or is not seen). They are functions too: both sides always run, so there is no short-circuit (a game's overlap test went 31 -> 55 fps once the call moved out). Bind the call above, or match on the first Bool. A self-call in a lambda body (_u => go(rest), a Unit -> T thunk) is not counted: the thunk does not run eagerly, unless its own body holds &&/||.

  • eager — a branch of a Bool.pick holds a call to another def of the same file that loops (it calls itself, or reaches a def that does). Bool.pick is a def too, so the branch runs whatever the condition says (a game's overlap test in a branch went 31 -> 55 fps once it moved out; one gaps(..) in a branch here cost 88 s of a 100 s run). pick sees only the self-call and strict only Bool.and/or, so the call to a neighbour is this rule's. Bind it above the pick, or branch with match on the condition. For a search that recurses, carry the test as a Bool into the next call (go(rest, k, test(h))) and match on it first, so the step stays a loop; a Unit -> T thunk around the recursive call leaves the loop on every step (thunk). src/lazy/lazy.bend, which matches on the Bool and applies a thunk in one branch, stays right for work that does not recurse. A call into Base is not counted: a def of the file is the cheap proxy for work the file itself wrote. Nor is a call in a lambda's body (from => to the next comma of its group), which the pick does not run; an argument after that comma counts again.

  • concat — a self-call whose argument grows a carried parameter by appending (acc ++ x, List.append(&2, T, acc, ..)) in that parameter's own position: each step copies the accumulator, so the walk is quadratic. Prepend with <> and reverse once. A parameter appended into another slot is not counted. The append may sit inside parentheses ((acc ++ x)), or be bound by a let first (+q = acc ++ x, then go(t, q)): a lone name reads the nearest q = .. / +q = .. before the call in its block or an enclosing one, so a later let of the name shadows it and a let in another case arm is not seen. Typed and destructuring lets, do-binds and pattern binders are not followed.

  • index — List.get/String.get at a computed index inside a def that calls itself: the list is walked again each step. Walk the cells instead (one sort phase went 39 s -> 0.9 s). A get anywhere in the def is reported, one in a base arm that runs once included. A literal index of any size is exempt. A List.get on a fixed table is table's; a String.get always stays here. A get that is the def's own self-call (the step of a def named List.get or String.get, as Base's are) is exempt.

  • table — List.get or List.set at a computed index inside a def that calls itself, when the list is a fixed table (a literal, a sized array, or List.replicate / Array.new / List.range with a constant count), inline, as a table def of the file, or held by the let of that name in scope. A let reaches the statements after it, not a sibling case arm, and a later let of the name to anything else ends it. Keep it in an Array. A literal index, a growing list, and a data-dependent length stay with index or stay quiet, so one call is one finding.

  • hoist — a list or array of more than eight constants, or a call that builds one from inputs that do not change, sits inside a def that calls itself and is then indexed. The build runs again on every step. Build it once, outside the recursion. A call builds one when it is a Base constructor (List.replicate, Array.new, ...) or a def of the file whose body is itself a fixed table of more than eight cells; a def whose body is not in the file does not count. Eight cells or fewer, and a build whose arguments depend on the step, are left alone.

  • ring — a self-call replaces a binder with a drop of a constant count and an append (List.drop / List.tail / String.drop / String.tail, then List.append / String.append / ++), passed back in that binder's own parameter position. Each step copies the window. Keep it in an Array and advance an index. A list the def matches as input (any scrutinee of a match), a window dropped into another parameter's slot, and a one-shot trim are left alone.

  • rewalk — one straight piece of a def calls the same walk twice on the same argument, and one result is used only for a single value (one index, one field, or a let read only that way) while the other result is kept whole. Take the value from that other result. A let of a name the argument uses between the two calls makes them different walks, and so does a different case arm.

  • unit — a multiply or divide by the literal 1, 1n or 1.0 on a step that recurses, either as * / / or as Nat.mul / U32.mul / F32.mul (and .div, only when the divisor is one). Drop the operation. Any other factor or divisor is left alone, and so is a base case: a case arm that does not call the def. Only a case arm can be a base case, so a Bool.pick branch beside a self-call is still the step, and so is a lambda body inside it. One finding per operation: Nat.mul(1n, 1n) is one.

  • scan (opt-in) — a def that calls itself and, on the same step, hands a parameter it carries unchanged (every self-call passes it back as the same lone name in its own position) to a walk: a Base list search (List.contains, List.find, List.filter, List.length, List.any, List.all, List.foldl, List.foldr), or a def of the file that walks that argument (the one it shrinks, unless a Nat or a String, or one it passes to a walk). Every step walks the list again, O(|A| * |B|). Index it once outside the loop, or merge two sorted walks. A literal table or an expression in that argument, a lambda's body, a case arm that does not recurse, a Base walk that rebuilds the list (List.map, List.append), and a def of another module are left alone. One finding per call, on its callee.

  • thunk (opt-in) — a lambda whose body is exactly a self-call and whose parameter the call does not read, passed as the one lambda of a call: a Unit -> T thunk such as Lazy.or_else(hit, _u => go(rest, k)). The closure is allocated on every step and the call in it is not a tail call of the def, so the search leaves the loop each time round (bend 2.0.34, 500 misses over 100k cells: JS 2.40 s against 0.28 s, native 1.18 s against 0.76 s). Carry the test as a Bool into the next call, go(rest, k, test(h)), and match on it first: the step is then a tail call and compiles to a loop. Lazy.* stays right for guarding work that does not recurse. A dispatch, a call given two or more lambdas (Lazy.either(T, c, _u => go(a), _v => go(b))), is left alone: one carried Bool does not replace it. Exactly: in the kids of a ( group whose arguments (split at their commas) hold exactly one with a => leaf of its own (not inside a bracket), a name leaf (the parameter), =>, the def's name and its ( group, with the kids ending there or going on with a comma, and no name leaf in the group spelling the parameter or the parameter then a dot. A body that does more than the call (_u => Some{go(t)}), a continuation that reads its parameter (a => go(f, a)), or a lambda that is no call's argument (x = _u => go(t)) is left alone; _ => loop(n) is not, since the rule reads the shape and not the type.

  • fromrev — String.from_list(List.reverse(..)): among the significant tokens, String.from_list, (, List.reverse and ( right after one another, one finding on the first. A buffer of chars consed on the front and then reversed and read into a String walks the buffer twice and builds a list only to throw it away; String.from_list is not a tail call either, so a long buffer runs the JS lane out of stack. Fold the buffer onto a String with SCon in one pass (src/rchars.bend, bolt's own):

    def text.go(buf: List<&2, Char>, acc: String) -> String:
  match buf:
    case Nil{}:
      acc
    case Con{h, t}:
      text.go(t, SCon{h, acc})

    Called as text.go(buf, SNil{}) (bend 2.0.34, a 100k-char buffer 200 times: native 0.35 s against 0.17 s; JS at 20k chars 4.6 s against 3.1 s, and at 50k the two-pass form overflows). Anything between the four tokens, another ( included, is not the shape, and neither is List.reverse.go. A LAWS.bend or a PROOF.bend is exempt.

  • put — Map.put. It is Base's internal helper: at a leaf it keeps the old key and replaces the value without comparing, so a new key silently overwrites another entry. Map.set compares. A file that defines Map.put (def Map.put, Base's own source) is exempt.

  • escape — \0 then a digit in a literal ("\033"). Bend has no octal escape: that is NUL followed by the digits. Write \u{1B}.

  • strings — a match over string-literal arms totalling more than 64 characters: compile time and memory blow up with the characters (45 chars cost 0.8 s and 0.35 GB here, 480 chars 12 s and 4.8 GB). Map the string to a sum type once. Only the first match column is read, and a literal with no closing quote is not counted.

  • chars — a match with more than eight character-literal arms (case '.':). Char is Chr{code: U32}, so each arm is a U32 literal inside a constructor pattern, and the C backend pays about 90 MB for one (eighteen arms cost 1.57 GB and 8.3 s here, 0.10 GB and 0.7 s once rewritten), compounding through every def downstream. It is the literals, not the arms: a match over eighteen constructors costs nothing measurable. Compare Char.to_u32(c) instead. Bind the fallback above the comparisons so eager does not fire on it, and take +c: Char, since the code point and the fallback both consume it. Where the arms carry linear values, leave the match alone: a cascade would break linearity and do every branch's work. Only the first match column is read, and only an arm whose pattern opens with a character literal counts (case Con{'x', t}: does not).

  • twice — a case pattern that opens with the same literal twice (case 10 <> 10 <> ..) in a recursive def: the checker hangs. Match one element a step. A def is recursive when its body calls it (name(..)); a parameter named like the def is not a call. Only the first match column is read.

  • arms — a later Nat arm that an earlier kn+p already matches, so it is unreachable. Succ{p} and Succ{_} count as 1n+p. The checker takes it silently and the answer is wrong: put the narrow arms first.

  • foreign — a foreign def with a .c body and no .js body, or the reverse: the missing lane cannot run it. A file headed # lanes: native needs no .js: that exact line must be one of the comment lines before the file's first non-comment line.

  • setting — a setting in a bolt.bend whose name is no rule's slug and no group (def wrp() -> String: "off", or a retired name such as quantify or shadow): grading only looks names up, so it sets nothing, and the typo fails open. It is reported once for each bolt.bend that grades a file of the run, at that bolt.bend's path and the setting's def line, after the per-file findings and before coverage, unsafe and trace. It is graded by that bolt.bend like any rule (def setting() -> String: "off" there turns it off). A bolt.bend is read, not linted, so a noqa comment in one silences nothing. bolt runs it; the editor does not.

  • fuel — a Nat literal (digits, then n), or U32.to_nat of a U32 literal (U32.to_nat(100000)), passed in a call, name(..), to a fuel parameter of a def of the same file. A fuel parameter is known by its name alone, the one before its colon: fuel, gas, steps or budget, or any name starting with fuel. Input past it is cut short with no error: derive the fuel from the input. In a law it is worse: a lemma proved over every fuel, used at a big fixed one against a goal written another way, overflows the checker's stack (bend 2.0.33/2.0.34). A literal of any size counts, 3n included. Only an argument that is the literal alone, or U32.to_nat( it ), counts, so a let-bound literal and (7n) are not seen. A def's own calls are exempt, and so is a def that returns an effect: a header with -> then the name IO (-> IO(Unit):), or one that ends in -> with IO(..): on the next line. Its fuel bounds reads, frames or retries the outside world sets (a drain of 256 datagrams a tick, a read of 100000 chunks), not the size of an input it was given.

  • tail (pedantic) — a self-call that is not a tail call, in a def whose first live parameter is a List or a String. On a long one the JS lane overflows its stack (a 48 KB header crashed a server; ~4,900 entries and ~64K elements elsewhere). Carry an accumulator. The test is on that parameter's type alone, never on whether the self-call shrinks it. Everything inside a Bool.pick(..) is skipped.

  • closed — a law in a LAWS.bend with no for/exs binder. A closed law, an equality ({lhs == rhs : T}, including IO(T)) or not, holds for the one input it names: a unit test the checker runs, not a guarantee. Nothing exempts one: quantify it, or delete it.

  • trace (project, opt-in) — SPEC.md, read from the directory bolt runs in, and the laws agree, when bolt lints the whole tree (never over files named on the line, which hold only some of the laws). A requirement table is headed exactly | ID | Requirement | Level | Status | Law | and a trust table | ID | Assumption | Why it is trusted |. An ID is uppercase letters and digits in two or more - segments (BOLT-CFG-1). A law proves one when a line of its comment block is exactly that ID. A pending row may name laws that prove part of it; they are checked as a proved row's are. A finding is a row that is not well formed, an ID listed twice, a proved row with an empty Law cell, a Trusted row with a Law cell, a Proved row's (proved or pending) <path> <law> entry that is missing, has no binder or lacks the tag, a Trusted row with no trust row, and a tag SPEC.md does not list as a Proved row, proved or pending.

  • unsafe (project) — an @unsafe def or a foreign def (a body of only import "./x.c" / import "./x.js" lines) that a LAWS.bend or PROOF.bend reaches through its relative imports, over the files bolt read. Since bend 2.0.32 such a proof fails: bend prints SOME PROOFS FAIL, then Error: N defs rely on unsafe or foreign code: and a - name list, and exits 1 (2.0.34), every def of every imported module counted. That list names the defs, not the import that brought the effect in; the finding names the import path from the law file (LAWS.bend -> mid.bend -> eff/io.bend). Move the effect into a sibling module no law file imports and pass it in as a service. Hash imports (import 0x.../path) are not followed.

  • coverage (project) — in a project that states laws (a LAWS.bend among the files bolt read), a def or a type that no law reaches. It is coverage, not law, because law is a Bend keyword: def law() is no def, so a bolt.bend could never set it by name. IO is no exemption: a def that returns IO(..) is graded like any other (a law can state an IO equality or quantify over an IO value), and so is every pure def in a module that also does IO, or that says "IO" in a comment. What is out of scope is decided by the def's name and the file's path, never by the file's text. A law names a def when it is a quantified law in a LAWS.bend and its binders or statement use the def, through the law file's import alias (Nav.text_of in lsp/LAWS.bend names text_of of lsp/nav.bend) or in the law's own file. A closed law, a law's own name, and a law outside a LAWS.bend (PROOF.bend's lemmas included) name nothing. A law reaches a def it names, and every def a reached def calls: a use on that def's lines, in its file or behind an import alias of a file in the run, so a helper that a law exercises only through its caller is covered, and one no law reaches is not. A type is covered when such a law or a reached def names it or one of its constructors (M.Sq{nn} covers type Shape with Sq{..}); naming another def of its module does not cover it, and a type reaches nothing. Out of scope: helper defs (dotted names; they still carry the reach to what they call), tests, and the law files (their defs carry it too); a dotted type is graded. main is a def: a law that names it covers it. A project without a LAWS.bend is not under law.

One binary

bolt is also bolt check file.. (the checker, bend, on each file, its errors in the same shape, path:line:1: error: message; a file bend could not be run on is path:1:1: error: could not run bend, an error like any other, never clean) and bolt lsp (the language server, over stdio). main.bend parses the command line with shake (import 0x085b03c84ca37125e38dddede7b91e55/main.bend, shake v0.2.0, its interface only) and dispatches on the selected command; a first word that names no subcommand is a file, so bolt a.bend b.bend lints those files, and with no files at all bolt lints every .bend file under the current directory (the walk in lint/plan.bend, which never descends into a hidden directory or node_modules). The lint is a pure planner, lint/plan.bend, over a World of answers, lint/world.bend, and a thin interpreter, lint.bend, that answers the planner's questions (a directory listed through walk/disk.bend, a foreign effect in dir.c and dir.js; a file read through lsp/files/) until it asks for nothing more, then prints the plan's lines and exits with its status. bolt help prints usage. A run that found errors exits 1. Bend's runtime takes its own flags out of the line before the program sees it, so bolt lsp reaches main as lsp. With no --gpu that launch is --gpu off (the cores); --gpu on or --gpu 4GB asks for the device.

In the editor

lsp runs the per-file rules on each edit and publishes the findings at the levels the nearest bolt.bend gives them: errors red, warnings yellow, off ones not at all, less what the file's noqa comments silence, then noqa's own (never on a project rule's code). A finding's code is its stable id (S003) and its source is bolt(group:slug) (bolt(style:wrap)). The project rules (coverage) need every file, so they run in bolt alone.

In the gate

Proveable claims (including IO equalities) are laws in LAWS.bend / PROOF.bend, not #| tests. tests/bare.bend is host/integration: it ends by running bolt over the whole repo and must see clean. The binary it lints with is the one it has just built from the tree under test, never whatever bolt is on the PATH: a bolt from an older release answers clean to every rule it does not implement yet, which reads exactly like a repo with nothing wrong in it.