fix(a2ml): complete normative core verification

.github/workflows/actions.lock

@@ -94,6 +94,7 @@ workflows:
         - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
     '.github/workflows/self-test.yml':
         - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+        - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed'
     '.github/workflows/signed-push-smoke.yml':
         - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
         - 'actions/create-github-app-token@bcd2ba49218906704ab6c1aa796996da409d3eb1'

.github/workflows/echidna-verify.yml

@@ -18,12 +18,14 @@ on:
     paths:
       - 'lol/proofs/**'
       - 'a2ml/src/**/*.idr'
+      - 'a2ml/a2ml-core.ipkg'
       - 'avow-protocol/avow-lib/src/abi/*.idr'
       - '.github/workflows/echidna-verify.yml'
   pull_request:
     paths:
       - 'lol/proofs/**'
       - 'a2ml/src/**/*.idr'
+      - 'a2ml/a2ml-core.ipkg'
       - 'avow-protocol/avow-lib/src/abi/*.idr'
   schedule:
     # Weekly re-verification to catch stale-proof drift
@@ -135,14 +137,16 @@ jobs:
           pack install-app idris2
           idris2 --version
 
-      - name: Type-check A2ML core (Proofs + v1.1 profiles/base-vocab)
+      - name: Type-check normative A2ML core
         run: |
+          set -euo pipefail
           export PATH="$HOME/.pack/bin:$PATH"
           cd a2ml
-          idris2 --check src/A2ML/Proofs.idr 2>&1 | tee ../idris2-a2ml.log
-          # v1.1 additive core: checking Profiles.idr transitively type-checks
-          # BaseVocab.idr and TypedCore.idr (its imports).
-          idris2 --check src/A2ML/Profiles.idr 2>&1 | tee -a ../idris2-a2ml.log
+          # Use the package target: per-file `--check` can exit successfully
+          # when an imported module is missing and therefore is not a real
+          # gate for the authoritative module set (standards#556).
+          idris2 --version | tee ../idris2-a2ml.log
+          idris2 --typecheck a2ml-core.ipkg 2>&1 | tee -a ../idris2-a2ml.log
 
       - name: Upload log
         if: always()

.github/workflows/self-test.yml

@@ -35,6 +35,15 @@ jobs:
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
 
+      # check-ts-allowlist-test.sh executes the generated Deno target, and the
+      # scorecard grounding suite runs pass-checks that use the same toolchain.
+      # Without installing Deno, the suite reported 18 assertion failures as
+      # one red test file and also made the scorecard fixtures fail.
+      - name: Install Deno test runtime
+        uses: denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed # v2.0.5
+        with:
+          deno-version: v2.x
+
       # PyYAML is required by the secret-scanner canary. The scorecard
       # grounding tests execute the same checks as registry-verify, including
       # checks that require ripgrep and xmllint.

.machine_readable/REGISTRY.a2ml

@@ -45,7 +45,7 @@ name = "A2ML — Attested Markup Language"
 stream = "foundation"
 home = "a2ml/"
 canonical_doc = "a2ml/README.adoc"
-source_hash = "sha256:480aeca64a094b3f184dc5aa98c00abb60ebcae33b41038410f2a5ff88d19427"
+source_hash = "sha256:01e65e3c955746526e47b8a313070c13647228a1f6c453ad1b43d147789e664a"
 route = "the typed/verified machine-readable document format"
 
 [[spec]]

a2ml/a2ml-core.ipkg

@@ -16,12 +16,9 @@ authors    = "Jonathan D.A. Jewell (hyperpolymath)"
 license    = "MPL-2.0"
 sourcedir  = "src"
 
--- SCOPE. Every module listed here type-checks under idris2 0.7.0 and is
--- gated in CI. A2ML.Converters is deliberately NOT listed: its renderers
--- (toMarkdown/toDjot/toHtml/toLatex) are mutually recursive with their own
--- where-block helpers, which cannot be total in that shape and needs a
--- hand-done restructure. Tracked separately -- see the repo issue. Adding it
--- here before that work is done would make this gate red on arrival.
+-- SCOPE. Every normative core module listed here type-checks under Idris2
+-- 0.7.0 and is gated in CI. Converters is included now that its renderers use
+-- structurally decreasing mutual recursion over List Block.
 modules = A2ML.TypedCore
         , A2ML.Surface
         , A2ML.Parser
@@ -32,3 +29,4 @@ modules = A2ML.TypedCore
         , A2ML.CoreTests
         , A2ML.ParserTests
         , A2ML.Tests
+        , A2ML.Converters