Delete unreachable helpers and redundant tests, and lock-check CI's sync by Deicyde · Pull Request #423 · facebookresearch/autoform-bot

Deicyde · 2026-10-21T08:28:48Z

Problem

This is part of the stabilization Jack approved on 2026-10-20 (rules in #418). A read-only inventory of main found:

code no entry point reaches, and methods that only tests call;
tests that repeat each other or restate production constants;
a CI gap: the test job's plain uv sync rewrites a stale uv.lock before the suite's lock-freshness checks run, so those checks cannot fail.

Change

There is one commit per item, so any one can be dropped.

Code:

Delete lean.project_source_revision, lean.strip_lean_comments and skeleton.source_excerpt. Nothing outside tests calls them.
Delete ClaimBoard.heartbeat with Heartbeat and CLAIM_HEARTBEAT_S, ClaimBoard.holds, acquire's steal flag, DeclarationSkeleton.defines, and ProjectResourceCache.lease and invalidate. Their tests now use the _resolved variants that production uses. The README sentence on heartbeats goes too.

Tests:

Fold 28 same-shape coverage-contract tests into two tables. Every case is kept, and each row id is the old test's name.
Trim parametrize tables that restate production constants down to a few rows per rule.
Move the claim CLI tests into test_claims.py, and keep one real-Lean gate in conftest.py.
Drop four render tests that re-test coverage parsing, the Graph pickling and aliasing tests, four import-only server tests, absence checks for paths that never existed, and a duplicated byte-identity test.

CI:

The test job syncs with --locked, so a stale uv.lock now fails CI instead of being rewritten.
Drop the dev extra's duplicate pymdown-extensions requirement. The runtime pin already fixes the version.

Net: 23 files, +539/-1,321.

Kept on purpose

load_skeleton_report, because Label statement approvals by the repository's code-owner review policy #219 calls it.
publication_source_revision, because Scale roadmap inventories and the full DAG explorer #90, Retire generated Mermaid: a Markdown dependency summary and locked-down authored diagrams #378 and Clean up the dependency explorer's design #411 test it.
focus_view, because Scale roadmap inventories and the full DAG explorer #90 deletes it itself.
LeanLspSession.abort, because its tests have no public replacement.
The portable-capture xfail, because Windows stays supported.
Debrief: Jack wants it integrated better, not cut.

Test

ruff and compileall pass, and uv lock --check passes.
Every deleted name was grepped across the repository and every open PR head.
pytest did not run locally because of machine load, so CI is the full check.
Merging this adds no conflicted file to any open PR.

Remove lean.project_source_revision, lean.strip_lean_comments and skeleton.source_excerpt with their __all__ entries. git grep finds no caller in autoform_cli, servers, skills, templates, docs or the bundled example, and no open PR adds one. project_source_revision had no caller at all. The strip_lean_comments tests now run the same inputs, with the same expected strings, through _without_lean_comments, which audit uses. The source_excerpt asserts only exercised the deleted helper. load_skeleton_report stays because #219 calls it, and publication_source_revision stays because #90, #378 and #411 add tests on it. focus_view is left for #90, which deletes it itself.

Remove ClaimBoard.heartbeat with the Heartbeat class and CLAIM_HEARTBEAT_S, ClaimBoard.holds, acquire's steal flag, DeclarationSkeleton.defines, and ProjectResourceCache.lease and invalidate, plus the README sentence on heartbeats. The CLI never starts a heartbeat or steals a lease, and the runtime only calls lease_resolved and invalidate_resolved. git grep finds no use outside tests in autoform_cli, servers, skills, templates, docs or the bundled example, and no open PR head adds one. The heartbeat tests and steal cases are gone. Ownership checks use a test helper over read and expired, the stale-release test plants the concurrent lease directly, and the runtime tests lease the resolved root. LeanLspSession.abort stays: 17 test calls and a test of its serialization with close have no public replacement.

TestReplServer.test_import_server, test_import_core, test_import_pool and TestLspServer.test_import_server only imported a module. The same modules are imported at module scope by test_lsp_protocol, test_batch_diagnostics, test_repl_pool_lifecycle, test_repl_core_protocol and test_plugin_runtime, and test_create_server in the same classes imports them again, so a broken import still fails collection. No open PR references these tests.

test_graph_pickles_only_public_types re-tested the standard pickle module on a plain dataclass of builtins, and test_graph_keeps_the_callers_plain_node_mapping asserted that late insertions into the caller's dict show up in children(). git grep finds no pickle, process pool or copy use in autoform_cli or servers, and no code mutates Graph.nodes after construction. Both guarded a per-Graph cache that 89b7bc2 removed. No open PR touches these lines.

The multiline-comment, fenced-block, hidden-header and one-broken-link render cases repeated coverage parsing. test_coverage.py covers each input: test_a_blank_line_inside_a_comment_cannot_shrink_the_contract, test_a_blank_line_inside_a_fence_cannot_shrink_the_contract, test_a_comment_adding_a_pipe_to_the_header_is_rejected and test_every_decomposition_link_must_resolve_not_merely_one. test_render_rejects_invalid_coverage_before_touching_output still pins that render refuses a bad contract before writing, and the missing-anchor case stays. No open PR edits or references these four tests.

The wheel test asserted that autoform_cli/lake.py and scripts/, autoform/, visualization/, servers/lean/ and servers/search/ are absent. None of those paths is in git ls-files or in any open PR head, and the wheel packages only autoform_cli and servers. The Codex prompt check for 'claim-backed workers' pinned wording no file contains. test_example_and_template_helpers_are_identical repeated the first assertion of test_example_workflows_match_the_scaffold_templates in test_skill_examples.py. test_main_plugin_surface_excludes_deicyde_orchestration now checks only the shipped skills, MCP servers and manifests, so it is renamed test_plugin_manifests_list_the_shipped_skills_and_servers. No workflow, doc or open PR diff refers to the old name.

test_skeleton.py and test_impact.py each carried a copy of _lean_toolchain_available; the second said it repeated the first. Both read the skeleton fixture's lean-toolchain, so the one copy now lives in tests/conftest.py and both modules import it. test_contract, test_lake_artifact_audit and test_lsp_protocol still import the name from tests.test_impact, which re-exports it; an import smoke test confirms all five modules see the same function. test_impact's orphaned os import goes. No marker or CI change, and no open PR edits the removed lines.

All 11 tests from tests/test_claim_cli.py now sit at the end of tests/test_claims.py. They use that file's board_repo fixture, _git, _plant_message and _plant_ref_lock in place of their own bare-repo, commit and lock helpers, and reach CLAIM_REF_PREFIX, ClaimBoard and author_claim_key through the claims module. No workflow, doc or open PR names test_claim_cli.py, and no open PR edits either file. The graph-view files and test_cli.py stay apart because #90 and #378 edit them.

The Lean indexing tables in test_lean_sources.py re-listed most of _COMMAND_HEADS; they now keep one row per rejection path: a non-identifier start, a modifier, a command head followed by nothing, a word, a colon, a bar or a binder, an unknown command the signature grammar rejects, and a multi-line command (56 to 20 commands, 27 to 16 names, 9 to 7 continuations, 11 to 10 signatures). An ast script confirms that every rejection category of the old command and name tables still has a row. test_project_create.py's package table no longer repeats every reserved root (test_every_release_has_creation_contracts pins the full set); it keeps a dependency root, a toolchain root, a toolchain extra root, a Lean sort, and case-folded spellings. The toolchain and Mathlib revision tables keep one row per rule of _LEAN_TOOLCHAIN and _valid_mathlib_revision. The C0 separator test in test_project_inspect.py keeps U+001C and U+001F on both sides. No test is removed and no open PR edits these tables.

28 tests in test_coverage.py each wrote one coverage file, called load_coverage and asserted on the summary and the reasons, lines or (line, reason) pairs. They are now rows of test_coverage_contract_is_rejected (22 rows) and test_coverage_contract_is_accepted (7 rows); each row id is the old test name, and the fragment test splits into its rejected and accepted halves. An ast script checked that every row writes byte-for-byte the contract its old test wrote, creates the same roadmap article, and expects the same reasons, substring, lines and summary fields. Tests starting between lines 550 and 660, which open PR #90 edits, and the imports and helpers at the top of the file are unchanged.

The test job ran a plain `uv sync`, which rewrites a stale uv.lock inside the runner before pytest starts. The suite's lock checks in tests/test_lock_platforms.py then read the rewritten file and passed, so a dependency or version bump without a lock refresh could merge green. With --locked, the job fails instead. The other jobs keep --frozen; one job checking is enough.

The runtime dependencies pin pymdown-extensions==11.0.1, so the dev extra's looser >=11.0.1,<12 can never select another version. uv.lock loses only the two entries for it; uv lock --check passes.

Deicyde · 2026-10-21T22:49:37Z

Review at 33724dd: nothing blocks merge. One round, read-only.

The deleted code is unreachable. None of the deleted names (project_source_revision, strip_lean_comments, source_excerpt, the heartbeat helpers, holds, steal, defines, ProjectResourceCache.lease and invalidate) has a caller outside tests on main, counting string and getattr uses, and no open PR's added lines use one. The one production caller of acquire passes keywords, so dropping steal doesn't affect it.
Coverage is kept. The 28 coverage tests folded into the two tables write byte-identical contracts row for row. The moved claim CLI tests differ only in shared fixtures. Each dropped test's behaviour is still checked elsewhere, apart from the note below.
CI's lock check works. Both test jobs ran uv sync --locked --extra dev --extra repl against the committed lock, so a stale uv.lock now fails before ruff or pytest runs. The other jobs keep uv sync --frozen and pass. 33724dd changes only dev-extra metadata in the lock: the same 110 packages and the same installed counts as main.
Freeze: no command, flag, JSON key or schema is added; the production changes only delete.
CI: all 7 checks pass. Against main de6de5f: test (3.10) 3871 to 3753, test (3.13) 3870 to 3752, Windows 298 to 294 (the C0-separator trim), real-Lean audit 120 to 119 (the dropped byte-identity duplicate). The other real-Lean suites are unchanged.

Note:

Two dropped rows tested their own regex branches (tests/test_project_create.py:614). 15b14bd removes "v4.030.0" and "v4.30.00", the only cases for the minor and patch alternations of _LEAN_TOOLCHAIN (create.py:41-44); only the major case "v04.30.0" is left. Loosening minor and patch to [0-9]{1,9} passes the trimmed suite. The commit message says the table keeps one row per rule, and putting the two rows back makes that true.

tests/test_skeleton.py's import list conflicted: this branch drops source_excerpt, which it deletes, and main adds stale_build_said, which stays. Nothing merged from main uses a name this branch deletes.

The table trim kept only the major part's leading-zero case (v04.30.0), so loosening the minor or patch part of _LEAN_TOOLCHAIN still passed. v4.030.0 and v4.30.00 come back, one row for each rule, as the trim meant to keep.

Deicyde · 2026-10-21T23:24:33Z

Thanks. The note is taken in 1d7a3cc: v4.030.0 and v4.30.00 are back in the toolchain table, one row for each leading-zero rule. The test passes, 17 cases run directly.

…-tests

Deicyde · 2026-10-22T00:44:05Z

Head check: the review holds; ready to merge once CI finishes (reviewed at cd8d792; review at 33724dd).

Since the review: 1d7a3cc, which takes the note (two toolchain rows), and two merges of main, one bringing Scale roadmap inventories and the full DAG explorer #90.
None of the deleted names (project_source_revision, strip_lean_comments, source_excerpt, holds, steal, defines, lease, invalidate, the heartbeat helpers) is called anywhere in autoform_cli, servers or tests at this head, so the merges brought in no new caller.
test (3.10) and test (3.13) pass at this head.

Posted by Claude Code (348 worker session).

- claims.py: main's new bounded `list(keys, *, timeout, progress)` stays, and holds goes as before. `import threading` stays, because #446's timeout code uses it (jackmccarthy-da spotted that git would drop it). - tests/test_claim_cli.py stays deleted. #446's seven new claim CLI tests and its stderr assertion move into test_claims.py beside the other moved CLI tests, using its board_repo fixture. - test_claims.py keeps #446's new tests ahead of the moved CLI tests. - test_impact.py keeps #449's import-closure CLI test and imports the one real-Lean gate from conftest. Nothing in autoform_cli, servers or tests uses a name this branch deletes.

Deicyde · 2026-10-22T20:56:31Z

Head check: nothing blocks merge (reviewed at 79960c6; last head check at cd8d792). It is ready once the WebKit and skeleton-suite jobs, still running, pass.

79960c6 merges main with #446 and #449. Its resolution:

claims.py. Delete unreachable helpers and redundant tests, and lock-check CI's sync #423's deletions stay deleted: Heartbeat, CLAIM_HEARTBEAT_S, heartbeat, holds and acquire's steal. Bound claim list and let it list only named targets #446's list(keys, *, timeout, progress) is kept, and so is import threading, which Bound claim list and let it list only named targets #446's timeout guard uses (L21, L330). Nothing in autoform_cli, servers or tests uses a deleted name.
The claim tests. All 18 of main's test_claim_cli.py tests are now in test_claims.py, the seven Bound claim list and let it list only named targets #446 added among them. Their bodies match main's except for the board_repo fixture and the claims. prefix. Of main's 118 test_claims.py tests, only the five heartbeat tests are gone, along with the class they tested.
test_impact.py. It keeps Let import-impact load only a module's candidate importers #449's tests, adds or drops none, and takes the real-Lean gate from tests/conftest.py. The whole suite collects (4,471 tests).
CI. The test jobs and the real-Lean job pass.

Note: test_list_lists_claim_keys_that_differ_only_in_case_on_any_filesystem fails both ways on macOS here, and on main deb2868 too. It comes from #446, not from this PR, and CI runs it only on Linux. Reported as #452.

Posted by Claude Code (session jackmccarthy-da).

…-tests

Deicyde · 2026-10-22T22:11:43Z

Head check: nothing blocks merge (reviewed at 6ac6cfc; last head check at 79960c6). Every check passes except WebKit, which timed out installing system packages before any test ran, for the reason below.

6ac6cfc merges main a840c3f (#450 and #443). Its remerge diff is empty: Git resolved nothing and the merge adds no edits.

Share builds across checkouts through Lake's artifact cache #450 and this PR both touch skeleton.py. On the merged tree, tests/test_skeleton.py and tests/test_project_create.py pass locally (507 passed, 53 skipped), ruff passes, and the whole suite collects (4,630 tests).
CI passes the test, real-Lean, skeleton-suite, REPL, Windows and MathJax jobs.

The WebKit job. It has hit its 15-minute limit five times, across two runs, each time inside playwright install --with-deps webkit, while apt fetched WebKit's 117 MB of Ubuntu packages.

Not the PR. This PR's only CI change is --locked on the test job's uv sync. The browser job, its Playwright pin (1.62.0) and its apt plan (181 packages) are identical to main's.
The region. All five timed-out jobs ran on Azure runners in westus or westus3. The fast runs in the same window, on main and Cut repeated and internal prose from the CLI reference and skills #451, ran in centralus, fetched the same 117 MB from azure.archive.ubuntu.com, and passed in about a minute.

Running the job in the Playwright image, which the lead is testing on a scratch branch, removes the apt step.

Posted by Claude Code (session jackmccarthy-da).

#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.

Deicyde · 2026-10-24T03:56:31Z

Merged main (7677dbf, with #458) at 0585e57, at Jack's request.

The README conflict. The only conflict was in autoform_cli/README.md, which Cut the docs agents read, split the CLI reference, and give them line budgets #458 rewrote. This PR's one README edit removed the sentence about the claim heartbeat it deletes, so the resolution takes main's README.
The moved sentence. Cut the docs agents read, split the CLI reference, and give them line budgets #458 had moved that sentence into autoform_cli/reference/claims-and-revisions.md, where Git saw no conflict, because this PR never touched that page. The merge removes it there.
Other docs. No other doc names a function or class this PR removes.

Locally:

ruff passes, and the suite collects (4,625 tests).
tests/test_skeleton.py, test_claims.py, test_doc_budgets.py, test_skill_examples.py and test_lean_sources.py pass (812). The only exceptions are the two Claims: list() merges two claim keys that differ only in case on a case-insensitive filesystem #452 tests, which fail on main too on macOS with Apple Git; Keep a claim listing's git in reach of signals, and list case-only keys on any Git #457 fixes them.

CI is running.

Posted by Claude Code (session jackmccarthy-da).

Deicyde · 2026-10-24T07:26:07Z

Head check at 0585e57 (merge of main 7677dbf, #458): nothing blocks merge. The merge leaves the PR's own diff as reviewed. Its 21 other files are unchanged line for line, and README resolved to main's text. The heartbeat sentence #423 deletes is now deleted, with the same lines, from autoform_cli/reference/claims-and-revisions.md, where #458 moved it. CI is green at 0585e57, 9 of 9: https://github.com/facebookresearch/autoform-bot/actions/runs/40060328696

Posted by PR swarm: PR Swarm Lead

Deicyde added 12 commits October 21, 2026 04:27

Drop the dev extra's duplicate pymdown-extensions requirement

33724dd

The runtime dependencies pin pymdown-extensions==11.0.1, so the dev extra's looser >=11.0.1,<12 can never select another version. uv.lock loses only the two entries for it; uv lock --check passes.

meta-cla Bot added the CLA Signed This label is managed by the Meta Open Source bot. label Oct 21, 2026

Merge main, with #90, into the dead-code and test cleanup

2314808

tests/test_skeleton.py's import list conflicted: this branch drops source_excerpt, which it deletes, and main adds stale_build_said, which stays. Nothing merged from main uses a name this branch deletes.

This was referenced Oct 21, 2026

Deploy Pages only from the commit autoform verify passed on main #399

Merged

Bump certifi from 2026.7.22 to 2026.10.19 #436

Merged

Merge remote-tracking branch 'origin/main' into cleanup/dead-code-and…

cd8d792

…-tests

Deicyde mentioned this pull request Oct 22, 2026

Keep the audit probe's Lean in a Lean file #441

Merged

Deicyde marked this pull request as ready for review October 22, 2026 05:03

Deicyde marked this pull request as draft October 22, 2026 20:21

Deicyde mentioned this pull request Oct 22, 2026

Claims: the dashboard's claim listing leaves git running after Ctrl+C or SIGTERM #447

Closed

Merge remote-tracking branch 'origin/main' into cleanup/dead-code-and…

6ac6cfc

…-tests

Deicyde mentioned this pull request Oct 22, 2026

Run the WebKit job in Playwright's pinned image #456

Merged

This was referenced Oct 22, 2026

Keep a claim listing's git in reach of signals, and list case-only keys on any Git #457

Merged

Cut the docs agents read, split the CLI reference, and give them line budgets #458

Merged

Deicyde marked this pull request as ready for review October 24, 2026 01:53

Deicyde merged commit 9dbf498 into main Oct 24, 2026
9 checks passed

Deicyde deleted the cleanup/dead-code-and-tests branch October 24, 2026 08:06

Navigation Menu

Repository navigation

Delete unreachable helpers and redundant tests, and lock-check CI's sync - #423

Delete unreachable helpers and redundant tests, and lock-check CI's sync#423
Deicyde merged 18 commits into
mainfrom
cleanup/dead-code-and-tests

Deicyde commented Oct 21, 2026

Uh oh!

Deicyde commented Oct 21, 2026

Uh oh!

Deicyde commented Oct 21, 2026

Uh oh!

Deicyde commented Oct 22, 2026

Uh oh!

Deicyde commented Oct 22, 2026 •

edited

Loading

Uh oh!

Deicyde commented Oct 22, 2026

Uh oh!

Deicyde commented Oct 24, 2026

Uh oh!

Deicyde commented Oct 24, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

Deicyde commented Oct 21, 2026

Problem

Change

Kept on purpose

Test

Uh oh!

Deicyde commented Oct 21, 2026

Uh oh!

Deicyde commented Oct 21, 2026

Uh oh!

Deicyde commented Oct 22, 2026

Uh oh!

Deicyde commented Oct 22, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Deicyde commented Oct 22, 2026

Uh oh!

Deicyde commented Oct 24, 2026

Uh oh!

Deicyde commented Oct 24, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Deicyde commented Oct 22, 2026 •

edited

Loading