chore: coverage at error, the audit folded into the RFC

SPEC.md

@@ -8,7 +8,7 @@ A spec is **well-formed** when `check` reports nothing for it (SHAKE-SPEC-1). Th
 
 The words `parse` receives are what the program passes it. In a compiled program they come from `argv`, after the runtime has taken its own flags and the first `--` (SHAKE-TRUST-2).
 
-The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). Every law as it stood then, and the progress of the rollout, is in [docs/rfc/shake-law-inventory.md](docs/rfc/shake-law-inventory.md).
+The reasoning behind each requirement, the verdict of each against the code at `b93357a`, and the decisions that shaped them are in [docs/rfc/shake-spec.md](docs/rfc/shake-spec.md). The RFC also records the audit behind them and the rollout that proved every row.
 
 ## Format
 

bolt.bend

@@ -1,5 +1,5 @@
-# bolt.bend: how bolt lints this repo. Every rule is an error except
-# `coverage`, which warns until the laws exist: the gate must see no errors.
+# bolt.bend: how bolt lints this repo. Every rule is an error: the gate must
+# see no errors.
 # See bolt/config.bend for the groups and levels.
 import Base
 
@@ -15,11 +15,11 @@ def suspicious() -> String:
 def style() -> String:
   "error"
 
-# a pure def named by no quantified law: advice while the laws of
-# docs/rfc/shake-spec.md are pending. That rule is `coverage` (L001). IO,
-# which no law can reach, says so with `# noqa: L001` on its def line.
+# a pure def named by no quantified law. That rule is `coverage` (L001). A
+# def no law applies to (IO, a builder, a type alias, proof machinery, the
+# example program) says so with `# noqa: L001 <why>` on its def line.
 def laws() -> String:
-  "warn"
+  "error"
 
 # a law with no binder
 def closed() -> String:

examples/demo/main.bend

@@ -3,7 +3,7 @@ import Base
 import ../../main.bend as Shake
 
 # the program spec
-def spec() -> Shake.Cli:
+def spec() -> Shake.Cli:  # noqa: L001 the example program, not the library
   Shake.app("demo", "A tiny command-line program.", Some{"0.1.0"},
     [Shake.flag("verbose", Some{"v"}, Some{"verbose"}, "More output")],
     [
@@ -44,7 +44,7 @@ def greet.tags(tags: List<&2, String>) -> IO(Unit):
       IO.print("tags: " ++ String.join(hh <> tt, " "))
 
 # the value bound to `name`, or "" when nothing bound it
-def text(+mm: Shake.Matched, +name: String) -> String:
+def text(+mm: Shake.Matched, +name: String) -> String:  # noqa: L001 the example program, not the library
   Maybe.default(&2, String, Shake.get(mm, name), "")
 
 # a successful greet: `who` when given, else `--name`, which has a default;

main.bend

@@ -18,11 +18,11 @@ def Cli() -> Data:
   S.Cli
 
 # a nested command
-def Sub() -> Data:
+def Sub() -> Data:  # noqa: L001 a type alias of the interface
   S.Sub
 
 # one argument: a flag, an option, a positional or a rest positional
-def Arg() -> Data:
+def Arg() -> Data:  # noqa: L001 a type alias of the interface
   S.Arg
 
 # a successful parse, one command at a time: the bindings the command made,
@@ -35,7 +35,7 @@ def ParseErr() -> Data:
   S.ParseErr
 
 # one way a spec contradicts itself
-def SpecErr() -> Data:
+def SpecErr() -> Data:  # noqa: L001 a type alias of the interface
   K.SpecErr
 
 # a program: name, about, optional version, top-level args and commands
@@ -49,7 +49,7 @@ def app(
   S.app(name, about, version, args, subs)
 
 # a nested command
-def sub(
+def sub(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   +about: String,
   args: List<&2, S.Arg>,
@@ -58,7 +58,7 @@ def sub(
   S.sub(name, about, args, subs)
 
 # a boolean flag
-def flag(
+def flag(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   short: Maybe<&2, String>,
   long: Maybe<&2, String>,
@@ -67,7 +67,7 @@ def flag(
   S.flag(name, short, long, help)
 
 # a valued option
-def opt(
+def opt(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   short: Maybe<&2, String>,
   long: Maybe<&2, String>,
@@ -80,7 +80,7 @@ def opt(
 
 # an option that may be given more than once; `get_all` reads every value, in
 # order, and `get` the last
-def many(
+def many(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   short: Maybe<&2, String>,
   long: Maybe<&2, String>,
@@ -92,7 +92,7 @@ def many(
   S.many(name, short, long, help, required, default, choices)
 
 # a positional
-def pos(
+def pos(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   +help: String,
   required: Bool,
@@ -102,7 +102,7 @@ def pos(
   S.pos(name, help, required, default, choices)
 
 # a rest positional: every leftover word, as one name
-def rest(
+def rest(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   +help: String,
   required: Bool,

src/LAWS.bend

@@ -2765,3 +2765,30 @@ law word_used:
   for h_live: {Grow.gw.live(st) == True{} : Bool}
   for h_same: {S.parse.step(tok, st) == st : S.St}
   Empty
+
+# the command path a report of `check` is at
+def spec_path(err: K.SpecErr) -> List<&2, String>:
+  match err:
+    case K.RestNotLast{path, _n}:
+      path
+    case K.SameName{path, _n}:
+      path
+    case K.SameShort{path, _s}:
+      path
+    case K.SameLong{path, _l}:
+      path
+    case K.SameSub{path, _n}:
+      path
+    case K.HelpSub{path}:
+      path
+    case K.DefaultNotChoice{path, _n, _v}:
+      path
+    case K.RequiredAfterOptional{path, _n}:
+      path
+
+# LAW: the text of every report of `check` says first where it is: `spec: `
+# at the root, else the command's path (a lemma for SHAKE-SPEC-1's reports)
+law spec_err_where:
+  for +err: K.SpecErr
+  exs msg: String
+  {Shake.spec_err_text(err) == K.at(spec_path(err)) ++ msg : String}

src/PROOF.bend

@@ -9652,3 +9652,22 @@ def Laws.word_used(tok, st, h_live, h_same):
           nu.need_w(S.looks_flag(tok), nn, tok, args, up, subs, path, binds, pos, raw, seen, S.Need{nn}, {==}, h_same)
         case S.Free{}:
           nu.rawf(raw, tok, args, up, subs, path, binds, pos, seen, S.Free{}, {==}, {==}, {==}, h_same)
+
+def Laws.spec_err_where(err):
+  match err:
+    case K.RestNotLast{+path, +name}:
+      ("rest positional '" ++ name ++ "' is not the last positional", {==})
+    case K.SameName{+path, +name}:
+      ("two arguments are named '" ++ name ++ "'", {==})
+    case K.SameShort{+path, +short}:
+      ("two arguments are spelled '-" ++ short ++ "'", {==})
+    case K.SameLong{+path, +long}:
+      ("two arguments are spelled '--" ++ long ++ "'", {==})
+    case K.SameSub{+path, +name}:
+      ("two subcommands are named '" ++ name ++ "'", {==})
+    case K.HelpSub{+path}:
+      ("a subcommand is named 'help', which `parse` keeps for help", {==})
+    case K.DefaultNotChoice{+path, +name, +value}:
+      ("the default '" ++ value ++ "' of '" ++ name ++ "' is not one of its choices", {==})
+    case K.RequiredAfterOptional{+path, +name}:
+      ("required positional '" ++ name ++ "' follows an optional one", {==})

src/cli.bend

@@ -118,7 +118,7 @@ def app(
   Cli{name, about, version, args, subs}
 
 # a nested command
-def sub(
+def sub(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   +about: String,
   args: List<&2, Arg>,
@@ -127,7 +127,7 @@ def sub(
   Sub{name, about, args, subs}
 
 # a boolean flag
-def flag(
+def flag(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   short: Maybe<&2, String>,
   long: Maybe<&2, String>,
@@ -136,7 +136,7 @@ def flag(
   Arg{name, short, long, Flag{}, help, False{}, None{}, []}
 
 # a valued option
-def opt(
+def opt(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   short: Maybe<&2, String>,
   long: Maybe<&2, String>,
@@ -148,7 +148,7 @@ def opt(
   Arg{name, short, long, Opt{}, help, required, default, choices}
 
 # an option that may be given more than once; `get_all` reads every value
-def many(
+def many(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   short: Maybe<&2, String>,
   long: Maybe<&2, String>,
@@ -160,7 +160,7 @@ def many(
   Arg{name, short, long, Many{}, help, required, default, choices}
 
 # a positional
-def pos(
+def pos(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   +help: String,
   required: Bool,
@@ -170,7 +170,7 @@ def pos(
   Arg{name, None{}, None{}, Pos{}, help, required, default, choices}
 
 # a rest positional: every leftover word, as one name
-def rest(
+def rest(  # noqa: L001 a builder: its result is the Arg or Sub it names, nothing to state
   +name: String,
   +help: String,
   required: Bool,
@@ -1393,57 +1393,6 @@ def parse.finish(st: St) -> Result<&2, &2, ParseErr, Matched>:
 def parse(app: Cli, argv: List<&2, String>) -> Result<&2, &2, ParseErr, Matched>:
   parse.finish(parse.walk(argv, parse.start(app)))
 
-# a ParseErr as a short tag
-def show.err(ee: ParseErr) -> String:
-  match ee:
-    case UnknownFlag{_at, word}:
-      "unknown " ++ word
-    case Missing{_at, name}:
-      "missing " ++ name
-    case NoValue{_at, name}:
-      "novalue " ++ name
-    case BadValue{_at, name, value}:
-      "bad " ++ name ++ " " ++ value
-    case NeedHelp{path}:
-      "help " ++ String.join(path, " ")
-    case Unexpected{_at, arg}:
-      "unexpected " ++ arg
-    case Repeated{_at, name}:
-      "repeated " ++ name
-
-# one bind as `name=value`
-def show.bind(bb: Bind, +rest: String) -> String:
-  Bind{n, v} = bb
-  n ++ "=" ++ v ++ Bool.pick(String, String.is_empty(rest), "", " " ++ rest)
-
-# the bindings as `name=value` words
-def show.binds(bs: List<&2, Bind>) -> String:
-  match bs:
-    case Nil{}:
-      ""
-    case Con{+h, t}:
-      show.bind(h, show.binds(t))
-
-# each command's bindings, root first, `; ` between commands
-def show.levels(mm: Matched) -> String:
-  match mm:
-    case Leaf{bs}:
-      show.binds(bs)
-    case Node{bs, _n, next}:
-      show.binds(bs) ++ "; " ++ show.levels(next)
-
-# a Matched as `path | binds`
-def show.matched(+mm: Matched) -> String:
-  String.join(path_of(mm), "/") ++ " | " ++ show.levels(mm)
-
-# a parse result as a single line
-def show(rr: Result<&2, &2, ParseErr, Matched>) -> String:
-  match rr:
-    case Fail{e}:
-      "err " ++ show.err(e)
-    case Done{m}:
-      "ok " ++ show.matched(m)
-
 # the short/long label of an option, plus a metavar for Opt
 def help.label.kind(kk: ArgKind, +name: String, +label: String) -> String:
   match kk:

src/eq.bend

@@ -10,7 +10,7 @@ law bool_cmp_self:
   {Bool.cmp(bb, bb) == EQ{} : Cmp}
 
 # the two bits, each compared with itself
-def bool_cmp_self(bb):
+def bool_cmp_self(bb):  # noqa: L001 a proof of this file's law
   match bb:
     case False{}:
       {==}
@@ -24,7 +24,7 @@ law word_cmp_self:
   {Word.cmp(nn, ww, ww) == EQ{} : Cmp}
 
 # by induction on the width: a word of no bits and a bit carried over one
-def word_cmp_self(nn, ww):
+def word_cmp_self(nn, ww):  # noqa: L001 a proof of this file's law
   match nn:
     case 0n:
       match ww:
@@ -45,7 +45,7 @@ law u32_cmp_self:
   {U32.cmp(uu, uu) == EQ{} : Cmp}
 
 # a number is a word of thirty-two bits, so the word's law answers for it
-def u32_cmp_self(uu):
+def u32_cmp_self(uu):  # noqa: L001 a proof of this file's law
   match uu:
     case U32{+ww}:
       word_cmp_self(32n, ww)
@@ -56,7 +56,7 @@ law char_cmp_self:
   {Char.cmp(cc, cc) == ((cc, cc), EQ{}) : (Char & Char) & Cmp}
 
 # a char is a code point, and the pair it is compared inside rides along
-def char_cmp_self(cc):
+def char_cmp_self(cc):  # noqa: L001 a proof of this file's law
   match cc:
     case Chr{+xx}:
       Equal.cong(Cmp, (Char & Char) & Cmp, rr => ((Chr{xx}, Chr{xx}), rr),
@@ -69,7 +69,7 @@ law string_cmp_self:
 
 # by induction on the string: the head's law and the tail's, composed the
 # way String.cmp composes them
-def string_cmp_self(ss):
+def string_cmp_self(ss):  # noqa: L001 a proof of this file's law
   match ss:
     case SNil{}:
       {==}
@@ -91,6 +91,6 @@ law string_eq_self:
   {String.eq(ss, ss) == True{} : Bool}
 
 # equality is the comparison read as a bit, so the comparison's law answers
-def string_eq_self(ss):
+def string_eq_self(ss):  # noqa: L001 a proof of this file's law
   Equal.cong((String & String) & Cmp, Bool, rr => String.eq.fin(rr),
     String.cmp(ss, ss), ((ss, ss), EQ{}), string_cmp_self(ss))

src/grow.bend

@@ -11,7 +11,7 @@ import ./cli.bend as Shake
 import ./eq.bend as Eq
 
 # the bindings a walker holds for its current command
-def binds_of(st: Shake.St) -> List<&2, Shake.Bind>:
+def binds_of(st: Shake.St) -> List<&2, Shake.Bind>:  # noqa: L001 proof machinery
   Shake.St{_m, _a, _g, _s, _p, bb, _o, _r, _n} = st
   bb
 # `big` is `small` with some bindings put in front
@@ -566,7 +566,7 @@ def gw.Stuck(big: Shake.St) -> Type:
   {gw.live(big) == False{} : Bool}
 
 # the three things a word does to a walker
-type Moved<-A: Type, -B: Type, -C: Type> is Type:
+type Moved<-A: Type, -B: Type, -C: Type> is Type:  # noqa: L001 proof machinery: what a step did, for the walker proofs
   Stays{proof: A}
   Enters{proof: B}
   Stops{proof: C}
@@ -1159,7 +1159,7 @@ def gw.stuck_walk(more, st, hh):
       gw.stuck_walk(tt, Shake.parse.step(ww, st), gw.stuck_step(ww, st, hh))
 
 # a walk either grows the walker or leaves it stuck
-type Went<-A: Type, -B: Type> is Type:
+type Went<-A: Type, -B: Type> is Type:  # noqa: L001 proof machinery: what a walk did, for the walker proofs
   Grew{proof: A}
   Stopped{proof: B}