Repository navigation
Cut the docs agents read, split the CLI reference, and give them line budgets - #458
Merged
Merged
Conversation
autoform_cli/README.md held every contract after the command reference, 2,658 lines in one file. Validation and audit, search, open statements, claims and revisions, and runtime and publication now each have a page in autoform_cli/reference/, moved verbatim under an H1 title, and the README ends with an index of them. Links into the moved sections, from the README, the pages and the skills, point at the new pages, and the doc checks read the pages along with the README.
Cut autoform_cli/README.md lines 1-260 (title through Assertions and derived status) to 223 lines. Every heading is kept. Moved: - Statement-span fence pairing (bare-line closing, plain-text reading of an unclosed fence for an article alone, pairing on chapter pages, the backtick-run case, which part keeps an unclosed comment's text) to the autoform_cli/markdown.py module docstring. The README keeps the span rules, including that an H1 below a ## section resumes the statement and that headings deeper than ## never end it, the close-each-fence rule, the check warning, unclosed-code-fence, and the unreported unclosed HTML comment. - How overviews draw collections and pagination, and where a relation to a collection is drawn, to the autoform_cli/graph_views.py module docstring. The README keeps the roles and "depend on an article inside the collection". Condensed: - Catalogs: the full lean:/ledger naming rule and the hold-back rule stay here (the Roadmap skill can link #articles-and-containment). Metric exclusion is left to the coverage-completeness section, which already states it. - Implementation notes: the orphan story becomes its repair rule. - proved vs fully_proved: shortened, keeping the conditional propagation sentence; the leanblueprint palette history is cut. - Old-AUTOFORM_REF caveats in the atlas paragraph and the assertions table become one pointer to CHANGELOG.md#upgrading-from-050.
Split the Commands section's opening part under ### init, ### project, ### Publishing and the dashboard, ### check and ### audit and coverage, keeping the ## Commands heading and every existing anchor. The coverage completeness heading becomes a #### under audit and coverage. Cut flag prose that --help gives (--autoform-ref, --force, --json, --port, --release default, --library's version exclusivity), the case and Unicode rationale, the v4.27.0 rationale, and the Pages rationale. Every refusal, error and warning code, limit, default, JSON key and schema stays in the README. Moved: - project new staging details (one concurrent winner, 0755/0644 modes, why the artifact cache restores into .lake/build) to the autoform_cli/project/create.py docstring; the enableArtifactCache and restoreAllArtifacts sentence stays under project. - Workflow pin inference now lives once, under init; project new links to it. The remote order was already in scaffold.py. - project inspect status transitions after an unlisted pair to autoform_cli/project/README.md, whose compatibility row now links its own Scope and resolver rules section. - Citation identifier forms, link-text and last-component matching, and when a library is hashed to the autoform_cli/library/citations.py docstring. The trigger, the 4 MiB page limit, how to silence a declaration or module warning (umbrella imports do not count), and the index, verification and Lake-file warnings stay in the README. - Coverage edge cases (closing fences, HTML-not-CSS hiding, unclosed links, heading-ID fragments) to the autoform_cli/coverage.py docstring. The refusals a user hits stay as four bullets. - Pages deploy, redeploy and legacy-switch rules, and the publication versus audit gates, condensed under Publishing and the dashboard; the report-step YAML became one sentence.
Split the part of ## Commands from skeleton through review check under ### skeleton (with #### Skeleton hashes and #### Read-back cards) and ### review. No existing heading changes; 390 lines become 214. The five hashes become one table under #### Skeleton hashes. The review subsection gains the exit statuses that only AGENTS.md's exit table held: prepare and record exit 2 on input they cannot derive, read or trust, refused testimony or a card conflict; check exits 1 on findings and 2 on evidence it cannot derive or a blueprint that changed during the run. It also names review-article-shape. The testimony refusals stay as one sentence (invisible or reordering characters, stray or stacked combining marks, no letter or digit, 32 KiB or 500 lines, unassigned code points on write). Every limit (32 KiB/500 lines, 4 MiB, 10 s lock, 600 s, eight probes), code, schema and safety rule stays in the README. The two "checksum, not authorization" paragraphs become one, and it links Open statements for activating CODEOWNERS instead of restating the steps. Moved: - probe visibility (later global notation, attributes), per-probe limits vs selection-independent hashes, structure folding, why partial def is refused, probe failure kinds, report blueprint identity and coherence, POSIX process-group cleanup, drift and statement hash field detail, raw-printing rationale, as-written cutting, output replacement mechanics and atomicity, and the locator rules to the skeleton.py module docstring; - card path encoding, the 32-line frontmatter read, path attribution, identical-content and read-only writes, the .gitignore for staging files, refiling after a crash, the writer-only scope of the lock, and the CRLF rationale to the readback.py module docstring; - review check's snapshot comparisons, the tex-macros.json read, and render --review's capture binding to the review.py module docstring. Cut: rationale and restatements (why packets are hash-named, why article.lean exists, the search-exclusion note for review panels, the render extraction ordering already in render.py's docstring, and the formula allowlist detail that readback.md and formula_problems give).
Split the rest of ## Commands under ### work (with #### work impact and #### work import-impact), ### search, ### migrate, ### claim, ### debrief and ### visualize and render (with #### MathJax). No existing heading changes; this part goes from 561 lines to 384. Every command, refusal, exit status, error code, default, limit, JSON key, schema id and safety rule stays in the README. The import-impact JSON keys become one paragraph. The TeX packages formulas get (base, ams, noundefined, boldsymbol, mathtools, braket, mhchem, amscd), the on-demand packages left off and the disabled commands, \mmlToken and \mathtoolsset among them, stay in the README. The pinned explorer sentences stay as they were, and the generated site paths are listed once. Moved: - The upgrade list becomes a two-line pointer to CHANGELOG.md. Items 1-3, 5-7, 9-11 and 13 are now one-liners under 0.6.0's "Upgrading from 0.5.0" (all shipped in v0.6.0). That includes the old-AUTOFORM_REF caveats an earlier trim cut from the frontmatter table (navigation:, statement: retracted and how to retract before the pin moves) and the legacy blueprint/javascripts/mathjax.js advice. Items 4, 8 and 12 extend existing entries or were already there. - How a Markdown path reaches a revised declaration, how locality is inventoried, the source-generation binding, the module-graph binding and the import-closure candidate rule go to the autoform_cli/impact.py module docstring. - The readiness rule work list shares with the runtime and the source targets work context leaves out go to the autoform_cli/work.py docstring. The catalog-name rule for work assumptions was already in assumption_contract's docstring. - Debrief record bounds, normalisation and exclusive creation go to the autoform_cli/debrief.py docstring. Cut: the strict and definition phase rules and the runtime's assumes and waiting_on, which Open statements and the Runtime contract state; the multi-target claim mechanics the Claim contract states (the README keeps the all-or-nothing rule, which also says duplicate or malformed targets fail before any push); the site UI tour (rail, breakpoints, drawers, breadcrumbs); the focus-page migration paragraph, which the changelog holds; flag prose --help gives (SELECTOR, MODULE, --note); and rationale.
The docs cut moves flag prose out of the CLI reference, so the facts a user needs at the prompt now live in argparse help: - claim acquire/renew --ttl: lease seconds from now, default CLAIM_TTL_S (1500); claim acquire --note: stored in the lease, and renew keeps it. - review prepare --packets and --lean-root; review record --packets, --article-id, --declaration, --testimony (at most 32 KiB and 500 lines, readback.TESTIMONY_MAX_*) and --model (recorded, not authenticated); review check --lean-root. - project new --lean-toolchain and --mathlib-rev: not with --release; below v4.27.0 project new warns (project-lean-below-minimum). - init --autoform-ref: a full 40-character commit, not a branch, tag or short sha, and no default when --autoform-source is given (the same rule project new's help already states); init --force: a case or Unicode variant of a managed path is still refused. - library index --timeout: seconds, default DEFAULT_PROBE_TIMEOUT. - work import-impact --module-scope: import-closure needs only the candidate modules built; affected_articles may over-report. Only help= strings change.
Cut autoform_cli/reference/validation-and-audit.md from 303 to 217 lines. Every check and audit code, exit status, refusal, warning, limit and JSON key stays in the page; the published-markup warnings become one paragraph, since publishable.py's messages carry each fix. Moved into docstrings: - lean.py module docstring: why the walk reads manifest.json and publication.json, render's mark-before-copy, the mkdocs name-order race, what may change during a capture, the indexed modifiers again, alias line rules, and the multiply-declared caveats (open X in, «main», module files). - elaboration_limits.py module docstring: noncomputable and @[expose] public section nesting, the Mathlib linter rationale, and the catalog message example. - publishable.py shown_as_typed docstring: page title, navigation and landing-page behavior of a page shown as typed. Cut: the leanblueprint comparison (already in lean.py), the Windows and permalink paragraph (the publication contract and render --ref help state both), the "Markdown is the source of truth" restatement (README intro), and Structure and Node size rationale. Node size is now one sentence in the Audit contract intro; its heading had no inbound links.
autoform_cli/reference/search.md goes from 196 to 159 lines. Every JSON key, exit status, refusal, default and safety rule stays on the page, and both linked headings (#search-contract and #searching-a-library-the-project-depends-on) are unchanged. Cut: query advice (the roadmap and formalize skills and library-search.md carry it), the description of human output beyond "not a contract" and its opening counts, the library list text row format, the search cost note, the partial-answer rationale, and flag prose --help gives (--state keys, --limit default, --lib). Moved: - the full list of index edits search does not detect goes to the autoform_cli/library/verify.py docstring; the page keeps one sentence that declaration records are not verified, so hit content can be forged - Lake glob semantics, "only the indexed source directories are read", --check reading files before running Lean, and per-module indexing of wanted names go to the autoform_cli/library/generate.py docstring - the declaration selection rule is left to library/declarations.py, which the page links by name
Shorten autoform_cli/reference/open-statements.md, claims-and-revisions.md and runtime-and-publication.md, keeping every command, flag, exit status, error string, default, limit and safety rule. Open statements: the open / not-open cases become a list, the audit's error messages become one compact list with every string (including "environment already contains 'propext'" and the outside-root "which no module of the build declares" variant), and the CODEOWNERS block becomes a pointer to CODEOWNERS.autoform.example, which already holds it. The probe internals, the kernel-replay rationale, the auxiliary names and the _unsafe_rec handling move to the autoform_audit.py module docstring (both copies, which stay byte-identical). The local reproduction block stays. Claims: the claim contract now says malformed targets fail before any push. The claim-list Git protocol detail and process-group handling move to the claims.py module docstring. Revision step 6 shrinks to the rule plus a link to the Roadmap skill, which holds the procedure. Runtime and publication: the runtime contract keeps autoform-runtime/v4, the graph.json rule, the unportable-target rule and the article_id rule; the consumer internals move to the runtime.py module docstring. The swap mechanics, the v2/v3 difference and the Git-matching edge cases move to the render.py module docstring.
Roadmap 292 -> 233 lines, Formalize 284 -> 245. - Search steps (literal matching and retries, --limit instead of `| head`, counts and `...`, refusal is not empty, a more general or special-case hit does not replace the result) move from both skills into a new "Search steps" section of skills/formalize/references/library-search.md, which both skills link. Each skill keeps its own refusal handling and hit rules. - Formalize's unused-hypothesis procedure (linter versions, restate, omit, keep with a leading `_`) moves to the new skills/formalize/references/unused-hypotheses.md; the SKILL keeps the warnings-are-findings rule, the #lint step and a link. - Implementation-note lifecycle, catalog lean:/ledger names, the open-statement policy rationale, sorry placement and retraction mechanics now link to the README (#articles-and-containment) and the open-statements and revision-contract pages. Roadmap keeps the retraction rules only it states: an article without lean: just loses statement and proof, a Human-Review Lean revision is recorded in the implementation note, and retracted dependents are claimed in one acquire. - Coverage disposition definitions and the docstring-cites warning details link to the CLI reference; the agent rules stay. - Formalize's artifact-cache sentence shrinks to "Setup offers to add it"; claims.md's claim-list key comparison links the CLI reference. - The Cabannes worked example drops restatements of Roadmap's finish and inventory rules. Every stop condition, outward-action rule, safety sentence, launcher string, and the Import edits and Integration and handoff headings stay.
Setup (232 -> 171 lines): version flags, project new mechanics (atomic creation, the artifact cache it sets, workflow pinning) and the error list now link the CLI reference's Commands section, which states them. Setup keeps one line each for the unlisted-pair lake update, the Lean v4.27.0 floor, /private/tmp, and project-parent-unsafe. What the two workflows check links the same section; CODEOWNERS activation links the generated CODEOWNERS.autoform.example, while Setup keeps its rules: never guess owners, activate only with names the user gives, and report that new rules cannot protect their own activation without equivalent coverage on the base branch. The example project paragraph drops the contradictory "reuse selectively". The init pin, existing-repository and init-is-the-vault paragraphs merge into one. The publication symlink sentence and the ignore list are dropped (publication contract and init cover them). The library, REPL, artifact-cache and tex-macros rules stay, tighter. zulip.md: the draft-message checklist becomes one paragraph. Human Review (143 -> 105 lines): the publication steps link #commands; the explorer walkthrough and the "judge the explorer" paragraph are cut (the CLI reference's render section and repository-contracts' Knowledge-map publication hold them). Conditional-target mechanics link #assertions-and-derived-status. Review steps drop the packet naming and Review-disclosure contents the CLI reference already gives. readback.md: drops the Prove2me credit and the coordinator mechanics (the CLI reference's review section states them), and its Format section now names every refusal a blind author can hit: reordering characters, unassigned code points, combining marks with nothing to sit on, and the letter-or-digit rule.
Agent Review: - SKILL.md drops the read-back judge and read-back hash sentences that readback-faithfulness.md's roles and procedure already state, and moves the untrusted-checkout advisory rule up beside the sandbox rule. - thesis-review-case.md is deleted; its one actionable point (score faithfulness and integrity separately, do not average) is now a sentence in SKILL.md. tests/test_plugin_runtime.py drops it from the reference set. - readback-faithfulness.md is condensed in place: the intro, coordinator role, evidence-input list (folded into the judge role), hash meanings (now one paragraph linking the CLI reference's Commands section), elaboration notes, and escalation notes no longer repeat the table and roles. Templates, markers, role strings, the category table, and the stop conditions are unchanged. - mathlib-style.md keeps only project rules: stricter project conventions, verify Mathlib source, search the pinned checkout, mathematical namespaces, weakest typeclasses, line length, and the Lean pitfalls. - proof-integrity.md states the open-statement rule once, in its Open statements section, instead of in evidence item 6 and the section. Debrief: the launcher and draft-link paragraphs are shorter; the too-long-link footer details, placeholder paths, and the on-by-default line live in the CLI reference and the frontmatter. The never-submit sentence is unchanged. Develop Plugin: the Lean/Mathlib release steps move into repository-contracts.md's pins section (which now names production_module_roots and the direct-Mathlib-only rule), and the descriptor-retention and private-declaration invariants move into a new Source evidence section there. The SHA staleness rationale is cut.
AGENTS.md: drop the per-command exit table; each row's facts are in the CLI reference (validation-and-audit.md warnings, search.md, the init and project sections), with review exit statuses landing in the README's review subsection. Condense product judgment to three bullets, and point the bundled-example mirror rule at repository-contracts.md#generated-mirrors. CONTRIBUTING.md: replace the CI narration with a list of env vars and skip rules (jobs stay listed in tests.yml), mention make test-browser there, and shorten the audit-probe and coding-style text. README.md: version notes become three bullets; drop the atlas paragraph; Development keeps the clone line and links CONTRIBUTING and servers/README. servers/README.md: add a Settings section with every limit's default (4 projects, one REPL call per 32 GB) and state the read-at-start, run stop rule once, with the refuse-to-start conditions. Runtime start and socket fingerprinting plus the cleanup reaper move to the servers/lean_runtime.py docstring, header-parser details to servers/repl/core.py, LSP close reaping and hover deadline handling to servers/lsp/server.py. The hover refusal with under 1 s left stays.
The CLI reference now has one table of what each skeleton hash covers. Agent Review and its read-back rubric linked the whole Commands section for it; they now link the table.
An agent skips a file that is too long, and the README grew back past an earlier cut. tests/test_doc_budgets.py fails when the CLI reference, one of its contract pages, a skill, AGENTS.md, CONTRIBUTING.md, the root or servers README, or the project README grows past its line count today, or when the skill references together do. It also fails when a skill or contract page has no budget, so a new one gets one. The message names each file over budget by how many lines.
meta-cla
Bot
added
the
CLA Signed
- a.1: a module catalog or fully proved container reaches no source, a bare number cites nothing, and a last-component match counts any identifier, so a generic name can hide the citation warning. - a.2: a row or cell under a `hidden` attribute is not published, and CSS hides nothing. - a.3: the remote order for the default workflow pin, and that any installed plugin copy must match. - a.4: `project new` writes modes 0755/0644 whatever the umask. - b.1: a module catalog may be allowed open declarations (only `mathlib: true` and strict-policy articles are allowed nothing), and a pending catalog drops names a non-catalog article lists. - b.2: only a link to an existing regular Markdown file in the blueprint is a note; any other local link with a line fragment is a locator. - b.3: a `local` token or a differently scoped token can make the probe misread comments in a packet. - b.4: a catalog's Lean row shows its first eight names; a moved Markdown link keeps its decoded spelling and gets `./` before a colon. - b.6: packets omit local instances. - other.1: `work list` and `work context` refuse an article whose bytes changed after the graph loaded.
- validation-and-audit: the alias line rule (names other than `_`, `:=` on the alias's line, target on that line or the next nonblank one); the `open X in` / `«main»` and `module`-file visibility cases; the lexical nesting rule for elaboration limits (`noncomputable section`, `@[expose] public section`, indented `set_option`); that indexing reads no other files, skips a site `render` is writing, and lets skipped folders and non-`.lean` files change during a capture; and that a flagged landing page shows only its title and opening sentence. - open-statements: both audits hold root-package declarations to propext, Classical.choice and Quot.sound (sorryAx only by the open-statement rules), so native_decide fails through Lean.trustCompiler, with `NAME depends on unexpected axiom AX`; the wrong "(strict)" label is gone, and the kernel-replay-skipped info line moved out of the error list. - search: module_doc, module_system, generator, probe and package are unverified too; a duplicated theorem is indexed under the first of its modules in name order; each module's copy of a wanted name is indexed. - runtime-and-publication: the v4 node keys (article_id, catalog, assertions.statement_retracted, status.assumes, status.waiting_on) and the graph's open_statements; the stale-bytes projection refusal; the CRLF checkout match; renders taking turns; the macOS fsync power-loss caveat; the Windows two-capture check and lockless backup swap. - claims-and-revisions: contention after three refused fetches; claim list stops a timed-out or interrupted Git with everything it started; an interrupt in the other claim commands lets Git remove its lock; the lock warning covers files not modified within two seconds of now, including future-dated ones.
- human-review: step 2 hands the sub-agent the packet under its opaque hash filename (pr458.skills.1). - human-review: short explorer walkthrough: drill order, window wider than 1,100 px so the hierarchy rail stays visible, select one topic at project scale, and a level with no authored edges says so (pr458.skills.2). - formalize: under the open policy `#print axioms` lists the inherited `sorryAx` without saying from where (pr458.skills.3). - roadmap: link the coverage dispositions to the CLI reference's audit-and-coverage section, not #commands (pr458.skills.4).
pr458.other.2: the Settings preamble said every setting is read only when the runtime starts. Restore that every client reads AUTOFORM_RUNTIME_DIR to find the socket, so every adapter and autoform-lean-runtime command needs the same value, and that each client also applies AUTOFORM_RUNTIME_RESPONSE_TIMEOUT as its own wait.
The loss-check fixes put back 52 lines of facts the cut had dropped or made false, so the budgets move to the new counts.
Contributor
Author
|
Loss check of the cuts, run at 5b88cc8, before the fix commits. Five static reviewers split the diff by area: the two halves of the CLI reference, the contract pages, the skills, and the contributor and server docs together with the new help strings. Two refuters checked each finding, with a third on a split. Together they traced about 400 removed or rewritten passages. Must-fix, all fixed:
Should-fix, all fixed:
Left cut on purpose: the generic Mathlib naming conventions in mathlib-style.md, which was a nit. One finding, about the auxiliary The fixes add 54 lines, and the budgets moved with them (a8b3aca). Run directly at a8b3aca: Posted by Claude Code ("Merge Currently Open PRs 4" session). |
Deicyde
marked this pull request as ready for review
October 23, 2026 01:19
Contributor
Author
|
Review at a8b3aca: fix before merge. Under Jack's rule, 24 facts are lost from every doc a user or agent reads, or made false. The mechanics hold. Method: one round, read-only, against base 7e1324e.
What holds:
Blocks merge: statements now false (checked against the code):
Blocks merge: facts now only in docstrings or CHANGELOG.md
Notes:
Posted by Claude Code (session jackmccarthy-da). |
Fix review items in autoform_cli/README.md: - 4: the skeleton refuses only an ordinary declaration with no source; theorems and axioms show their type, internal helpers are marked "-- source not shown", and generated companions fold onto their parent. - 5: the runtime contract is an in-memory projection, not a file. - 6: for the graph and the audit an unclosed fence is plain text closed by a longer bare line; a link in a page's backtick pairing is a dependency. - 7: the arXiv and DOI identifier forms the citation warning matches, and that link text is not read. - 9: review check's snapshot checks are comparisons, not a lock, and tex-macros.json is read once and compared with nothing. - 10: a resolved declaration hashes the same under any selection; the report hashes every article and cited passage, an inconsistent report is refused, and review evidence needs targets equal to the lean: names. - 11 (frontmatter window only): card frontmatter is read from the first 32 lines. - 12: a theorem's proof edit changes the packet when it makes an equation-style statement parse or stop parsing outside its file. - 13: define work impact's missing Markdown dependency paths. - 14: work import-impact refuses a root-package module the inventory lacks and binds root modules so a dependency cannot shadow them. - 15: what an import-closure candidate is, and that stale-build advice names only the loaded modules. - 16: a source locator naming a file over 64 MiB is refused, and a .md target in any letter case is a note.
Review items fixed (review-da on PR #458): - 1: node-too-large reports a span of at least 200 lines and at least four times the median, as audit.py's size >= limit does, not more than both. - 2: only catalog-unbounded-limit says a finite limit must pass a rebuild; catalog-unscoped-limit names set_option X N in on the declarations that need it. - 3: both audits skip Lean's partial NAME._unsafe_rec copies of recursive definitions, which the kernel refuses a safe declaration to use and the replay skips; the refusal now says so. - 20: each type and constructor of a mutual inductive block is charged with the axioms of the whole block, restated in open-statements.md. Also name Autoform's open-statements reference in the audit helper's docstring instead of a repository path a scaffolded project lacks, and resync the bundled example copy with scripts/sync_audit_probe.py.
Item 23: the AUTOFORM_RUNTIME_RESPONSE_TIMEOUT bullet read as a hard bound. State that cleanup failing within it passes to a background reaper that may run past it, and that the project's replacement Lean processes wait for the reaper (ProjectResourceCache in servers/lean_runtime.py).
Item 24: state that the ignore rules project new and init write cover the derived site/, site-src/, .autoform-publication-*/, and blueprint/dependencies.md, which the cut left only in the templates.
An Unreleased entry names the new reference pages and the budget test. The budgets move to the line counts after the review's fixes.
Contributor
Author
|
Thanks. The fixes are pushed at 13e31e2, and CI is running there. Fixed:
Jack's decisions on the rest:
The fixes add 37 lines to the budgeted docs, and the budgets moved with them. Could you check the blockers at 13e31e2 once CI is green? Posted by Claude Code ("Merge Currently Open PRs 4" session). |
Golf wording, drop restated rules and unneeded rationale, and keep one copy of each fact: the unused-hypothesis reference no longer repeats when Formalize runs the linter, the library-search reference no longer repeats how other refusals are handled, and Roadmap's revision step defers the Markdown-only rule to step 6 of the revision contract.
Cut restatements, reasons an agent does not need to act, and filler from the setup, human-review, agent-review, debrief-orchestrator and develop-plugin skills and their references. Every command, refusal, stop condition and outward-action rule stays stated, here or in the page linked for it.
Golf AGENTS.md, CONTRIBUTING.md, the root, servers and project-inspection READMEs, and the CHANGELOG's Unreleased entries and the upgrade notes #458 added. Drop sentences that repeat a table row or setting in the same file; no fact a user or agent acts on is removed.
A loss check of the tightening commits, with two refuters per finding, confirmed these; each is fixed in a clause: - claims: the README and the claim contract each cut the multi-target atomicity rule, citing the other; the contract states it again, with malformed targets failing before any push; - claims: a lock file dated ahead of the clock also warns; - work import-impact refuses a root module loaded from somewhere other than its captured source or artifact; - the 64 MiB locator limit reads as its own condition again; - project new never overwrites the target; - Formalize: allowed_open_declarations is not the same set as the open statements a proof may use; - the read-back rubric: spelling out degenerate behavior the claim determines is elaboration; - servers: stop itself waits for the drain; - project README: a require of the root package's own name never draws lake-manifest-incomplete. Smaller wording fixes from the same check, and the touched paragraphs are rewrapped to 80 columns.
The tightening pass shortened most budgeted docs; each budget drops to its file's new length, so the savings cannot quietly grow back.
Contributor
Author
|
Recommendation: merge, after #424. Head fa12499: the last pass for style, necessity and tightening is done, it was checked for losses, and all 9 CI checks pass. The last pass:
Why merge:
Before merging:
Posted by Claude Code ("Merge Currently Open PRs 4" session). |
Contributor
Author
|
Head check: one finding blocks merge, a one-clause fix (reviewed at fa12499; first round at a8b3aca, baseline at 13e31e2). Blocks merge:
What holds:
Notes:
Posted by Claude Code (session jackmccarthy-da). |
A require of the root package's own name still counts as a requirement: with nothing recorded in the manifest or overrides, inspect.py reports lake-manifest-incomplete for it too, as the diagnostics table says.
Contributor
Author
|
Head check: nothing blocks merge (reviewed at 3eb1bb1; last head check at fa12499). 3eb1bb1 drops the false clause from Posted by Claude Code (session jackmccarthy-da). |
- The README keeps #454's mathlib_declaration and mathlib_file rows with #459's wording, and this branch's proved/fully_proved paragraph, which now names the Assumes row of the statement box as #459 does. - #453's generator sentence, in a section this branch moved, goes to reference/search.md: tested on 4.34.1 and 4.35.0, CI runs its real tests on 4.35.0. - CHANGELOG keeps this branch's Docs and Claims entries and adds main's Render entry. - The README budget rises by the two table rows, to 1131.
Contributor
Author
|
Head check: nothing blocks merge (reviewed at 9b2a936; last head check at 3eb1bb1). 9b2a936 merges main 63ed6bd (#424, #453, #454, #459 and #461) into this PR, which now targets main. The merge keeps everything main added since this branch's base 7e1324e:
Posted by Claude Code (session jackmccarthy-da). |
Deicyde
added a commit
that referenced
this pull request
Oct 24, 2026
#458 rewrote CONTRIBUTING.md's CI paragraph into a short pointer to tests.yml plus a list of what skips locally, so the paragraph this branch edited is gone. The resolution takes main's text: it no longer describes how a job gets its tools, and tests.yml's comment on the WebKit job says it runs in Playwright's image. This branch's changes are now tests.yml and test_release.py's pin test.
Deicyde
added a commit
that referenced
this pull request
Oct 24, 2026
Conflicts in autoform_cli/README.md and CONTRIBUTING.md, where #458 cut and condensed the docs. Both take main's text, with this branch's facts in its wording and within its line budgets: the explorer typesets its rail's and details' titles and summaries, formulas in links and buttons get no MathJax tab stop or menu, and CI's WebKit job unpacks the MathJax package too.
Deicyde
added a commit
that referenced
this pull request
Oct 24, 2026
The claim contract moved to autoform_cli/reference/claims-and-revisions.md, so this PR's README corrections now go there, within its line budget: the timeout bounds the listing's Git commands, not removing its own refs, and `claim list` and `claim cleanup` are named as the listings that stop Git with everything it started. The detail the reference has no room for, the dashboard's process group and terminal and the case-collision naming, goes into claims.py's module docstring, which #458 gave the old README text.
Deicyde
added a commit
that referenced
this pull request
Oct 24, 2026
#458 rewrote autoform_cli/README.md and moved its claim contract into autoform_cli/reference/claims-and-revisions.md. This branch's only README edit removed the sentence about the claim heartbeat, which it deletes, so the resolution takes main's README and removes that sentence where #458 moved it. Git saw no conflict there, because this branch never touched the reference page. No other doc names a function or class this branch removes.
This was referenced Oct 24, 2026
Draft
Deicyde
added a commit
that referenced
this pull request
Oct 24, 2026
#442 brought in main (the WebKit job in Playwright's container with genuine MathJax, the explorer math fix, the dead-code cleanup and the docs cut) and readable authored-area overviews for large local scopes: overview groups, scope overview flows, area return history and route trails refreshed with each projection. Conflicts, resolved so both sides' behaviour holds: - Map header: the redesign's "Title · uses N · used by M", with the overview group's area (or "Unassigned topics") in the title slot. - Views: the redesign's wording and pressed(); an open overview group reads as Map, the scope overview's root as Areas. - fit(): the redesign's frame(), linked framing and mapHeight(), with #442's decision that route detours no longer enlarge the frame and its 44px bottom inset. A frame scaled to fill the band exactly no longer counts as cropped through a rounding error. - Links: the redesign's quiet rule counts overview groups as area cards, then #442's flow mapping keeps its widths. compactRegions() counts them too, so phones keep every link. - Cards: overview groups get the area cards' meta, counts and "N topics:" summary, and a neutral frame rather than a status tint. - Reader handle: the redesign's title, swatch and titles, with ui$scopeOverview in the collapsed and close conditions. - README: #442's cut text; the theme upgrade note moved to the changelog, where #458 put the upgrade notes. Tests: #442's new scoped-overview tests read the redesign's header, card meta and handle; the dense chapter and phone first-view cases follow #442's island packing; two #442 browser-test bugs are fixed (a wait for aria-busy="false", which is never set, and a selector, .bp-reading-inner, that matches nothing); the cold-mount harness loads scopeOverviewProjection.
This was referenced Oct 25, 2026
Deicyde
added a commit
that referenced
this pull request
Oct 25, 2026
Restore the rules #458's doc cut dropped or blurred
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 #424: its base is #424's branch, and I'll retarget it to main when #424 merges. Opened above the agent-PR cap with Jack's approval.
Problem
Agents skip a file that is too long, and then the rules in it do nothing. At #424's head, after #451's cut, the CLI reference
autoform_cli/README.mdwas 2,658 lines (163 KB). The largest skills were Roadmap (292 lines), Formalize (284), Setup (232) and Human Review (143).Change
One commit per area.
autoform_cli/reference/: validation and audit, search, open statements, claims and revisions, and runtime and publication. The README keeps the article format and the commands, and ends with an index of the pages. Links into the moved sections point at the pages, and the doc checks read them.--helpcovers goes, once the help strings it relied on are filled in:claim --ttland--note, thereviewflags,project new's toolchain flags,init --autoform-refand--force,library index --timeout, andwork import-impact --module-scope.tests/test_doc_budgets.pyfails when one of these docs grows past its line count today, or when a skill or contract page has no budget.autoform_cli/README.mdautoform_cli/reference/*.md(5 new pages)skills/roadmap/SKILL.mdskills/formalize/SKILL.mdskills/setup/SKILL.mdskills/human-review/SKILL.mdSKILL.mdskills/*/references/*.mdservers/README.mdEvery command, flag, exit status, refusal, error code, default, limit, JSON key and safety rule is still stated in a doc a user or agent reads; a fact that went only into a docstring did not count. Before the cut, a critic spot-checked the planned cuts and found 13 that would have lost such a fact, among them the TeX package list, the review exit statuses, the testimony refusals and the catalog ledger rule. All 13 are kept.
Tests
__main__.py: with those stripped, the AST of all 25 changed files is identical to Test what the docs do, not their wording #424's head. The bundled audit script stays byte-identical to the template.tests/test_skill_examples.py37 passed;tests/test_doc_budgets.py2;tests/test_release.py7;tests/test_readback_testimony.py117;tests/test_lake_artifact_audit.py87, with 38 skipped for Lean;test_search's reference examples andtest_plugin_runtime's reference set.Overlap
These open PRs edit the same docs. They will conflict with this one, or have to fit the budgets once it lands:
reference/claims-and-revisions.md);