fix(a2ml): make the normative Idris2 core type-check + add the missing .ipkg - #555
Conversation
… .ipkg
SPEC.adoc 3.1 declares "The normative Idris2 model lives in src/A2ML/ ... the
source files are authoritative." It did not type-check, and nothing built it:
there was no .ipkg anywhere under a2ml/, and no CI job invokes the Justfile
core-tests recipe. So the authoritative core was never machine-checked.
Adds a2ml/a2ml-core.ipkg so the claim is checkable with
`idris2 --typecheck a2ml-core.ipkg` (the ipkg target is used deliberately:
per-file `idris2 --check` exits 0 when an imported module is simply missing,
which makes it a fake gate).
Fixes A2ML.Proofs, which failed outright. All four fixes are genuine proofs —
no postulate, no believe_me:
1. import Data.List.Quantifiers — `All` was used but never imported, so the
uniqueAppendDisjoint signature failed to elaborate.
2. `elemAppend` was referenced twice but defined nowhere and imported from
nowhere. Replaced with two lemmas proved by induction on the Elem witness:
elemAppendLeft (membership survives appending on the right) and
elemAppendSplit (membership in a concatenation is membership in one side).
3. `|>` is not an Idris2 operator; the intent was to weaken an Elem across an
append, which is exactly elemAppendLeft.
4. validatedHasUniqueIds / validatedHasResolvedRefs referenced the argument
by name in their own signatures before binding it, and projected `ids` /
`refs` / `uniqueProof`, which three record types share. Bound the argument
and qualified the projections.
A2ML.Proofs now type-checks. The remaining blocker is A2ML.Parser (16 errors:
7 unification, 6 totality under %default total, an undefined <|>, and a use of
the private TypedCore.collectIds) — tracked separately; no CI gate is added in
this PR because it would be red on arrival.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 1 resolved / 1 findingsAdds the missing Idris2 package manifest and fixes the A2ML.Proofs module so core core-types elaborate correctly. Consider updating the ipkg comment to reflect that the parser module still fails type-checking.
✅ 1 resolved✅ Quality: ipkg comment claims full type-check but Parser still fails
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
#562) Answers **gitar-bot's comment on #555**. The bot was **right** that the documented command fails — but its diagnosis was incomplete and its suggested remedy (soften the comment / scope the module list) would have made the claim *less* true. **Measured:** `idris2 --typecheck a2ml-core.ipkg` → **exit 1, 16 errors** (Idris2 0.7.0). **1. Code fix.** 2 of the 16 shared one root cause: `strIndex : String -> Int -> Char` is partial and returns a bare `Char`; `peek` and `char` pattern-matched it as `Just`/`Nothing`. Added a total bounds-checked `charAt : String -> Nat -> Maybe Char`. **16 → 14.** **2. Honest header.** The remaining 14 are real and now documented in the file: 7 totality, 5 unification, 1 undefined `<|>`, 1 private `collectIds`. And the part that matters most: the header claimed this package makes SPEC.adoc §3.1 "machine-checked" and referred to "the CI job that consumes this". **No workflow in this repository invokes it.** The claim was decorative — exactly the fake gate the next paragraph of that same header warns about. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Signed-off-by: dependabot[bot] <support@github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Mistral Vibe <vibe@mistral.ai>
1 participant
The problem
SPEC.adoc§3.1 says: "The normative Idris2 model lives insrc/A2ML/… the source files are authoritative."It did not type-check — and nothing ever checked it:
.ipkgfiles anywhere undera2ml/, so there was no build target;core-testsJustfile recipe (that recipe is honest — itexit 1s whenidris2is absent — but nothing calls it).So the authoritative definition of A2ML has been unverified. Given the family is about to be registered with IANA and three dialects must agree through this core, that is the foundation to fix first.
What this PR does
Adds
a2ml/a2ml-core.ipkgso the claim is machine-checkable:idris2 --typecheck a2ml-core.ipkg. The ipkg target is deliberate — per-fileidris2 --checkexits 0 when an imported module is merely missing, which is a fake gate (an estate-wide lesson).Fixes
A2ML.Proofs, which failed outright. All four are genuine proofs — nopostulate, nobelieve_me:import Data.List.Quantifiers—Allwas used but never imported, souniqueAppendDisjoint's signature failed to elaborate ("No type declaration for…").elemAppendwas referenced twice but defined nowhere and imported from nowhere. Replaced with two lemmas proved by induction on theElemwitness —elemAppendLeft(membership survives appending on the right) andelemAppendSplit(membership in a concatenation is membership in one side or the other). Both verified against Idris2 0.7.0.|>is not an Idris2 operator; the intent was to weaken anElemacross an append — exactlyelemAppendLeft.validatedHasUniqueIds/validatedHasResolvedRefsreferenced the argument by name in their own signatures before binding it, and projectedids/refs/uniqueProof, which three record types share (UniqueDoc,ResolvedDoc,ValidatedDoc). Bound the argument; qualified the projections.Verified locally with idris2 0.7.0:
A2ML.Proofsnow type-checks (0 errors, down from a hard failure).TypedCoreandSurfacetype-check too — Idris2 only proceeds to buildA2ML.Parseronce its dependencies succeed.What remains — and why no CI gate here
A2ML.Parserstill fails with 16 errors: 7 unification failures, 6 totality failures (under%default total), an undefined<|>, and a use of the privateTypedCore.collectIds.I have deliberately not added a CI gate in this PR — it would be red on arrival, and landing a red required check would block the queue. The gate should land together with the parser repair, tracked separately. This PR is a strict improvement: the package manifest now exists and the proof module is sound.