Repository navigation
Conversation
…im the library table, name headings
Four problems found by reading /atlas and /atlas/7713 over the real smoke-2 store
(331 passages, 10 articles).
Capped quotes. The export quotes at most a passage's first 12 words (proposal
§2.7 and §10, the verbatim-quotation cap), so 322 of smoke 2's 331 quotes stop
mid-sentence with nothing saying so. The builder now stores quote_capped per
passage: a quote under 12 words is whole, and a 12-word quote is whole exactly
when its sha256 equals the record's span_sha256 (the producer's sha of the whole
passage span; read, never required). The page puts an ellipsis outside the
quotation, after the highlight in the card and after the closing quotation mark
in the Subject row, with "(the passage continues)" for screen readers, and a note
under Passages. The quote stays verbatim. Two of smoke 2's whole passages are
exactly 12 words, which a word count alone would have cut.
Central statements. 204 of 331 passages are supporting (worked examples, setup
sentences) and set the headline of the bar over all passages. The Coverage box
and the dashboard's Totals add a "Central statements" line, the subject and
central passages by status, beside that bar, which stays. The article page counts
its passages' prominence; the dashboard reads the new counts.by_prominence in
current.json, which sums the new summary.by_prominence of each article.
Library table. The dashboard listed all 48 universe libraries by id, 39 of them
all zeros. Rows are now the libraries holding a passage or a related declaration,
by passages, then complete locations, then name; the rest are named with their
commits in a <details> below the table. The article page's Where row already
shows only libraries with a location or a related declaration, so it is unchanged.
Headings. A passage heading's pieces are flex items and the section's "§ " is CSS
content, so its accessible name ran together ("Theorem · centralStatement" where
generated content is not read). A visually hidden " · " (the existing atlas-sr
class) now separates them.
Store: quote_capped and the by_prominence counts are optional fields added within
v1 (schema strings unchanged); the Worker falls back for older stores (a word
count for quote_capped, no dashboard line without counts.by_prominence), and
docs/ATLAS.md section 4 now states that rule. The fixture models both 12-word
cases with real span shas, and the golden store is regenerated. Rebuilt with this
builder, the smoke-2 store differs from the old one only by the new fields.
site/assets/atlas.css and atlas.js are unchanged (byte-identical to 8b219e2), so
their asset versions stay. Atlas pages remain outside the render cache.
…ix ends, the central line's place and words Fixes the two reviews of 6c227f7. Builder (build_store.quote_extent, replacing quote_capped's body): - The export right-strips the quote but hashes the span as it is, so a whole 12-word passage whose span ends in whitespace was marked as a cut head. 29 of the 21,755 paragraphs of the producer's wpm source set end that way (23 in a hair space, 5 in a space and a no-break space, 1 in a no-break space). A quote at the cap is now whole when span_sha256 is the sha of the quote followed by no whitespace or by any run of one or two whitespace characters (every str.isspace character); a longer run still reads as a head, the safe side. - A capped head's suffix is taken from the page, not the passage, so it can hold the passage's end. The builder now finds that end (span_sha256 against the quote plus the suffix's first characters, or the whole suffix and a whitespace run) and stores passage_ends_in_suffix, a new optional v1 field; the card then shows no "(the passage continues)" after a suffix that reaches the passage's end, while the Subject row, which shows the quote alone, keeps its ellipsis. - Records of one passage must agree on span_sha256, as on every other passage field, so record order can no longer decide the ellipsis. A set without span_sha256 still builds. Smoke 2 rebuilt: 322 heads as before, 0 suffix ends, and no other difference than the new field. The golden store is regenerated. Pages: - An ellipsis after a quote now means only that the passage continues: a suffix is context and no longer trails off with its own "…", which the note under Passages would otherwise have described wrongly. The note reads "Quotes show at most the first 12 words of a passage. A … after the highlighted quote means the passage continues; “Read it in context on Wikipedia” shows the rest." - The article's central-statements line moves after the Status row (the bar's legend) and before the Where row, so the first figures under the bar are the bar's, as on the dashboard. It now says what it counts and what it leaves out: "Central statements: 19 of the 37 passages state the article's subject or a named result or definition; the other 18 are supporting (examples, setup). Of these 19: ✓8 formalized, ◔9 partial, ✕2 not formalized." (the dashboard adds "across 10 articles"). Its commas are elements, so the summary box's .atlas-mini + .atlas-mini margin no longer widens the gap after each one or indents a wrapped line. - The dashboard's list of empty libraries follows the table's column notes, which now sit right under the table (and are left out when there is no table). - With no universe object (the route passes null when it cannot read one), the by-library rows come from counts.by_library under their ids, so the page no longer says that no library holds anything when the counts say otherwise. Checked over the smoke-2 store at 1280, 375 and 320px in both themes: axe finds no violations, nothing scrolls sideways, the line sits between Status and Where. site/assets/atlas.css and atlas.js are unchanged (byte-identical to 8b219e2). Atlas pages remain outside the render cache.
…ys and F5's span, with quote_capped #85's key checks at record level, subject end and lean end stay as they are; #103's quote_capped, passage_ends_in_suffix and by_prominence are store fields and pass them. quote_extent now takes F5's span as a shortcut (tail = (end - start) - len(exact)) and falls back to the span_sha256 search only for a tail one or two characters past the suffix. span_sha256 is now required, so #103's "a set without it builds" test is gone; #85's span test compares a set with spans against the same set without them, and new tests check the shortcut against the hash path case by case and on the fixture.
…sage In quote_extent's fallback zone (a span tail one or two characters past the suffix) the hash decided alone, so inconsistent producer data could show a provably cut passage as whole: the span covered a suffix with words in it while span_sha256 hashed the bare quote. Such a span now caps the quote whatever the hash says; a whitespace-only suffix proves nothing and the hash still decides. ATLAS.md section 4 states the rule; the smoke sets are unchanged (322 capped).
…ository, keyed by id Two conflicts. make_fixture's absence keeps #103's subject(source_id, quote, layout) and takes #85's ends, one per distinct (repo, commit), which for the fixture's distinct repositories are the same bytes. docs/ATLAS.md section 4 keeps #85's sentence that every library in the view model is a library id, followed by #103's quote_capped and passage_ends_in_suffix notes. The rest merged cleanly: #103's dashboard (held libraries by passages, the others listed below the table) reads the names libraryViews now gives, so libraries split from one repository are "Lean core · Init" and "Lean core · Std" there too. test_build_store passes (110 tests), as do wiki/test/atlas.test.ts and the typecheck. The smoke-2 sets d1, d1c and d1e and brain4's unsplit e2e set build byte for byte the stores the pre-merge builder built; brain4's split-universe e2e set, which it refused, builds.
Owner
Author
|
Verdict: merge after #85 lands and release B is promoted, once this PR targets main and CI has run there. Nothing blocks merge. Two static reviews, one of correctness and one of the claims against the diff and CI, looked at the diff from #85's head (7288b96). Two refuters checked the substantive finding.
Notes (none blocks merge):
Posted by Claude Code (AutoformBot "Merge Currently Open PRs 4" session). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #85. Its base is
claude/formalization-atlas, so GitHub retargets it tomainwhen #85 merges.I viewed
/atlasand the article pages locally (the e2e harness, loopback only) with the real smoke-2 store: 10 Tier A articles, 331 passages, record set39ce722d. Four problems showed up, and this PR fixes them.quote_cappedandpassage_ends_in_suffix, using the record'sspan_sha256(the hash of the whole passage). The page puts a muted "…" after the quote, outside the highlight and outside the quotation marks, plus screen-reader text "(the passage continues)". Whole passages, including 12-word ones and ones whose span ends in whitespace, get no ellipsis.summary.by_prominence/counts.by_prominence. This is an additive v1 field, and older stores fall back.<details>with their commits..atlas-srclass, fixes it.site/assets/atlas.cssandatlas.jsare byte-identical to #85. The release-B attestation in #99 stays valid, and no?v=bump is needed. Atlas pages are still not render-cached.Tests: 1,168 Worker tests, 104 Python commands (98 builder tests) and 24 Playwright tests, 16 of them atlas, with axe at 375px. A review pass covered correctness and reader wording, and all of its findings are fixed here except one 0px gap that would need CSS.
A deployed store must be rebuilt with this builder to carry the new fields. Until then the page treats every 12-word quote as cut, and the dashboard omits the central line.