chore(repo): 315 MB of scratch was tracked in a directory .gitignore declares ignored - #2489
Closed
noahgift wants to merge 1 commit into
Closed
chore(repo): 315 MB of scratch was tracked in a directory .gitignore declares ignored#2489noahgift wants to merge 1 commit into
noahgift wants to merge 1 commit into
Conversation
noahgift
enabled auto-merge
August 15, 2026 09:20
…declares ignored
`.gitignore:62` says `**/.pmat-work/`. Git tracked 461 of those files anyway --
315 MB, dominated by 140 pmat per-ticket `contract.json` files at ~5 MB each,
dated April, each recording a baseline commit. Classic add-before-ignore: the
pattern was written after the files were staged and `git rm --cached` was never
run. Every clone paid the checkout cost.
Verified nothing reads them before removing: no hit in the Makefile, any
workflow, `scripts/`, any `.rs` file, or any pmat config -- with a positive
control proving the searches work (the same greps find `scripts/` in 15 Makefile
lines and 6 workflows, and `contracts/` in 628 Rust files). `cargo check` after
removal is clean. Files stay on disk; only the index changes.
Honest about the benefit: this removes the CHECKOUT cost for new clones, not the
download. History still carries the blobs, so `size-pack` stays 265 MiB. Fixing
that means rewriting history, which is not something to do quietly.
Guard added, RATCHETED at 320 rather than driven to zero, because the remaining
ignored-but-tracked files are not all removable:
* `proptest-regressions/*.txt` are matched by `.gitignore:22` and MUST stay
tracked -- each records a failing proptest seed so that regression is
re-tested forever. There the ignore RULE is what is wrong, not the tracking.
A blanket "remove everything ignored-but-tracked" would have silently
discarded the repo's regression seeds.
* `.pmat-metrics/` (208 files), `benchmark-results/`, and Lean run logs are
scratch too, but each needs its own "does anything read this" check.
781 -> 320. Mutation-verified: force-add one ignored file -> RED naming the
growth 320 -> 321; removed -> GREEN. Self-test has a positive control row
proving it reports only the ignored file and not every tracked file.
Refs #2481
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
noahgift
force-pushed
the
fix/tracked-ignored-scratch
branch
from
August 18, 2026 17:12
3963d3d to
aeddfa2
Compare
noahgift
added a commit
that referenced
this pull request
Aug 19, 2026
Contributor
Author
|
Landed via #2537 (batch B), squash-merged as |
auto-merge was automatically disabled
August 19, 2026 21:45
Pull request was closed
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.
.gitignore:62says**/.pmat-work/. Git tracked 461 of those files anyway --315 MB, dominated by 140 pmat per-ticket
contract.jsonfiles at ~5 MB each,dated April, each recording a baseline commit. Classic add-before-ignore: the
pattern was written after the files were staged and
git rm --cachedwas neverrun. Every clone paid the checkout cost.
Verified nothing reads them before removing: no hit in the Makefile, any
workflow,
scripts/, any.rsfile, or any pmat config -- with a positivecontrol proving the searches work (the same greps find
scripts/in 15 Makefilelines and 6 workflows, and
contracts/in 628 Rust files).cargo checkafterremoval is clean. Files stay on disk; only the index changes.
Honest about the benefit: this removes the CHECKOUT cost for new clones, not the
download. History still carries the blobs, so
size-packstays 265 MiB. Fixingthat means rewriting history, which is not something to do quietly.
Guard added, RATCHETED at 320 rather than driven to zero, because the remaining
ignored-but-tracked files are not all removable:
proptest-regressions/*.txtare matched by.gitignore:22and MUST staytracked -- each records a failing proptest seed so that regression is
re-tested forever. There the ignore RULE is what is wrong, not the tracking.
A blanket "remove everything ignored-but-tracked" would have silently
discarded the repo's regression seeds.
.pmat-metrics/(208 files),benchmark-results/, and Lean run logs arescratch too, but each needs its own "does anything read this" check.
781 -> 320. Mutation-verified: force-add one ignored file -> RED naming the
growth 320 -> 321; removed -> GREEN. Self-test has a positive control row
proving it reports only the ignored file and not every tracked file.
Refs #2481
Co-Authored-By: Claude Opus 5 noreply@anthropic.com