chore: enforce the Phase 7 chapter and tutorial obligations - #9249
Merged
Conversation
PLAN/Phase7.md says a library reaches done_through 7 when it has a reference chapter that builds inside HexManual and when every tutorial anchored to it exists. Nothing checked either, and both had drifted. Add scripts/check_phase7.py and wire it into the existing lint job. For every library at done_through >= 7 it asserts a chapter at HexManual/Chapters/<Lib>.lean, or, for a Mathlib companion, a "# The Mathlib correspondence" section in its computational partner's chapter -- the established convention, since no *Mathlib library has its own chapter and five sit at 7 on the strength of a partner section. It then asserts HexManual.lean imports the chapter, so `lake build HexManual` actually elaborates it, and that every anchored tutorial exists at the path PLAN/Phase7.md records. The anchor table is parsed from that file rather than duplicated, so re-anchoring is a one-file edit. Re-anchor the Kummer-Dedekind tutorial from hex-gfq to hex-berlekamp-zassenhaus. hex-gfq is not among its primary libraries; SPEC/tutorials.md names hex-poly-z, hex-berlekamp-zassenhaus, and Mathlib's NumberTheory.KummerDedekind. It factors an integer polynomial modulo a prime and reads the result as splitting data, so it is gated on integer factorization rather than on the finite-field constructors. Roll HexGF2 back to 6. Its chapter exists but the AES tutorial anchored to it does not, so Phase 7 is not complete; scripts/status.py now offers it Phase 7 work again, which is the point. HexGFq stays at 7: with the Kummer-Dedekind tutorial re-anchored it has no outstanding anchored tutorial, and its chapter exists. HexBasic is at 7 with no chapter and is recorded as a visible exemption rather than a silent pass; whether it wants a chapter or a rollback is a call for the planner. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Covers the Conway regeneration and table widening, the GF(2) correspondence refactor, and this Phase 7 check, and corrects the CI claim in the previous progress file. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review found the checker was not robust enough to gate CI, and that its
central rule was an unwritten convention the code merely followed.
State the rule in PLAN/Phase7.md: a mathlib: true companion does not get
its own chapter, and its Phase 7 deliverable is a "# The Mathlib
correspondence" section in its computational partner's chapter. Five
companions already sit at done_through 7 on that basis, so the checker
was reading an existing practice back as policy without the policy
existing. Now the document says it and the checker enforces what the
document says.
Roll HexBasic back to 6 rather than exempting it. It sits at 7 with no
chapter, which is the same violation HexGF2 was rolled back for, and a
per-library exemption list in the checker is a worse answer than an
honest done_through.
Harden the checker against failing open, which is worse than not having
one:
- The anchor table is located by its header and schema, and a malformed
or missing table is an error rather than zero rows and a pass. The
previous parser scanned every line for one regex, so reformatting the
table silently disabled the tutorial checks entirely.
- A tutorial must be imported and {include}d by HexManual.lean, not
merely present. An unbuilt file proves nothing.
- Tutorial paths must be normalized, .lean, and inside
HexManual/Tutorials; absolute paths and .. traversal are rejected.
- Anchor slugs resolve through the committed SPEC paths, so hex-gf2 and
hex-lll match exactly and hex-g-f2 matches nothing. The previous
hyphen-insensitive comparison accepted any misspelling that agreed on
letters.
- Chapter imports are matched as anchored import lines rather than as
substrings, so a commented import or a longer module name no longer
satisfies the check.
Add scripts/test_check_phase7.py, 14 tests over the fail-open cases, and
run it in CI beside the checker.
State the Kummer-Dedekind anchoring as the current rule rather than as a
change from a previous one, per the convention that PLAN/ carries the
design rather than its history.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
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
1 participant
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.
This PR adds
scripts/check_phase7.py, re-anchors the Kummer-Dedekind tutorial, and rollsHexGF2back todone_through: 6.Stacked on #9242; review that first.
PLAN/Phase7.mdsays a library reachesdone_through: 7when it has a reference chapter that builds insideHexManualand when every tutorial anchored to it exists. Nothing checked either, and both had drifted:HexManual/Tutorials/holds one of the four required tutorials while two of the three missing ones are anchored to libraries recorded as done.The new check runs in the existing lint job. For every library at
done_through >= 7it asserts a chapter atHexManual/Chapters/<Lib>.lean, or, for a Mathlib companion, a# The Mathlib correspondencesection in its computational partner's chapter. That second form is the established convention rather than a concession: no*Mathliblibrary has its own chapter, and five of them sit at 7 on the strength of a section in the partner's. It then assertsHexManual.leanimports the chapter, solake build HexManualactually elaborates it, and that every anchored tutorial exists at the path the anchor table records. The table is parsed out ofPLAN/Phase7.mdrather than duplicated in the script, so re-anchoring a tutorial stays a one-file edit.The Kummer-Dedekind tutorial moves from
hex-gfqtohex-berlekamp-zassenhaus.hex-gfqis not among its primary libraries:SPEC/tutorials.mdnameshex-poly-z,hex-berlekamp-zassenhaus, and Mathlib'sNumberTheory.KummerDedekind. The tutorial factors an integer polynomial modulo a prime and reads the result as splitting data, so it is gated on integer factorization rather than on the finite-field constructors.HexGF2rolls back to 6. Its chapter exists but the AES byte-arithmetic tutorial anchored to it does not, so Phase 7 is not complete, andscripts/status.pynow offers it Phase 7 work again.HexGFqstays at 7: with Kummer-Dedekind re-anchored it has no outstanding anchored tutorial, and its chapter exists.HexBasicsits at 7 with no chapter. That predates this check and is recorded as a visible exemption with its reason rather than silently tolerated; whether it wants a chapter or a rollback is a call for the planner, so the script prints it as a notice on every run.🤖 Prepared with Claude Code