The local checkout of this repo carries 245 uncommitted modified files. They are not residue.
They are the only existing cure for a defect that makes 42 tracked source files unparseable on
origin/main, and any tree-cleaning command destroys them.
The measurement (Idris2 0.7.0, pristine origin/main via git archive)
Detector over src/**/*.idr |
Files |
Occurrences |
Raw grep (^|[[:space:]])postulate[[:space:]] |
46 |
369 |
| Declaration position only (comments excluded) |
42 |
360 |
| Comment-only mentions |
4 |
9 |
| Local working tree, declaration position |
0 |
0 |
postulate is not an Idris2 keyword — v0.7.0 answers Couldn't parse declaration, rc=1, and it
is absent from the changelog for v0.2.0–v0.8.0. It was injected by 6c80e0b5
"[P1] Explicit postulate sweep (Fork A) (#189)". It also violates this repo's own register, which
states "Do NOT use the postulate keyword."
Controlled pair — src/Proven/SafeRegex/Proofs.idr, same compiler, same flags
| Tree |
Result |
pristine origin/main |
Error: Couldn't parse declaration at 25:1--25:68, rc=1 |
| local working tree |
rc=0, 0 errors |
⚠ The error coordinates point at the wrong line
Idris2 reported line 25 — well-formed prose. The offending declaration was at line 36.
A ||| docstring block attaches to the declaration that follows it, so the compiler reports the
docstring's coordinates. Anyone grepping the reported line finds prose and concludes the report is
spurious. This is why the damage survived so long.
Do not run any of these in this repo
git checkout -- . · git stash · git clean · git reset --hard
Each would re-break all 42 files. git add -A is also banned while the sweep is undisposed —
bd/ exists in the tree and must never be staged.
Relationship to #204
#204's parse-failure census measured a tree that still contained this damage (census mtime
08:31, cure 10:08). 39 of its 47 own-defect parse failures were this, not authoring defects —
corrected there. This issue is the
disposition question, not the count question: the cures are real and unmerged.
Full detail incl. reproduction commands: docs/IDRIS2-BUILD-WORK-PACKAGE.adoc §2, §8.
The local checkout of this repo carries 245 uncommitted modified files. They are not residue.
They are the only existing cure for a defect that makes 42 tracked source files unparseable on
origin/main, and any tree-cleaning command destroys them.The measurement (Idris2 0.7.0, pristine
origin/mainviagit archive)src/**/*.idr(^|[[:space:]])postulate[[:space:]]postulateis not an Idris2 keyword — v0.7.0 answersCouldn't parse declaration, rc=1, and itis absent from the changelog for v0.2.0–v0.8.0. It was injected by
6c80e0b5"[P1] Explicit postulate sweep (Fork A) (#189)". It also violates this repo's own register, which
states "Do NOT use the
postulatekeyword."Controlled pair —
src/Proven/SafeRegex/Proofs.idr, same compiler, same flagsorigin/mainError: Couldn't parse declarationat25:1--25:68, rc=1⚠ The error coordinates point at the wrong line
Idris2 reported line 25 — well-formed prose. The offending declaration was at line 36.
A
|||docstring block attaches to the declaration that follows it, so the compiler reports thedocstring's coordinates. Anyone grepping the reported line finds prose and concludes the report is
spurious. This is why the damage survived so long.
Do not run any of these in this repo
git checkout -- .·git stash·git clean·git reset --hardEach would re-break all 42 files.
git add -Ais also banned while the sweep is undisposed —bd/exists in the tree and must never be staged.Relationship to #204
#204's parse-failure census measured a tree that still contained this damage (census mtime
08:31, cure 10:08). 39 of its 47 own-defect parse failures were this, not authoring defects —
corrected there. This issue is the
disposition question, not the count question: the cures are real and unmerged.
Full detail incl. reproduction commands:
docs/IDRIS2-BUILD-WORK-PACKAGE.adoc§2, §8.