Skip to content

feat: add script/count-blocked-by-build-error#13471

Open
kim-em wants to merge 1 commit intoleanprover:masterfrom
kim-em:count-blocked-by-build-error
Open

feat: add script/count-blocked-by-build-error#13471
kim-em wants to merge 1 commit intoleanprover:masterfrom
kim-em:count-blocked-by-build-error

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Apr 19, 2026

This PR adds a standalone Python script that wraps lake build, captures its output, and for each failed module reports how many modules in the selected lean_libs transitively import it. The count is an upper bound on how many downstream modules were blocked by the failure in the workspace.

The script enumerates modules via lake query <lib>:modules, builds the forward import graph using batched lake query +M:imports --json calls, and inverts it locally. A batched query that fails (e.g. because one module has an unparsable header) is bisected down to singletons so one bad file doesn't drop the whole report.

Example output:

$ script/count-blocked-by-build-error --lib Mathlib -- Mathlib.Topology.Basic
...lake build output streamed here...
Some required targets logged failures:
- Mathlib.Topology.Basic
error: build failed

Enumerating selected-library modules...
Building import graph for 5043 modules...

Selected-library dependents:
  Mathlib.Topology.Basic: 1842

This is a follow-up to #13454 (which added lake build --summary). The original issue #13316 asked for blocked-downstream counts inside Lake itself; moving that computation to a standalone script keeps Lake's build-reporting path minimal and avoids re-parsing every workspace module from within the build runner.

🤖 Prepared with Claude Code

@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 19, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Apr 19, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 80cbab16420b90104647a795a18f9890fd8150e8 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-19 07:27:05)
  • ✅ Mathlib branch lean-pr-testing-13471 has successfully built against this PR. (2026-04-21 03:06:37) View Log

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 19, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 80cbab16420b90104647a795a18f9890fd8150e8 --onto 3fc99eef102549c743c6c63547983319bfae6f01. You can force reference manual CI using the force-manual-ci label. (2026-04-19 07:27:06)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-21 02:09:32)

This PR adds a standalone Python script that wraps `lake build`, captures its
output, and for each failed module reports how many modules in the selected
`lean_lib`s transitively import it. The count is an upper bound on how many
downstream modules were blocked by the failure in the workspace.

The script enumerates modules via `lake query <lib>:modules`, builds the
forward import graph using batched `lake query +M:imports --json` calls, and
inverts it locally. A batched query that fails (e.g. because one module has an
unparsable header) is bisected down to singletons so one bad file doesn't drop
the whole report.

This is a follow-up to leanprover#13454 (which added `lake build --summary`). The
original issue leanprover#13316 asked for blocked-downstream counts inside Lake itself;
moving that computation to a standalone script keeps Lake's build-reporting
path minimal and avoids re-parsing every workspace module from within the
build runner.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@kim-em kim-em force-pushed the count-blocked-by-build-error branch from 9730091 to b8636c4 Compare April 21, 2026 01:20
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 21, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Apr 21, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-other mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants