Conversation
Lake builds a `lean_lib` from its root module and that module's transitive
imports. `proofs/lean4/lakefile.lean` names no `globs`, so the closure is the
whole build, and `Trinity.lean` -- twelve lines, nine imports -- is the whole
specification of what compiles.
Twelve files are outside it:
files lines sorry
reached by the root 11 7355 1
NOT reached 12 15553 4
`lake build` prints what it compiled and never what it skipped, so a stranded
file produces no output at all: not an error, not a warning, not a line. The
omission is invisible to the only instrument pointed at it.
Two corrections to how this was described when it was found (#2895):
- It is twelve files, not eleven. `Trinity/GoldenFloatRoundTrip.lean` is
stranded too and is not under `IcarusLowerable/`. Describing the defect as
"that subtree" was a narrative that fit the first eleven; asking the root what
it reaches finds the twelfth.
- The reachable half is 7355 lines, not the 7447 reported then.
It also re-populates a ratchet (#2898): `lean-proofs.yml` counts `sorry` by
grepping the directory while the build compiles the closure, and four of the
five it counts are in files nothing opens.
The command refuses rather than answering when it cannot: no `lean_lib` in the
lakefile, a lakefile that sets `globs` (which would make the closure the wrong
question), a missing root file, or a root that reaches only itself. A report of
zero stranded files has to mean the tree, never the parser.
Tests are mutation-checked. Undirecting the edges -- so that a file importing a
reached module counts as reached -- fails `a_file_nothing_imports_is_not_in_the_closure`,
which is the exact confusion the defect invites.
Refs #2895
Refs #2898
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 22:16:03 UTC
Summary
Seal Status
|
This was referenced Aug 29, 2026
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 22:32:03 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
gHashTag
enabled auto-merge (squash)
August 29, 2026 22:47
Contributor
PR DashboardGenerated at: 2026-08-29 22:48:26 UTC
Summary
Seal Status
|
Contributor
PR DashboardGenerated at: 2026-08-29 22:59:32 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
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
1 participant
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.
A build graph is a claim about coverage that nothing prints.
lake buildprints what it compiled. It never prints what it skipped, so a fileoutside the graph produces no output at all — not an error, not a warning, not a
line. The only way to see the omission is to ask the root what it reaches and
compare with what exists.
Two corrections to #2895
Eleven was twelve.
Trinity/GoldenFloatRoundTrip.leanis stranded and is notunder
IcarusLowerable/. Describing the defect as "that subtree" was a narrativethat happened to fit eleven of the twelve. The general question — what does the
root reach — finds the one the description lost.
7447 was 7355. The reachable line count reported when this was found was
wrong by 93.
What it changes downstream
lean-proofs.ymlcounts admitted proofs by grepping the directory. The buildcompiles the closure. Four of the five
sorryit counts are in files nothingopens, so the ceiling reads as "five admitted in a tree that builds" when it is
"one admitted in the part that builds, four in the part that does not" (#2898).
Refusals
The command answers
0 strandedonly when that is the tree. It bails on: nolean_libin the lakefile, a lakefile that setsglobs(the closure is then thewrong question), a root file that does not exist, and a root that reaches only
itself — which is far more likely to mean
importlines are not being read thanthat the library is one file.
Mutation-checked
a_file_nothing_imports_is_not_in_the_closureimportread at any indentationimports_are_read_only_at_column_zerosorrymatched without word boundariessorry_is_counted_per_line_and_delimitedThe first mutation is the defect's own invitation: eleven of the twelve stranded
files import each other busily, and that traffic is what makes the subtree look
connected to something.
Refs #2895
Refs #2898