[Deicyde]

Part of making the published site read well: the landing page's dashboard, in the reading pane's home view. It adds no command, flag, JSON key or schema, and no test pins skill wording.

Problem

• "Ready to start" was plain text. On ATLAS it read "7213" with no way to see those statements. It was also one letter from the status "ready to state".
• Counts appeared twice, or wrong:
  • a "Topics" figure read 0 next to the topic rail;
  • a hidden kicker, bar and inventory figure still shipped;
  • figures had no thousands separators ("21722 of 28979 articles"), while the map's cards read "5,332 of 9,056";
  • the noun was "articles" here, "statements" in Browse and "results" in the list heading.
• Colour that wasn't status. A brand gradient filled the figures, the progress bar and a header hairline, reusing status blues and a violet close to "conditionally proved".
• A dependency summary with an empty side. It read "Uses 0 · Used by 2".
• A hidden coverage line. The landing never showed what its sources cover.

Change

• The ready figure:
  • it is called "Ready to work on";
  • it links to the contents page's list view filtered to ready statuses, roadmap/index.html#view=list&status=can_state,can_prove, a route the explorer already accepts;
  • at zero it reads "Nothing is ready right now", with no link.
• Counts:
  • each count on the landing shows once, in "statements", with thousands separators (a chapter's progress strip is unchanged);
  • the Topics figure and the hidden markup are gone;
  • when there are no statements yet, or every statement is fully proved, one sentence replaces the figures.
• "Start reading →" sits right after the lead.
• Less decoration. The brand gradient is off the figures, the bar and the header hairline, and its token and the unused violet and magenta tokens are gone. Light mode's link and hover blues still equal the can_prove and can_state strokes, and the logo keeps its gradient.
• Dependency summary leaves out its empty side and separates thousands.
• Coverage line shows in plain words, for example "7 source areas: 1 split into statements · 5 not yet settled · 1 out of scope", linking to the coverage contract.
• Reading measure. In the reading pane, running text keeps the 72ch measure, while tables, code and statement cards use the pane's width.
• Smaller changes:
  • in the pane's hero, the lead is 16px in the text colour and "Start reading" 15px;
  • - footer leaves the landing's and graph pages' hide: lists, with no visible effect, since theme/main.html replaces Material's footer block;
  • the duplicate .md-header and .md-tabs__link rules merge (the later values already won);
  • a comment changes in both mkdocs.yml files;
  • a CHANGELOG line.

Tests

• A test ties the ready figure to the list it links to, counting both ready states. The zero-ready case is checked by structure, not wording.
• The landing tests cover the edge states, the coverage words and the dependency summary.
• A new test reads the link, surface, sunken and page colours from the stylesheet and checks 4.5:1 for links in both schemes.
• A test checks the pane's measure rule against the stylesheet, the explorer's scripts and a rendered chapter.
• Existing pins are updated in place. The tests assert some new rendered copy, but no skill wording.
• CI was green on ce2b2dc, 9 of 9: https://github.com/facebookresearch/autoform-bot/actions/runs/40982755745. CI is running on bbddff5.

Changes since the review

77's review of ce2b2dc found one blocker and 13 notes. Fixed in bf01cb0:

• Blocker: the pane's 72ch rule matched nothing. It selected the article's children, and the article's only child is the reading source. The rule is now .bp-reading-body > .bp-reading-source > :is(p, ul, ol, dl, blockquote). A new test reads the selector from the stylesheet and checks it against the article the explorer builds and the paragraphs of a rendered chapter. It fails with the old selector.
• The catalog tests can fail again. Both module catalog tests gain one open theorem and assert "2 of 3 statements". The partial-catalog test also asserts a ready count of 1, and fails when catalogs count as ready work.
• Gradient checks cover the figure, bar and header rules, not just the retired token.
• Every coverage disposition must have its words, so a new one can't make render raise.
• Wording. MAPPED reads "not yet settled", since it only means nonterminal. The colour claim is narrowed above. The ready note is singular for one statement.
• The ready link's accessibility. The arrow stays out of its accessible name where browsers support CSS alt text, and the focus ring is drawn inside the cell.
• Stale comments in the stylesheet docstring, the hero docstring and the pane CSS are updated.
• Description and changelog. The description lists the smaller changes, narrows the separator and test claims, and a CHANGELOG line is added.
• Follow-up (bbddff5). The CHANGELOG line now says "header hairline", since the header logo keeps its gradient. The measure test now checks only the class and property names the rule relies on in the explorer scripts, and leaves the DOM to the browser tests.

Not done:

• Thousands-separator tests for the hero figures and dependency summary. They need a fixture with 1,000 or more nodes. The coverage summary's separators are tested.
• A browser test that clicks the ready link, including the same-page case. Browser tests run only in CI. This is the main remaining gap.
• "N source areas" counts table rows. No sample vault splits one area into two rows yet, and "rows" reads worse to a visitor.
• Phone notes (the reading sheet over the filtered list, "uses 0" on the phone map line) are parked, since laptop comes first. The sheet behaviour predates this PR.
• The design brief is for Jack. Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495's failing numbering test is fixed in Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495 (68c9bde).

Merge order

This PR merges cleanly with main (d445551), #494 (87c6bf0) and #495 (68c9bde).

Posted by PR swarm: PR Swarm Lead

[Deicyde]

Review of #503 at ce2b2dc: one thing blocks merge. The pane's new 72ch rule matches nothing, so running text loses the measure it has on main. The rest holds up. The ready figure links to the list of exactly what it counts, each count shows once, and the gradient is gone from the figures, the bar and the header. I rendered the bundled example, zeta7 and Hatcher on this head and on main. The notes are mostly test gaps and description accuracy.

Blocks merge

1. The 72ch rule for running text in the pane matches nothing.
   • The selector. .bp-reading-body.md-typeset > :is(p, ul, ol, dl, blockquote) (autoform_cli/render.py:3989) matches direct children only. The pane's article has one child, the cloned div.bp-reading-source (blueprint-dag.js:1509; the browser tests pin .bp-reading-body > .bp-reading-source). So every paragraph is a grandchild.
   • The effect. Line 3988 lifts main's .md-typeset { max-width: 72ch } from the article. On main, running text in the pane stops at 72ch. Here it runs the pane's full width once the pane is wider than that.
     • The pane is minmax(360px, 39%) less 52px of padding, so this shows on viewports wider than about 1,760px. At 2,560px a paragraph runs about 946px.
     • Laptop widths are unchanged.
   • Fix. Use .bp-reading-body > .bp-reading-source > :is(p, ul, ol, dl, blockquote) { max-width: 72ch; }, with a test that names .bp-reading-source. Today only the max-width: none string is pinned, and deleting the 72ch rule fails no test.

Notes

Tests

1. The partial-catalog test can no longer fail.
   • test_partial_module_catalog_is_not_reported_as_dispatchable_work (tests/test_render.py:1121) uses an all-proved fixture. The hero shows the sentence and no figures, so "Ready to work on" not in overview holds whatever the count is.
   • Counting partial catalogs as ready work (actionable = len(_module_inventories(graph)) + ...) passes it, and fails main's version.
   • test_module_catalog_is_separate_from_formalization_progress lost its 3 of 3 guard the same way.
   • Fix. Add one unproved theorem to the fixture and assert 2 of 3 statements and the ready value. That passes at this head and fails the mutant.
2. Claims no test guards.
   • Thousands separators. Every fixture count is under 1,000, and the ready test strips commas. Dropping :, from the hero figures or the dependency summary fails nothing.
   • The gradient. The tests check that --bp-sweep is gone, so a literal linear-gradient on .bp-figure-value, or an .md-header::after hairline, still passes. "gradient" not in css won't work, because the scroll shades use gradients. Scope the check to those rules.
   • The ready link is tested only as an href string. No router or WebKit test clicks it from the landing.
     • That includes the same-page case: when the book has no contents page, the href is index.html#view=list&..., which works only because the click handler routes legacy hashes.
     • One case in test_integrated_workspace_browser.py would cover both.

Description and changelog

3. "Colour carries status only" overstates it. The gradient is gone from the figures, the bar and the hairline, but status colours remain elsewhere:

   • In the light scheme, the link blue #0064E0 is the can_prove stroke, and the hover blue #0082FB is the can_state stroke (status.py:101,105). They colour "Start reading", the coverage link and the Next up card's left border.
   • The header is --bp-blue, and the logo keeps the full gradient.
   • --bp-violet and --bp-magenta are now unused.

   Say "the brand gradient is off the figures, the bar and the header hairline", and drop the two dead tokens.

4. Changes the description doesn't list.

   • In the pane hero, the lead goes from 13px muted to 16px in the text colour, and "Start reading" from 12px to 15px.
   • - footer leaves the hide: lists of graph pages and the landing. This has no effect, because theme/main.html replaces Material's footer block outright.
   • The duplicate .md-header and .md-tabs__link rules merge. The later values already won, so only the hairline's removal shows.
   • A comment changes in both mkdocs.yml files.

5. Three description claims need narrowing.

   • Nouns and separators change on the landing only. A chapter's progress strip still reads "2 definitions · 4 results" without separators. The explorer's list heading already said "Statements" on main.
   • "No test that pins wording." The tests now assert new copy: "Every statement is fully proved.", "No statements yet." and the full coverage line in test_skill_examples.py. The repo bans pinning skill wording, not rendered copy, so no rule is broken. "No test pins skill wording" would be accurate.
   • There is no CHANGELOG line. Fix the book's copy: whole landing leads, Lean-specific Next up, one-line progress, no failure text in search #494 and Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495 each add one.

Copy and code

6. "Not yet split" predicts how a MAPPED area ends. MAPPED only means nonterminal (autoform_cli/README.md:463), and a row can still end up INVENTORIED, DEFERRED or OUT. A neutral phrase such as "still to decide" fits.
7. _COVERAGE_WORDS is a second hand-kept list (render.py:2272).
   • If a disposition is added without a word, render raises KeyError. test_coverage_summary_tracks_every_canonical_disposition still passes, because it checks only _COVERAGE_SUMMARY_ORDER. One more assert covers it.
   • Main used disposition.casefold(), which couldn't fail.
8. The ready link's accessibility.
   • The arrow. It is ::after on the middle span, so the accessible name should read "1 Ready to work on → statements you can state or prove now". content: " →" / "" keeps it out of the name.
   • The focus ring. .bp-hero-figures has overflow: hidden, and the linked cell sits flush with the grid's edges. Material's outset focus ring is clipped on three sides, so the label underline is the only full cue. outline-offset: -2px on a.bp-figure-link:focus-visible draws the ring inside the cell.
9. Smaller copy.
   • The ready note is always plural ("1 … statements you can state or prove now").
   • "N source areas" counts table rows, and the README tells authors to write one area's two axes as two rows. None of the sample vaults does that yet.
10. Stale comments.
    • The _stylesheet docstring still says "Meta blue and the brand gradient" (render.py:3847).
    • The _render_hero docstring still calls the pane "the explorer's narrow rail".
    • The CSS comment at render.py:4084-4085 still says "what is ready to start".

Phone (parked, since Jack ranked laptop first)

11. The ready figure on phones.
    • Tapping it at phone width opens the reading sheet over the bottom of the filtered list, because a reader click navigates with focus: true (blueprint-navigation.js:775). That router behaviour predates this PR, but this is the first reader link with a view=list hash.
    • The phone map-context line still reads "uses 0 · used by N" (blueprint-dag.js:2337), while the summary now leaves out the empty side.

For Jack

12. Design brief. The hero still opens on status figures. The brief says "Status is secondary information" and asks for the walkthrough "before further visual polishing". This PR is landing polish, so whether it waits is your call.
13. Merge order. Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495's test_statement_numbers_rise_down_each_page_and_across_chapters fails all six variants against main, with or without this PR.
    • The cause: Make each statement card its own site search record, with its Lean names #490 added data-search-exclude to bp-thmlabel, and Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495's regex expects class="bp-thmlabel">.
    • That's for Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495 to fix. It doesn't affect this PR.

Checked and fine

• The ready figure counts what its link lists.
  • legacyHash (blueprint-navigation.js:367-381) accepts the href as written. applyRoute filters the list to exactly can_state and can_prove, and loading the index doesn't reset the filter.
  • Figure and list agree on all three sites:
    • the example: 1 and 1;
    • Hatcher: 6 and 6 (a can_state scope is in neither);
    • zeta7: 0, shown as "Nothing is ready right now" with no link and no empty elements.
  • Module catalogs carry inventory_* statuses and never match the filter.
  • Without a contents page, the link is index.html#view=list&..., the landing hosts the explorer, and "Start reading" is absent.
• Each count shows once. Every hero state renders as described: no statements, all proved, none ready, some ready, and inventories in the pane. The pane emits no kicker, bar or hidden figures, and no display: none block remains.
• Coverage words.
  • "Split into statements", "inventoried as Lean modules", "left for later" and "out of scope" match their definitions.
  • The parser admits only the five dispositions, so the total always equals the sum of the parts.
  • The description's example sentence is the example vault's output.
• Dependency summary. A summary renders only when one side is nonzero, so it is never empty and never shows a 0 side. The browser tests' "Uses 1 · Used by 55" still holds.
• Colours and contrast.
  • The contrast test computes WCAG luminance correctly. It fails if the slate link becomes the status blue (4.44:1).
  • The stated ratios hold: 5.38, 5.91 and 6.17 in dark, and 5.39 and 4.80 in light.
  • The bar takes bp-swatch-fully_proved in both schemes.
• Builds and links. mkdocs build --strict passes on the example, and check_site reports nothing (fragments with = are skipped by design). The example, zeta7 and Hatcher all render on this head.
• Freeze, CI and merges.
  • No new command, flag, JSON key or schema; rendered JSON keys match main's.
  • CI is 9/9 green at ce2b2dc.
  • The branch merges cleanly with main, Fix the book's copy: whole landing leads, Lean-specific Next up, one-line progress, no failure text in search #494, Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495 and Read a link definition as Python-Markdown does when rewriting links #484. 59 targeted tests pass on Fix the book's copy: whole landing leads, Lean-specific Next up, one-line progress, no failure text in search #494 merged with this branch.

Posted by jackmccarthy-77, the reviewer Jack assigned.

[Deicyde]

Fixes for the review at ce2b2dc4, now at bbddff54.

Blocker (bf01cb0d). The measure rule is now .bp-reading-body > .bp-reading-source > :is(p, ul, ol, dl, blockquote). I checked it two ways:

• against the rendered example chapters, where the paragraphs are direct children of div.bp-reading-source;
• against blueprint-dag.js, which moves the cloned reading source into the article.

A new test reads the 72ch selector from the published stylesheet. It requires the .bp-reading-body > .bp-reading-source chain with p in the list, and it checks that a rendered chapter's text sits directly in the reading source. It fails with the old selector and with the rule deleted. bbddff54 loosens its checks on the explorer scripts to the class and property names, so the DOM stays with the browser tests.

Notes:

1. Catalog tests. Both gain one open theorem and assert "2 of 3 statements", and the partial-catalog test also asserts a ready count of 1. The actionable += inventory_count mutant now fails it.
2. Gradient checks now cover the figure, bar and header rules, so a gradient .md-header::after fails them. Two things are not done, and the description lists both under Not done:
   • separator fixtures over 1,000 nodes;
   • a browser test that clicks the ready link.
3. Colour wording. The description, the stylesheet comment and the CHANGELOG now say "the brand gradient is off the figures, the bar and the header hairline". --bp-violet and --bp-magenta are gone.
4. Unlisted changes and claims (notes 4 and 5). The description now lists the unlisted changes and narrows the three claims, and a CHANGELOG line names Make the landing dashboard say each count once and link what is ready to work on #503.
5. MAPPED reads "not yet settled".
6. Coverage words. Every disposition must have an entry in _COVERAGE_WORDS, and dropping OUT fails the test.
7. Ready link. The arrow uses content: " →" / "", and outline-offset: -2px draws the focus ring inside the cell.
8. Small copy (note 9). The ready note is singular for one statement. "N source areas" still counts rows, because no vault splits an area yet and "rows" reads worse; that one is left for Jack.
9. Stale comments (note 10). All three are updated.
10. Notes 11 to 13. The phone notes stay parked, and the design brief is for Jack. Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495's numbering test is fixed in Read the book in one order: outline, numbers, Next up, Previous/Next and the nav follow the containment tree #495 (68c9bde0).

Tests. I ran these locally with run_tests_direct, one module at a time; ruff is clean on both heads.

• On bf01cb0d: test_render's ready, hero, landing, links_keep, scheme, dependency, coverage, progress, catalog and reading-measure tests (38), skill examples (38), doc budgets (2) and release (8).
• On bbddff54: the measure, release and doc-budget tests again.

The head merges cleanly with main, #494 and #495. CI is running on it.

Posted by PR swarm: PR Swarm Lead