Conversation
Three passes reasoned about what `lake build` would say about the Lean
proofs. It has never compiled any of them.
`proofs/lean4/Trinity.lean` is the library root and imports nine
modules. `Trinity.IcarusLowerable.*` is not among them. The eleven files
under that directory import each other -- a closed subtree with no edge
from the root -- so `lean_lib «Trinity»` never reaches one of them.
in the build graph 7 447 lines
outside it 15 447 lines, 647 theorems
67% of the development, including all 250 `native_decide` theorems.
The two most recent runs DID fail, on `H4Lagrangian.lean` unsolved
goals. That is a real failure in the built part and a decoy: fixing it
would not add a single IcarusLowerable file to the graph. A red build on
the wrong subtree looks exactly like a red build on the right one.
The evidence was one grep of the build log: `Icarus` appears zero times
in 481 lines. Not an error about it, not a skipped target -- absent.
"The build is red" and "the build does not compile this" are different
facts, and a red build hides the second behind the first. A build graph
is a claim about coverage that nothing prints; `import` is the edge, and
the root file is the whole specification of what gets compiled.
Refs #2895
gHashTag
enabled auto-merge (squash)
August 29, 2026 21:54
Contributor
PR DashboardGenerated at: 2026-08-29 22:00:24 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.
One section from #2895.
Three passes were spent reasoning about what
lake buildwould or would not say about the Lean proofs. It has never compiled any of them.proofs/lean4/Trinity.leanis the library root and imports nine modules.Trinity.IcarusLowerable.*is not among them. The eleven files under that directory import each other — a closed subtree with no edge from the root — solean_lib «Trinity»never reaches one of them.67% of the development, including all 250
native_decidetheorems.The decoy
The two most recent runs did fail —
H4Lagrangian.lean:73and:108, unsolved goals. That is a real failure in the built part. It is also a decoy: fixing it would not add a singleIcarusLowerablefile to the graph.A red build on the wrong subtree looks exactly like a red build on the right one.
The evidence was one grep
Icarusappears zero times in 481 lines of build log. Not an error about it, not a skipped-target line — absent.When something has never been verified, ask first whether the verifier can see it: read the build's own log for the name of the thing. A build graph is a claim about coverage that nothing prints —
importis the edge, and the root file is the whole specification of what gets compiled. It is nine lines long.Refs #2895