Repository navigation
chore(abi): remove the idrisiser tree (owner decision; it never typechecked) - #154
Merged
Merged
Conversation
…hecked)
generated/idrisiser/ was the third Idris2 tree JNK-01 found: wrappers that
the idrisiser tool generated from idrisiser/*.tsig per idrisiser.toml. Its
module names were lowercase, so `idris2 --check` refused them ("Expected a
capitalised identifier, got: key"), nothing in it was ever verified, and
no ledger row depended on it. The owner decided to remove it rather than
regenerate it.
Removed: generated/idrisiser/ (6 files), idrisiser/*.tsig (3), and
idrisiser.toml. generated/ is now empty, so it goes too.
References updated:
- scripts/check-abi-tree.sh: section 7 used to print a note when
generated/idrisiser existed. It now fails if generated/idrisiser,
idrisiser/ or idrisiser.toml comes back, like the retired src/idris-abi
check, so a second ABI tree cannot return unnoticed. Negative control:
`touch idrisiser.toml` -> FAIL.
- .machine_readable/bot_directives/gitbot-fleet.a2ml: dropped from
never-touch and its note (an entry removed, nothing added).
- .machine_readable/contractiles/Mustfile.a2ml: no-dangerous-proof-escapes
greps src/abi/ only. generated-code-in-generated is removed: its check
was `test -d generated`, which fails once there is no generated code,
and the stale contractile.just never ran it anyway.
- README.adoc, PROOF-NEEDS.adoc: the idrisiser caveats now say it was
removed and why.
Left alone: CHANGELOG.adoc (generated from commits) and STATE.a2ml (A2ML
is retired estate-wide; superseded by .deed, K9 and coordination.k9).
Checks: check-abi-tree OK; aspect 32/32; dashboard-check OK with
"119 tests measured, 8 PROVEN claims".
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 25 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
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
2 participants
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.
Summary
Owner decision (2026-10-14): remove the idrisiser tree rather than regenerate it.
generated/idrisiser/was the third Idris2 tree JNK-01 found: wrappers the idrisiser tool generated fromidrisiser/*.tsigperidrisiser.toml. Its module names were lowercase, soidris2 --checkrefused them ("Expected a capitalised identifier, got: key"). Nothing in it was ever verified, and no ledger row depended on it.Removed:
generated/idrisiser/(6 files),idrisiser/*.tsig(3) andidrisiser.toml.generated/is now empty, so it goes too.References updated:
scripts/check-abi-tree.sh: section 7 used to print a note when the tree existed. It now fails ifgenerated/idrisiser,idrisiser/oridrisiser.tomlcomes back, the same way it treats the retiredsrc/idris-abi, so a second ABI tree can't return unnoticed..machine_readable/bot_directives/gitbot-fleet.a2ml: the tree is dropped fromnever-touchand its note. One entry is removed and nothing is added; A2ML is retired, so these files only shrink..machine_readable/contractiles/Mustfile.a2ml:no-dangerous-proof-escapesnow grepssrc/abi/only.generated-code-in-generatedis removed. Its check wastest -d generated, which fails once there is no generated code, and the stalecontractile.justnever ran it anyway.README.adoc,PROOF-NEEDS.adoc: the idrisiser caveats now say it was removed and why.Left alone:
CHANGELOG.adoc: it is generated from commits.STATE.a2ml: A2ML is retired estate-wide, superseded by.deed, K9 andcoordination.k9.Type of change
📌 New pins
None.
How has this been verified?
bash scripts/check-abi-tree.sh→OK: one ABI tree (4 modules, 1 package). Negative control:touch idrisiser.toml→FAIL: idrisiser.toml exists (retired idrisiser tree).bash tests/aspect/cross_cutting_test.sh→PASS: 32 FAIL: 0.cargo run -q -p dashboard-check -- --check .(Idris2 0.8.0, Agda 2.6.3) → OK,119 tests measured, 8 PROVEN claims.Checklist
Notes for reviewers
The red checks already red on
main(the #135 set) will show here too. A separate PR fixes them, as part of the CI/CD workflow overhaul.🤖 Generated with Claude Code
https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
Generated by Claude Code