[M3-2c] The evidence strip: computed counts, each linking to its proof (#95) - #108
Conversation
1f314a1 to
396f833
Compare
There was a problem hiding this comment.
Pull request overview
Adds a build-time “evidence strip” to the home page that displays four computed measures (modules, Agda LOC in code fences, postulates, third-party requests), with each figure linking to its supporting proof/audit source and (optionally) animating a count-up when motion is allowed.
Changes:
- Introduces a Python counter (
count_evidence.py) that generates committeddocs/assets/evidence.jsonfrom anagda-algebrascheckout. - Adds an MkDocs hook (
evidence_hook.py) that expands<!-- evidence-strip -->into the rendered strip using the committed JSON. - Adds styling + a small JS count-up animation controlled by the
--motion-counttoken, and wires the hook/script intomkdocs.yml/Makefile.
Reviewed changes
Copilot reviewed 13 out of 13 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| scripts/python/evidence_hook.py | New MkDocs hook that renders the evidence strip HTML from committed JSON |
| scripts/python/count_evidence.py | New script that counts modules/LOC/postulates and emits evidence JSON |
| mkdocs.yml | Registers the hook and includes the evidence count-up JS |
| Makefile | Adds make evidence AA=... target to regenerate the committed JSON |
| docs/stylesheets/tokens.css | Adds --motion-count timing token |
| docs/stylesheets/extra.css | Adds evidence strip layout/typography/link styling |
| docs/javascripts/evidence.js | Adds IntersectionObserver-driven count-up animation |
| docs/index.md | Adds the <!-- evidence-strip --> marker to the home page |
| docs/assets/evidence.json | Adds the committed evidence data consumed by the hook |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| def _render(data, page, files): | ||
| cells = [] | ||
| for m in data["measures"]: | ||
| classes = "ev-n ev-zero" if m.get("emphasis") and m["value"] == 0 else "ev-n" | ||
| cells.append( | ||
| f'<a class="ev" href="{_href(m["href"], page, files)}" ' | ||
| f'title="{m["command"]}">' | ||
| f'<span class="{classes}" data-n="{m["value"]}">{m["value"]:,}</span>' | ||
| f'<span class="ev-l">{m["label"]}</span>' | ||
| f'<span class="ev-d">{m["detail"]}</span>' | ||
| f"</a>" | ||
| ) | ||
| src = data["source"] | ||
| commit = src["commit"][:7] | ||
| caption = ( | ||
| f'<p class="ev-caption">Counted, not asserted: the library figures are ' | ||
| f'from <a href="{src["repo"]}">ualib/agda-algebras</a> at ' | ||
| f'<code>{commit}</code> ({src["commit_date"]}), the request count from ' | ||
| f"this site's own audit. Hover a figure for the command that produced " | ||
| f"it; <code>make evidence</code> recounts.</p>" | ||
| ) | ||
| return '<div class="evidence">' + "".join(cells) + "</div>\n" + caption |
There was a problem hiding this comment.
Taken (fd7f74f): every interpolated field now goes through html.escape — the resolved href, title, label, detail, and the caption's repo/commit/date — and value is normalized with int() once, so the zero-emphasis test, data-n and the printed figure cannot disagree about type. The JSON is first-party and committed, so the practical risk was invalid markup more than XSS, but the fix is the same either way.
| def agda_lines(path: Path): | ||
| """The lines inside ```agda fences of one literate module.""" | ||
| lines, in_fence = [], False | ||
| for line in path.read_text(encoding="utf-8").splitlines(): | ||
| if in_fence: | ||
| if line.startswith("```"): | ||
| in_fence = False | ||
| else: | ||
| lines.append(line) | ||
| elif line.startswith("```agda"): | ||
| in_fence = True | ||
| return lines |
There was a problem hiding this comment.
Tested rather than argued, and not taken — with the numbers to show why. A differential run at the counted commit (ualib/agda-algebras@594bc1c, all 370 modules) compared three matchers: the committed column-0 one, an indent-tolerant \s*+fence variant, and a maximally lenient reading of the md_begin/md_end regexes in Agda's own Literate.hs.
Results: the corpus contains zero indented agda-tagged fences, and column-0 vs indent-tolerant agree line for line — 65,459 lines, 0 postulates, byte-identical JSON. The lenient reading would add 203 lines across 10 files, and inspecting them shows ASCII diagrams and paragraph prose around display blocks (e.g. the indented fence at src/Setoid/Terms/Translation.lagda.md:46). So loosening this matcher inflates the count with lines nothing type-checked — the one failure mode the strip exists to rule out. Undercounting-by-strictness is the acceptable tail; overcounting is not.
The counter now records this as a checked assumption rather than a silent one (fd7f74f): agda_lines documents the reasoning, and exits loudly if a future commit of the corpus introduces an indented opening fence or an indented bare fence inside an open block — so the assumption breaking kills the recount instead of shipping a quietly wrong number.
df07998 to
4943776
Compare
396f833 to
1fc85d7
Compare
Four measures under the hero -- 370 Agda modules (370 of 370 --safe), 65,459 lines of Agda, 0 postulates, 0 third-party requests -- each a link to the thing that can check it, with the producing command in its tooltip and the counted commit in the caption. count_evidence.py counts from an agda-algebras checkout: modules, the lines inside code fences only (prose in a literate module is not code), and line-leading `postulate` occurrences, corroborated by the --safe pragma count. Definitions and theorems are deliberately not counted: a grep cannot defend the distinction, and an indefensible number is worse than none. The output is committed as docs/assets/evidence.json, so the build needs no checkout and no network; `make evidence AA=...` is the deliberate recount. evidence_hook.py renders the strip from the JSON (one renderer, so a displayed number and its recorded command cannot drift); internal hrefs resolve through the files collection so a moved page fails the build. The final numbers ship in the HTML; evidence.js adds only the count-up, gated on prefers-reduced-motion, with its duration read from the --motion-count token (ADR-009: timing lives in tokens.css). Part of #95. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Copilot's escaping point is taken: every field of evidence.json that crosses into the strip's markup now goes through html.escape, and the value is normalized with int() once, so the zero test, data-n and the printed figure cannot disagree about type. The JSON is first-party and committed, so the practical risk was invalid markup more than injection, but the fix is the same either way. The unquoted $(AA) in the evidence target is quoted, taken as read. The third point -- that column-0 fence matching could undercount indented ```agda blocks -- was tested rather than argued: a differential run at the counted commit (594bc1c), three matchers over all 370 modules, found zero indented fences and zero difference between column-0 and indent-tolerant counting; the hardened counter reproduces the committed JSON byte for byte. A maximally lenient reading of the fence regexes in Agda's own Literate.hs would add 203 lines, and inspection shows those are ASCII diagrams and prose around display blocks -- exactly the inflation the strip promises not to commit. So column-0 stays, now as a checked assumption: agda_lines documents the reasoning and exits loudly on any indented fence a future corpus commit might introduce. Part of #95. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
4943776 to
fd7f74f
Compare
What
Four measures under the hero, counted rather than asserted:
370 Agda modules (370 of 370 carry
--safe) · 65,459 lines of Agda (code fences only) · 0 postulates · 0 third-party requestsEach cell links to what can check it (the library repo; the site's audit docs), carries the producing command in its tooltip, and the caption names the exact commit the numbers were counted from (
ualib/agda-algebras@594bc1c, 2026-08-01).make evidence AA=/path/to/agda-algebrasrecounts.Stacked on #107 (base
94-m3-2b-constellation); merge order #106 → #107 → this.Honesty decisions, recorded
.agdaiinterfaces lands later it can join the strip.--safe(which rejects postulates) is verified per-module, and the request count is the offline audit's, linked to the Checks section that explains it.evidence.js, ~50 lines, no deps) runs only when motion is allowed and IntersectionObserver exists; its duration is read from the new--motion-counttoken per ADR-009. Crawlers, JS-off, and reduced-motion readers see the real values with nothing missing.Mechanics
count_evidence.py→ committeddocs/assets/evidence.json(build needs no network);evidence_hook.pyrenders the strip following therecent_posts_hook.pypattern, and resolves internal hrefs through the files collection so a moved target fails the build rather than shipping a dead link.make evidenceis idempotent against an unchanged checkout (verified — second run produced no diff).Verified
mkdocs build --strictgreen;make design-auditgreen (50 pages × 2 themes, AA everywhere, all same-origin, no font substitution).Part of #95.
🤖 Generated with Claude Code