Merge branch 'main' into claude/zealous-knuth-urnNU

Author: hyperpolymath

.github/workflows/echidna-verify.yml

@@ -93,7 +93,7 @@ jobs:
           submodules: recursive
 
       - name: Cache pack
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9 # v4.0.2
+        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
         with:
           path: |
             ~/.pack
@@ -116,17 +116,31 @@ jobs:
           git clone --depth 1 https://github.com/stefan-hoeck/idris2-pack.git "$HOME/idris2-pack"
           cd "$HOME/idris2-pack"
           # Use the bootstrap script in non-interactive mode
-          bash install.bash </dev/null || echo "::warning::pack install had warnings"
+          # pack's install.bash prompts for the scheme binary; feeding newlines
+          # makes the prompt take its detected default (chezscheme) instead of
+          # hitting EOF (which aborts the bootstrap and leaves pack uninstalled).
+          yes '' | bash install.bash || echo "::warning::pack install had warnings"
+          # pack installs its launcher into ~/.local/bin (newer layout) and/or
+          # ~/.pack/bin (older); add both so `pack` resolves on PATH.
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
           echo "$HOME/.pack/bin" >> "$GITHUB_PATH"
-          export PATH="$HOME/.pack/bin:$PATH"
-          pack install-api idris2
+          export PATH="$HOME/.local/bin:$HOME/.pack/bin:$PATH"
+          # `install-api` is not a pack subcommand; `install-app idris2`
+          # installs the idris2 executable into the pack bin dir so the
+          # subsequent `idris2 --check` resolves. The base library (Prelude,
+          # base, contrib) ships with idris2, so no .ipkg is needed for a
+          # standalone --check.
+          pack install-app idris2
           idris2 --version
 
-      - name: Type-check A2ML.Proofs
+      - name: Type-check A2ML core (Proofs + v1.1 profiles/base-vocab)
         run: |
           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
 
       - name: Upload log
         if: always()
@@ -147,7 +161,7 @@ jobs:
           submodules: recursive
 
       - name: Cache pack
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9 # v4.0.2
+        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
         with:
           path: |
             ~/.pack
@@ -167,10 +181,21 @@ jobs:
           sudo apt-get install -y build-essential libgmp-dev chezscheme
           git clone --depth 1 https://github.com/stefan-hoeck/idris2-pack.git "$HOME/idris2-pack"
           cd "$HOME/idris2-pack"
-          bash install.bash </dev/null || echo "::warning::pack install had warnings"
+          # pack's install.bash prompts for the scheme binary; feeding newlines
+          # makes the prompt take its detected default (chezscheme) instead of
+          # hitting EOF (which aborts the bootstrap and leaves pack uninstalled).
+          yes '' | bash install.bash || echo "::warning::pack install had warnings"
+          # pack installs its launcher into ~/.local/bin (newer layout) and/or
+          # ~/.pack/bin (older); add both so `pack` resolves on PATH.
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
           echo "$HOME/.pack/bin" >> "$GITHUB_PATH"
-          export PATH="$HOME/.pack/bin:$PATH"
-          pack install-api idris2
+          export PATH="$HOME/.local/bin:$HOME/.pack/bin:$PATH"
+          # `install-api` is not a pack subcommand; `install-app idris2`
+          # installs the idris2 executable into the pack bin dir so the
+          # subsequent `idris2 --check` resolves. The base library (Prelude,
+          # base, contrib) ships with idris2, so no .ipkg is needed for a
+          # standalone --check.
+          pack install-app idris2
           idris2 --version
 
       - name: Type-check AVOW proofs

.machine_readable/6a2/AGENTIC.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # AGENTIC.a2ml — AI agent constraints and capabilities
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-agentic/.
+@profile(id=a2ml/agentic)
+
 [metadata]
 version = "0.1.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # ECOSYSTEM.a2ml — Standards ecosystem position
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-ecosystem/.
+@profile(id=a2ml/ecosystem)
+
 [metadata]
 version = "1.0.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/META.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # META.a2ml — Standards meta-level information
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-meta/.
+@profile(id=a2ml/meta)
+
 [metadata]
 version = "1.0.0"
 last-updated = "2026-05-15"

.machine_readable/6a2/NEUROSYM.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # NEUROSYM.a2ml — Neurosymbolic integration metadata
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-neurosym/.
+@profile(id=a2ml/neurosym)
+
 [metadata]
 version = "0.1.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # PLAYBOOK.a2ml — Operational playbook
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-playbook/.
+@profile(id=a2ml/playbook)
+
 [metadata]
 version = "0.1.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/STATE.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # STATE.a2ml — Standards project state
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-state/.
+@profile(id=a2ml/state)
+
 [metadata]
 project = "standards"
 version = "0.2.0"

.machine_readable/REGISTRY.a2ml

@@ -32,7 +32,7 @@ name = "A2ML — Attested Markup Language"
 stream = "foundation"
 home = "a2ml/"
 canonical_doc = "a2ml/README.adoc"
-source_hash = "sha256:b34ffe4d51c1715c4f2e51183d7a510865dc03e962fbeae121e3868fd88a718a"
+source_hash = "sha256:ffda43ed07bed095c7623d3c6a1d38c8f17a6b9e4eebaebe3bfde5aff62bcfb0"
 route = "the typed/verified machine-readable document format"
 
 [[spec]]
@@ -41,7 +41,7 @@ name = "K9 Self-Validating Components"
 stream = "foundation"
 home = "k9-svc/"
 canonical_doc = "k9-svc/README.adoc"
-source_hash = "sha256:eae3b6a0f4e2da1afcfddfecf7a5c173d6c0ac090923c63fe9c14806b5a3b11b"
+source_hash = "sha256:6a9c2065fc29abdaaeef08c3e551f21c7408afd3c9a7cee4ed3e73460db443ab"
 route = "self-validating components with embedded contracts + deploy logic"
 
 [[spec]]
@@ -266,7 +266,7 @@ name = "Standards Hypatia Rules"
 stream = "integration"
 home = "hypatia-rules/"
 canonical_doc = "hypatia-rules/README.adoc"
-source_hash = "sha256:707852684795e8474bc764473c36bc4d56fa139014ab3abbc0f550319637138c"
+source_hash = "sha256:a63e95c5e43ced2ee13c58014175da156c71ab731f01449e3a61b3e2f33bbe52"
 route = "the dogfooding rules that scan THIS repo (incl. drift detection)"
 
 [[spec]]

.machine_readable/anchors/ANCHOR.a2ml

@@ -1,5 +1,9 @@
 # ⚓ ANCHOR: standards
 # This is the canonical authority for the standards repository.
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-anchor/.
+@profile(id=a2ml/anchor)
 
 id: "org.hyperpolymath.standards"
 version: "1.0.0"

a2ml/README.adoc

@@ -50,7 +50,9 @@ A2ML is a typed, attested markup format. It verifies structure and references.
 
 == Documents
 
-* link:SPEC.adoc[Spec: Surface Grammar + Typed Core]
+* link:SPEC.adoc[Spec (current normative, v1.1.0): Surface Grammar + Typed Core + Profiles]
+* link:VERSIONS.adoc[Specification Lineage (versions + era)]
+* link:archive/[Archived (frozen) prior specs]
 * link:docs/QUICKSTART.adoc[Module 0 Quickstart + FAQ]
 * link:docs/MODULES.adoc[Syntax Modules (Opt-in)]
 * link:docs/GRAMMAR.adoc[Grammar Appendix]
@@ -101,6 +103,8 @@ A2ML is a typed, attested markup format. It verifies structure and references.
 * link:RELEASE-NOTES-v0.1.0.adoc[v0.1.0 Release Notes]
 * link:RELEASE-NOTES-v0.5.0.adoc[v0.5.0 Release Notes]
 * link:RELEASE-NOTES-v0.6.0.adoc[v0.6.0 Release Notes]
+* link:RELEASE-NOTES-v1.0.0.adoc[v1.0.0 Release Notes]
+* link:RELEASE-NOTES-v1.1.0.adoc[v1.1.0 Release Notes]
 
 == Announcement
 
@@ -110,9 +114,13 @@ A2ML is a typed, attested markup format. It verifies structure and references.
 
 == Status
 
-* Draft specification, v0.6.0
-* Prototype parser + CLI + demo page available
-* Typed core stubs + core tests passing (prototype)
+* *Stable specification, v1.1.0* (era v1). See link:VERSIONS.adoc[VERSIONS.adoc]
+  for the lineage; prior drafts (v0) and the frozen v1.0.0 release are under
+  link:archive/[archive/].
+* v1.1.0 is additive over v1.0.0: profile mechanism, base record vocabulary,
+  citation primitives, and canonical hashing — all inert under the base modes.
+* Prototype parser + CLI + demo page available.
+* Typed core + core tests passing (prototype).
 
 == License