test: make the suites capable of failing — and fix the 19 lexer defects that exposed

[hyperpolymath]

Foundation work, breadth-first, before any axiom is discharged — per the standing
"firm foundation, breadth before depth" directive.

The problem: nothing here could be verified by running it

Every proof-debt item was unfalsifiable in practice, because four layers of the base were
soft, and each hid the next:

1. lake test reported "no test driver configured" — none existed.
2. The suites printed FAIL/✗ and then printed "All tests passed!" unconditionally,
   with main : IO Unit, so the process always exited 0. LexerTest even documented a
   counter — "Count of test failures, tracked via IO.Ref" — that was never implemented.
3. test/TypeSafetyTests.lean was declared by no Lake target, so it was never built.
   It had rotted and no longer compiled.
4. lake build only builds the default target (the GqlDt library), so the test
   executables were never compiled by CI either. lexer_test had also rotted.

What that was hiding: 19 real lexer defects

Once the suites could fail, lake test immediately went red with 19 failures — all
genuine spec-conformance bugs, all from one off-by-one.

LexerState.peek takes an offset where 0 means the current character (s.peek 0 ≡
s.curr; the default is 1). All seven two-character lookahead sites passed 0, so every
one compared the character it already held against the character it expected next. The
branches were all present and correct — none could ever be taken.

Input	Was	Should be	Spec
<= >= != <>	[opLt, opEq] etc.	one token each	operator table, prec 5
:	opDoubleColon (advancing twice)	opColon	:: is cons (prec 6), : is type annotation
-	no token at all	opMinus	swallowed as a -- line comment
/* b */	[/, *, b, *, /]	skipped	§8.2 C-style block comments

Fix: peek 0 → peek 1, seven sites. 19 failures → 0.

One of the 19 was a genuine test bug rather than a lexer bug: schema::table expected
three identifiers, but table is a reserved SQL keyword and keywords are case-insensitive,
so it correctly lexes as .kwTable — as this same suite asserts elsewhere. The
qualified-identifier case now uses a non-reserved name, and the keyword interaction is
asserted explicitly rather than left as a latent contradiction between two tests.

What landed

test/TestHarness.lean (new) — the failure counter LexerTest's comment promised, plus
summarise, which turns the tally into a process exit code. All four suites now record
failures and return IO UInt32; ParserTest's 18 ✗ sites were printing to stdout and
returning Unit, and now record. The unconditional "All tests passed!" banners are gone.

lakefile.lean — lean_lib TestSupport (so suites can import the harness),
lean_exe type_safety_test (previously unbuildable), and a @[test_driver] script test.
ffi_test is deliberately excluded: it links liblith_bridge.a and is covered by the
zig-ffi job, so including it would make lake test fail on a clean checkout for a non-Lean
reason.

Compile fixes needed just to get the rotted suites building: String.containsSubstr
doesn't exist in Lean 4.15 (all three probes test single characters, so String.contains
is right); TypeSafetyTests didn't open Prompt/Provenance, passed a NonEmptyString
where insertEvidence wants a Provenance.Rationale, and passed BoundedNat's min/max as
data when they are structure parameters — plus its main sat inside a namespace, so
the linker found no entry point.

Governance files (your call (b)) — the five sweep4 files, rewritten rather than
replayed. The sweep version named @metadatastician (owns other estate repos, not this
one), and its ARCHITECTURE.md described a src/ tests/ config/ layout this repo does not
have. Replaced with the real structure, the build order, and a verification-posture table.
GOVERNANCE.md records the rules a change must clear, each traced to a specific past
failure rather than asserted as principle.

Verification

lake test  →  exit 0, 163 checks, 3 suites green

Canary-tested both directions, because a gate that has never gone red is not evidence
of anything: seeding firstType "SELECT" == some .kwDelete turns lake test red
(exit 1, Lexer: 1 check(s) FAILED); removing it returns exit 0.

READMEs corrected. ✅ Lexer: … operators, literals, comments was false when written;
it is now true, and verified by 163 executable checks rather than asserted.

Not in this PR

flake.nix removal (your call (c)) is deliberately held. The estate package policy is
"Guix primary (guix.scm), Nix fallback (flake.nix). A repo satisfying neither is the
violation." This repo has no guix.scm, so flake.nix is currently the only artefact
satisfying it — removing it turns Governance red. Writing a guix.scm instead would mean
committing a file I cannot execute (guix isn't installed here), which is the handwaving the
doctrine forbids. Raised rather than guessed.

The 16 axioms are untouched. This PR only makes the ground firm enough to stand on.
docs/proof-debt.md D3 is additionally gated on the arithmetic-vs-geometric mean decision,
since PromptScores.overall_correct welds the averaging rule into a proof field.

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved 1 resolved / 1 findings

Adds executable test suites and fixes 19 off-by-one lexer lookahead defects, but the lake test driver script still fails to build the required test executables.

✅ 1 resolved

✅ Bug: lake test driver never builds the test executables

📄 lakefile.lean:20-23 📄 lakefile.lean:44-58 📄 lakefile.lean:70-84
The @[test_driver] script test only runs pre-built binaries under .lake/build/bin/, but nothing builds them: the three test executables (lexer_test, parser_test, type_safety_test) are not @[default_target] (only lean_lib GqlDt is), and the CI workflow runs lake build (default target only) before lake test. On a clean checkout/CI the binaries do not exist, so the driver prints ✗ … binary not found, pushes every suite into failed, and returns 1 — and the workflow's else-branch turns the job red with ::error::lake test failed. The claimed lake test → exit 0 only holds locally where the suites were built manually, so the very gate this PR introduces is broken in CI. Either build the suites inside the driver, mark them as default targets, or add an explicit lake build lexer_test parser_test type_safety_test step to CI.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}