Repository navigation
Commit 5e2a003
authored
Do not keep a harness report in the library repository (#1021)
`propcheck.md` sits in the repository root. It is the output of `propcheck`,
one of the analysis harnesses that lives outside this repository, and it
arrived here because that harness wrote its report into the working directory
rather than resolving a path from its assembly. Every run since has been
invoked from elsewhere, so the file has not been touched by a run since it was
committed and says the corpus is 151 expressions and 1340 checks whether or not
that is still true.
A report nobody regenerates where they read it is worse than no report: it
carries a number with no way to tell how old the number is. The figures that
belong in this repository are the ones in
`Docs/Contributing/SimplificationContract.md`, which quotes them in prose next
to what they mean and is edited by hand when they move.
The `.gitignore` entries stop the same thing happening again for propcheck and
for the eleven other harnesses that write a report with the same shape, and
ignore the worktree directory the agents branch into, which is a full checkout
per branch and must never be added.1 parent badd7a6 commit 5e2a003
2 files changed
Lines changed: 17 additions & 13 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
58 | 58 | | |
59 | 59 | | |
60 | 60 | | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
This file was deleted.
0 commit comments