209 lines
14 KiB
Markdown
209 lines
14 KiB
Markdown
# The checks nobody runs
|
|
|
|
Twice now a script in this repository has been quietly wrong for weeks, and both
|
|
times it was found by accident rather than by anything failing. `test/survey-x86.sh`
|
|
had two programs refused by name for about a month. `web/examples/check.sh` had been
|
|
red since September 12th. This is the inventory of everything in the tree that
|
|
asserts something and is not reached by `dune test`, what each one says today, and
|
|
what was done about the general problem.
|
|
|
|
A third failure was indeed waiting. It is the interesting one, and it is not the
|
|
failure it looked like.
|
|
|
|
## The inventory
|
|
|
|
Everything executable or fixture-shaped outside `dune test`, run rather than assumed.
|
|
|
|
| What | Verifies | Run how | State |
|
|
|---|---|---|---|
|
|
| `web/examples/check.sh` | each `web/examples/*.flan` against the `.out` beside it, plus `flan shim` on shimdemo and a killed `--dev` build of breakdemo | now `@page` | **passes**, 21 checks |
|
|
| `web/examples/quotes.sh` | every block on `index.html` that is not a program — usage text, refusal messages, the LLVM excerpt, the renderer's output, the Emacs keys — re-derived and looked for on the page | now `@page` | **was red, 11 of 42**; fixed, now passes |
|
|
| `test/survey-x86.sh` | stdout, stderr and exit status of every corpus program, x86 backend against LLVM | `@x86`, and by hand | **passes**, 103 match / 0 differ / 0 refused / 38 skip |
|
|
| `test/cells.sh` | a `--dev` build really calls through its indirection cell: an `LD_PRELOAD`ed constructor stores a different body, four builds, `22 22` against `42 42` | nothing — now `@cells` | **passes**, 4 checks |
|
|
| `tools/colon-to-dot.py --check` | every `.flan` uses the dot spelling for field labels | nothing | **reports 20 hits, all false.** See below — this one is a hazard, not a check |
|
|
| `tools/unit-return.py --check` | every `defn` states a return type, `Unit` spelled `()` | nothing | **reports 30 hits, all false.** Same hazard |
|
|
| `emacs/test-flan-dape.el` | dape driving lldb-dap sets a breakpoint from a `.flan` buffer and reports Flan frames | nothing loads it | **cannot run here** — `require 'dape` fails, dape is not installed. Its own header says it is out of `dune test` on purpose |
|
|
| `emacs/test-flan-mode.el`, `test-flan-watch.el` | indentation shapes; the watch accumulator | loaded by `test-flan-cider.el` | covered by `dune test` |
|
|
| `spike/x86/bench.sh`, `cost.sh` | nothing — they measure and print tables | by hand | measurement, not checks |
|
|
| `spike/embed/run.sh`, `merged.sh`, `sig.sh`, `symbols.sh` | nothing — sizes, startup numbers, a symbol-collision report with no exit status | by hand | measurement, not checks |
|
|
| `spike/backend/run.sh`, `spike/generics/run.sh` | nothing — they drive a spike by hand | by hand | measurement, not checks |
|
|
|
|
Recorded-output fixtures: `find . -name '*.out'` outside `_build` returns twenty
|
|
files and all twenty are in `web/examples`. There is no second family of golden
|
|
files hiding anywhere.
|
|
|
|
## The red one, and why nobody saw it
|
|
|
|
`quotes.sh` failed eleven of its forty-odd checks, and the honest account is that
|
|
**nine of the eleven were the script's fault, not the page's**. This matters, because
|
|
the obvious move — "the page is stale, update the page" — would have been wrong nine
|
|
times out of eleven and would have rewritten correct prose.
|
|
|
|
**Three were an over-wide needle.** `result`, `quoted` and `i64index` compare a
|
|
compiler message against the page. The page has them, exactly. But `flan check` grew
|
|
a source excerpt with a caret under the offending form, and the script stuffed the
|
|
whole of the output into the needle, so it was comparing three lines against a page
|
|
that quotes one. The script now takes the message and nothing else.
|
|
|
|
**Six were probes for refusals that no longer happen.** `(Vec T)`, `(Map K V)`,
|
|
`(Handle T)`, an `(Fn …)` parameter, a `defer` inside a `let`, and `break` were each
|
|
refused as "not implemented yet" when this loop was written. All six work today. The
|
|
page's "Not implemented yet" table lost their rows as each one landed — correctly,
|
|
and `acda9ed` says so in its own message — but nobody went back to the probe list.
|
|
Those six were the last thing in the tree asserting a claim the page had already
|
|
stopped making, and they are deleted, with a comment saying what the list used to
|
|
cover so the next reader is not left guessing.
|
|
|
|
**And what kept this invisible is the part worth keeping.** `flan check` answers a
|
|
program that compiles with its entire symbol table. So each of those six probes
|
|
failed by printing eighty lines of prelude signatures into a report that was already
|
|
forty lines long. The author had built a guard against false greens — the empty-needle
|
|
case, with a comment calling it the one failure the script exists to catch — and the
|
|
rot arrived instead as a **two-hundred-line unreadable red**. A check whose output
|
|
nobody can read is a check nobody reads. A clean exit is now its own one-line failure:
|
|
`this program compiles now — the page still says it is refused`.
|
|
|
|
Two failures were genuine, and both were a document that had gone stale:
|
|
|
|
**`cell load`.** The page quotes an LLVM excerpt from `flan emit --dev`. A `--dev`
|
|
`main` now pushes a condition frame before anything else, which shifted the SSA
|
|
numbering by one, so the page's `%t1 = load ptr, ptr @"flan.cell.work"` is `%t2`
|
|
today. The three quoted lines are now what the compiler prints, with the frame push
|
|
marked as elided rather than silently dropped.
|
|
|
|
**`renderer`, which is the September 12th failure again and was still there.** The
|
|
check greps `NEXT.md` (now `TODO.org`) for a line of inspector output. `NEXT.md` is a rolling scratch
|
|
document; the line was rewritten out of it, the grep went empty, the empty-needle
|
|
guard fired and said "whatever this quotes has moved" — into a report nobody was
|
|
reading. Behind that noise the page was genuinely wrong in exactly the way `check.sh`
|
|
was wrong two days ago: the colon-to-dot sweep rewrote every field label in the
|
|
corpus, `lib/render.ml` writes `.field` today and `test_repl.ml`'s fixtures are dots
|
|
throughout, and the page had been showing `(V {:x 1.5 :y 0})` for a renderer that
|
|
prints `(V {.x 1.5 .y 0})`. The page is corrected; so is the identical block in
|
|
`docs/BUILT.md`, which nothing checks and which had drifted the same way. The check's
|
|
anchor moves from `NEXT.md` (now `TODO.org`) to `test/programs/raylib-imported.flan`, which `dune test`
|
|
builds and runs, so it cannot quietly stop saying it.
|
|
|
|
The design lesson is one line: **an anchor in a rolling document is not an anchor.**
|
|
|
|
## The hazard in `tools/`
|
|
|
|
This is not a rotted check, it is worse, and it deserves its own paragraph.
|
|
|
|
`tools/colon-to-dot.py` advertises itself as re-runnable — "converting an already-
|
|
converted file is a no-op, so this can be run again over files a parallel branch
|
|
wrote in the old spelling". Run `--check` today and it reports twenty field labels to
|
|
convert across six files. Every one of them is `{:where (copyable? $t)}`, the generic
|
|
constraint clause, which is not a struct literal and names no field. The generics lane
|
|
introduced a brace form the tool has never heard of. **Running that tool for real
|
|
would corrupt `test/programs/generics.flan`, `reload-generic.flan`,
|
|
`generic-map-reject.flan`, `generic-runaway.flan`, `spike/generics/prelude-shapes.flan`
|
|
and `syntax-sketch.flan`.**
|
|
|
|
`tools/unit-return.py` has the same shape of fault. It decides whether a `defn`
|
|
already states a return type by transcribing the old `parse.ml`, and that
|
|
transcription knows the prelude's types and the builtins but not a type that arrived
|
|
through `declare-c`. So it reads `(defn v2-add [a Vector2 b Vector2] Vector2 …)` as a
|
|
function with no return type and would insert `()` in front of sixteen correct
|
|
signatures in `vendor/raylib/vector.flan`.
|
|
|
|
Neither is wired to an alias and neither should be. They are finished one-shot
|
|
migrations whose `--check` mode now reports noise, and the safe move is to delete them
|
|
or to put a line at the top of each saying they are historical and must not be re-run
|
|
without being taught `{:where}` and imported type names first. **That is the author's
|
|
call and nothing here touched them beyond reading.** It is flagged because a
|
|
destructive script sitting in `tools/` looking maintained is a worse trap than a red
|
|
test.
|
|
|
|
## What got wired
|
|
|
|
Three stanzas in `test/dune`, in the shape `@x86` established — a `rule` with an
|
|
alias rather than a `test`, because a test stanza attaches to `@runtest` and offers no
|
|
way to be attached to anything else, and with `FLAN` passed in because a script that
|
|
shells out to `dune` from inside a dune action waits on a lock it cannot get.
|
|
|
|
**`@page`** runs `check.sh` then `quotes.sh`. 42 checks, eleven seconds, five of which
|
|
is breakdemo's deliberate `timeout 5`. Its comment gives a *different* reason for being
|
|
opt-in than its three neighbours do, and the difference is the point: `@sanitize`,
|
|
`@valgrind` and `@x86` are opt-in because they are slow, and this one is not slow. It
|
|
is separate because of what a failure means. These two fail when a **document** has
|
|
gone stale, not when the compiler has regressed, and a suite that goes red because
|
|
prose drifted teaches whoever runs it to skim past red. `dune test` should mean "the
|
|
language broke". `@page` should mean "the page is lying".
|
|
|
|
**`@cells`** runs `test/cells.sh`, which was a real four-check pass/fail script
|
|
that nothing in the tree ran. It is not folded into `@x86` because it asks a different
|
|
question: the survey asks whether the backend agrees with LLVM about what a program
|
|
prints, and no program can answer this one, because a dev build starts with every cell
|
|
already pointing at the body this build compiled.
|
|
|
|
**`@checks`** is `@page`, `@x86` and `@cells` in one word.
|
|
|
|
All three scripts learned to resolve `FLAN` to an absolute path, which turned out to
|
|
be the only thing actually standing between them and a dune rule: `%{workspace_root}`
|
|
expands relative to the directory the rule is written in, and every one of these
|
|
scripts `cd`s somewhere before using it.
|
|
|
|
## Item 3: what would genuinely have caught these
|
|
|
|
The honest answer first. **There is no local mechanism with teeth, and `@checks` is
|
|
not one.** It is discoverability, not enforcement. An alias nobody types is no better
|
|
than a script nobody types; it only looks more responsible. What the umbrella buys is
|
|
that *deciding to check* and *checking everything* become the same act, so the gap
|
|
between "somebody wondered" and "everything was verified" is one command instead of
|
|
five — and five names to remember is four too many, paid every time, by whoever is
|
|
least likely to know they exist. It shortens the gap. It does not close it.
|
|
|
|
**The recommendation is `@checks` plus a written convention, and nothing else.**
|
|
`README.md` now has a "Checking it" section giving the four commands, saying which
|
|
means what, and saying plainly that nothing runs `@checks` for you. The convention it
|
|
proposes is that a lane's handoff quotes `@checks`, the way the x86 handoffs already
|
|
quote the survey's counts — which is a habit this repository demonstrably already has,
|
|
and habits that already exist are the only ones worth adding a rule to.
|
|
|
|
**Against a git hook, which is the tempting answer.** `@checks` is a couple of minutes,
|
|
nearly all of it `@x86` building every program twice. A pre-commit hook costing two
|
|
minutes gets switched off within a week, and a disabled hook is strictly worse than no
|
|
hook because it reads as coverage. A pre-push hook is cheaper in principle, because
|
|
pushing is rare — but the remote is not reachable from here and this repository's work
|
|
is merged between local worktrees, so there is no push to hang it on. There is no
|
|
`.git/hooks` content and no `core.hooksPath` today; that is a reasonable state and it
|
|
was left alone.
|
|
|
|
**What would actually have caught both failures within a day** is CI on every push,
|
|
and this repository has none. That is the real answer and it should not be dressed up.
|
|
The failure mode being defended against is not "somebody ran the check and ignored the
|
|
result" — it is "a month passed and nobody ran anything" — and only a machine that
|
|
runs without being asked fixes that.
|
|
|
|
**One thing deliberately not done, because it is the author's call.** `@page` is eleven
|
|
seconds against `dune test`'s forty-eight, and five of those eleven are a fixed sleep.
|
|
That is a quarter again on top of the suite — not free, but not the reason it is out
|
|
either — and putting it in the suite is the one move that would give it actual teeth. The argument against is the one in its comment —
|
|
that mixing "the page is lying" into "the language broke" devalues both — and that is
|
|
a judgement about what a red suite should mean, not a measurement. The number is here
|
|
so the decision can be made on it rather than on an assumption.
|
|
|
|
## Verification
|
|
|
|
- `dune test --root .` — 232 checks, 0 failures, 47s. Unchanged: nothing was added to
|
|
the default suite.
|
|
- `dune build --root . @x86` — passes. 103 match, 0 differ, 0 refused, 38 skip.
|
|
- `dune build --root . @page` — passes, 42 checks. Verified both ways:
|
|
`web/examples/hello.out` was temporarily rewritten to say `goodbye world`, the build
|
|
went red with a readable diff and exit 1, and the break was reverted. The tree is
|
|
clean.
|
|
- `dune build --root . @cells` — passes, 4 checks.
|
|
|
|
## Loose ends for the author
|
|
|
|
- The two scripts in `tools/` described above. They are live hazards and the fix is a
|
|
decision, not a patch.
|
|
- `emacs/test-flan-dape.el` cannot run on this machine and nothing loads it. It is the
|
|
one check in the inventory whose state is genuinely unknown.
|
|
- Three commits — `8bd5547`, `64e4f6c`, `0251cf4` — were on this worktree's branch and
|
|
were dropped by the reset to `dev-loop` that this lane was told to perform. They are
|
|
your own unmerged edits to `web/index.html`, `plan.org`, `NEXT.md` (now `TODO.org`)
|
|
and `lib/build.ml`,
|
|
they are unrelated to anything here, and they are still reachable by hash.
|