Conversation
…e shape One question, asked of six build roots in a day, found stranded work behind every one of them: proofs/lean4/Trinity.lean 9 imports 23 .lean 12 files, 15553 lines cli/tri/src/main.rs 27 mod 33 .rs elab.rs, 4 tests bootstrap/src/main.rs 44 mod 97 .rs 7 files, 7 gate bodies coq/_CoqProject 9 .v 11 .v 486 lines, 0 Admitted Cargo.toml members 5 crates 6 crates cli/tri-mcp, 996 lines MERGE_CRITICAL 15 workflows 47 both actual offenders A build system prints the work it did. A coverage claim is about the work it did not, and nothing prints that: `lake build` never names a file it skipped, and `cargo build` cannot error on a file it does not compile. The section records what makes it hard to see rather than only the recipe. A red build hides it behind a loud unrelated failure. A `paths:` filter attaches a green check to the commit that edited the uncompiled file. Orphan subtrees import each other busily, so undirecting the edges reports zero and reads as good news. And the count going DOWN is the silent direction -- 358 tests to 354, with no gate reading that number. Refs #2895 Refs #2900
# Conflicts: # .claude/skills/ci-gates/SKILL.md
gHashTag
changed the title
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This was referenced Aug 29, 2026
# Conflicts: # .claude/skills/ci-gates/SKILL.md
gHashTag
changed the title
gHashTag
enabled auto-merge (squash)
August 29, 2026 22:47
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:49:23 UTC
Summary
Seal Status
|
Contributor
PR DashboardGenerated at: 2026-08-29 22:59:29 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. |
Contributor
PR DashboardGenerated at: 2026-08-29 23:01:54 UTC
Summary
Seal Status
|
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 question asked of six build roots, in a day:
proofs/lean4/Trinity.lean.leancli/tri/src/main.rsmod.rselab.rs, 319 lines, 4 testsbootstrap/src/main.rsmod.rscoq/_CoqProject.v.vAdmittedCargo.tomlmemberscli/tri-mcp, 996 linesMERGE_CRITICALIssues: #2895, #2900, #2902, #2903, #2904, #2905.
A build system prints the work it did. A coverage claim is about the work it did
not, and nothing prints that.
The section is mostly about what makes this hard to see:
H4Lagrangian.leanwhile thefact was that
Icarusappears zero times in 483 lines of log.paths:filter is worse than silence.coq/**means editing anuncompiled
.vtriggers the workflow, which compiles the nine listed files andattaches a green check to that commit.
Lean files import each other. Undirecting the edges reports zero.
sorrycounted bylean-proofs.ymlare in files nothing opens.Refs #2895
Refs #2900