Repository maintenance

Read side by side

Current priority: navigation, record consistency, reproducibility instructions, and collection tooling. Further proof reviews are deferred. Existing findings and completion gates remain in the finalization queue.

Choose the right tool

Run commands from the collection root. The verification guide gives the routine check sequence and checkout requirements. Navigation and record tools use Python's standard library and Git where they inspect source history. Package build and qualification tools document their additional requirements.

For routine wording or navigation changes, edit the relevant template or maintained document, then use update_completion_status.py. The source-navigation and publication-metadata scripts reconcile source and publication records. Review their dated inputs before reuse. Use a separate output directory to inspect their overlays before applying them.

Library observations are kept in LIBRARIES in update_publication_metadata.py. The qualification page, publication metadata, and contribution ledger use those same observations. Before updating them, inspect each repository's branch commit, workflow result and run commit, and release-tag commit. Record the observation date. A passing run must match the checked source revision. Keep the release-tag commit separate when the tag points to an earlier edition. These local tools validate the recorded identities and do not query GitHub for newer results.

The browse-resource registry selects direct reading, text, Lean, and code links for every primary component. browse_navigation.py validates each selection against that component's import receipt and the committed tree, then generates the browse hub, category/resource finders, and individual work pages in docs/works/. Update the selected links when an edition changes. File names alone do not justify a change in scientific status. PDF guides are kept separate from actual Lean files. Incubator entries retain their placement.

Each work page has Read, Written proofs, Lean, Code, and Evidence sections, return links, and previous/next links within its collection. The evidence catalogue links back to that work. Older category anchors remain available. To change a generated navigation page, edit the renderer or resource registry and regenerate the page. Work pages and resource finders use headings and single-column lists to remain readable in narrow panes.

Resource finders have stable component anchors and title shortcuts within each collection. Work sections link to their exact finder entry, which links back to the corresponding section. Generate both links together. Only link to a finder when it has a matching resource. A formal setup document alone must not put a work in the Lean-source finder.

The lean_setup resource kind identifies text instructions, source maps, or replay prerequisites. It is separate from .lean source and PDF guides. Prefer a small mathematical-module directory or a documented package interface as the first source shortcut. Retain wider project/ancestry links when needed, and label historical checkpoint instructions explicitly. Each new selection still needs ownership and committed-path validation. Reading a setup guide does not execute its commands.

The renderer also records the maintained SRIC 0.3.3 correction as the first code route, with a link to its existing repair report. The original imported code stays linked and is labeled as the preserved edition. Its import receipt remains unchanged.

navigation_links.py checks inline relative Markdown links against case-sensitive file and directory paths and validates fragments in maintained/generated pages. It ignores fenced and inline code examples, handles encoded file names and repeated heading IDs, and rejects duplicate explicit anchors. The status command reports checked links/fragments and separately counts remote links and original-source fragments that it does not validate. This is a navigation check, not a full Markdown parser, HTTP availability scan, or PDF accessibility audit.

record_navigation.py and proof_review_coverage.py are supporting modules called by the status tool. The latter checks the links between existing claims and evidence. Running the status tool does not perform a new proof review. The test_*.py files are the collection tooling regression suite. The workflow guide describes which commands GitHub runs and which workflows can publish.

Keep records traceable

Use the records guide to locate the current entry point and dated evidence. A source receipt, test result, and written review establish different things. Keep setup failures, skipped checks, and scientific findings distinct.

Selected published cleanup checkpoints

The reader website guide documents the shared HTML site, reading ZIPs, claim locations, library pins and publication workflow. Update the reader registry and templates alongside generated pages. Keep the accessibility limitations and the scope of transcribed claim links explicit.

These entries record two completed documentation/tooling updates from 27 October 2026. For later changes, see the Git history. Neither checkpoint adds a mathematical review or changes scientific status.

The linked workflow results belong to those commits. A later green run does not replace an earlier receipt or expand its scientific scope.

Contributing · Run and verify · Documentation