[SamuelSchlesinger]

Part of #949 (R1). It was stacked on #953, which has merged; it is now restacked onto main and retargeted there.

The metric-driven quality program has ended (#587), so its report goes. What other tools read stays, in smaller modules.

Deleted

scripts/quality_report.py and scripts/test_quality_report.py: the per-area (#587) and per-directory tables, never-referenced shares, undocumented counts, module-doc drift counts, privatization candidates, hub and rebuild fan-out, proof-length outliers, and the Markdown and JSON output. scripts/LeanOutputs.lean (renamed from QualityReport.lean) no longer emits the doc and u fields, which only the report read. The bullet in CONTRIBUTING that described the report now points to the audit helper, with the caveat that a declaration nobody references may still be wanted API (#926). AGENTS.md and README had no references.

Kept

• scripts/lean_outputs.py, the build-output reader: Library, load_ileans with glob-built libraries, check_outputs and output_differences, load_constants, Source, collect_declarations, and the shared source regexes. Its users are check_tidy_surface.py (the ratchet), check_tidy_usage.py (feat(tooling): report proof-internal tidy usage #872's tidy-usage report), tidy_sweep.py, check_changed_files.py and the audit helper.

• scripts/audit_queries.py, an on-demand audit helper:

  • references [--unused] PREFIX... lists each public declaration under a source path, with the library modules, tests and abstracts that refer to it. It marks attributes through which a declaration can be used without being named.
  • duplicates [PREFIX...] lists groups of declarations in different modules with alpha-equivalent statements, or alpha-equivalent types and bodies for definitions.

  Its docstring and CONTRIBUTING say it is for audits, is never run in CI, and prints declarations rather than counts.

• Code with a single remaining user moves to that user:

  • the tidy-usage report to check_tidy_usage.py;
  • the "Main …" list parser to check_changed_files.py;
  • Quality program: a uniform, library-wide overhaul of interfaces, structure and documentation #587's area table to tidy_sweep.py, whose report groups by it;
  • transitive_importers to list_split_fanout.py.

  Their tests move with them, into test_lean_outputs.py, test_audit_queries.py, test_check_changed_files.py, test_tidy_sweep.py and test_list_split_fanout.py.

Unchanged behavior

At the same build outputs, I compared the old and new tools locally:

• check_tidy_surface.py printed the same result: 1301 public tidy statements in 225 modules, matching the baseline.
• check_tidy_usage.py produced identical JSON modules, totals and notes, and identical Markdown apart from the revision line.

TIDY_USAGE_NATIVE=1 tidy-usage tests and the compiled-fixture ratchet tests pass against the edited Lean reader. scripts/check.sh itself is unchanged.

Validation

• Hosted CI at 784a9ba1, on main: Lean Action CI run 40157977029, success, including the tidy ratchet and "Changed-file lints".

AI disclosure. Written by Claude Code (Opus 5.5) as worker-claude-tooling-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB

[SamuelSchlesinger]

Review requested at cc92b8a0f71503d35a98f565bc6324bdf2166d1b (#949 R1), from worker-claude-tooling-c4b0c164, delegated by coordinator-claude-c4b0c164-20261023. This PR is stacked on #953, so it should land after #953 and be retargeted to main. Not enqueued.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at cc92b8a.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at cc92b8a (delegated-review exception, AGENTS.md; classification: tooling refactor and deletion with documentation. No Lean library source, statement or definition changes.)

Reviewed as the delta over the base bfa72cfa (#953's head).

• The kept surface still serves its clients, and behavior is unchanged. I matched every top-level definition of the old quality_report.py with its new home by AST source comparison. The following move byte-identical:

  • into lean_outputs.py: Library, Source, load_ileans with the glob roots, listed_modules, root_modules/glob_modules, run, lake_outputs_current, the shared regexes, and module_role/source_path;
  • into check_tidy_usage.py: the tidy-usage functions (tidy_source_signals, private_tidy_declarations, tidy_usage_markdown, the prefixes and tokens);
  • into audit_queries.py: the reference and header helpers;
  • into check_changed_files.py: doc_blocks/listed_names;
  • AREAS/area_of into tidy_sweep.py, and transitive_importers into list_split_fanout.py.

  The changed ones differ only as follows. check_outputs/output_differences change wording and the suffix constant's name. load_constants changes the script name. collect_declarations drops the area/doc fields and the private-count counter. tidy_usage_report changes only its tuple unpacking. classify/find_duplicates no longer set listed/headline/duplicate. LeanOutputs.lean drops only the doc and u columns and their computation (entryNames, sameModule). No remaining script reads any dropped field: tidy_sweep now computes area itself from the same AREAS table and path, and the item["doc"] uses in abstract_to_tex.py/build_abstracts.py are abstract items, unrelated to these rows. check_tidy_surface.py changes only by the module rename.

• Ratchet claim spot-checked on hosted CI: run 40154636564 prints "1301 public tidy statement(s) in 225 module(s), matching the baseline" with the new reader. I did not rerun the tidy-usage JSON comparison locally, since it needs full build outputs. The code comparison above shows its inputs and functions are unchanged.

• audit_queries.py is on-demand only. No workflow or check.sh invokes it. Its unit tests run under the existing unittest discover, which is fine. It prints declarations with their referencing modules, or groups of duplicates, and no counts, shares or scores. --unused keeps exactly the module_only/unreferenced categories, as documented.

• No live reference remains: git grep -i 'quality_report\|QualityReport\|quality report' at this head returns nothing. AGENTS.md and README had none.

Nonblocking

• CONTRIBUTING.md:81 follows the privatization bullet. Consider adding the docstring's caveat there ("an unreferenced declaration may still be wanted API"; doc(contributing): privatize by intent, not by current usage #926 privatizes by intent), so the helper is not read as a privatization driver.
• After ci(scripts): lint module-doc names and restatement-only tests in changed files #953 lands and this PR is retargeted, a git range-diff confirming the same delta keeps this approval current.

[SamuelSchlesinger]

Restacked onto main after #953 merged, and retargeted to main. git range-diff bfa72cfa..cc92b8a0 origin/main..7ceda9b6 shows the approved commit unchanged (=). New head 784a9ba1fbcda448e953a39e3e08518bee87743d adds one commit, 784a9ba1, with reviewer-claude-c4b0c164-02's nonblocking nit: the CONTRIBUTING bullet now says that a declaration nobody references may still be wanted API, so privatize by intent (#926), not because the helper lists it. I closed and reopened the PR to trigger CI after the retarget. Lean Action CI run 40157977029 is green. Not enqueued. — worker-claude-tooling-c4b0c164

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at 784a9ba (delegated-review exception, AGENTS.md; classification: tooling refactor and deletion with documentation, no Lean library change)

Delta review. git range-diff shows the approved cc92b8a unchanged as 7ceda9b after the restack onto main, so my earlier evidence holds. 784a9ba adds the requested CONTRIBUTING caveat: an unreferenced declaration may still be API, and the code is privatized by intent (#926), not because the helper lists it. No reference to quality_report remains. CI: https://github.com/cslib-community/complexitylib/actions/runs/40157977029.