Skip to content

Commit 9d0e641

Browse files
Finish the stale-fact sweep + add a language-registry consistency guard (#120)
## Context Final follow-up to the registry reconciliation (#106, #113, #119). Two parts: **(1)** sweep the last stale in-tree / count residue those PRs didn't reach, and **(2)** add a CI guard so the 15-entry family can't silently drift back out of sync. ## 1. Stale-fact sweep - **`PROOF-NEEDS.md`** — dropped the `~456,000 LOC` count (it counted code no longer in this repo) and reframed the in-tree paths (`ephapax/formal/Semantics.v`, `oblibeny` ABI) as living in each language's own repo. Kept as a genuine cross-language proof-gap tracker. - **`README.adoc`** — disambiguated the **Tangle** language from the out-of-scope **KRL resolution stack** in the three places that conflated them (the `KRL — … (Tangle)` heading, the database-relationship line, and the entry-point note), consistent with the split established in #106/#113. - **`EXPLAINME.adoc`** — reconciled the language count. It quoted a defunct README claim of "ten programming languages" and carried an 8-row "eight core + two specialised" table; now says **14 languages + the KitchenSpeak DSL**, points at `LANGUAGES.a2ml` as canonical, and notes the table is a representative subset (listing the six not shown). - **`language-status-tracker.jl`** — the repos dir is now overridable via `HYPERPOLYMATH_REPOS_DIR` instead of being hardcoded to `~/Documents/hyperpolymath-repos`, so it can run somewhere other than one machine. (`TEST-NEEDS.md` was already reconciled in #106 — no change needed.) ## 2. Language-registry consistency guard (the durable win) New **`hooks/validate-language-registry.sh`** + a **`language-registry`** job in `dogfood-gate.yml` (mirrors the existing `coordinator-boundary` job). It fails the build when the family disagrees across surfaces: - **Source of truth:** `languages/<id>.md` pointers (15). - Asserts **exact** match against: `LANGUAGES.a2ml` `[[language]]` stanzas (excluding forward-looking `proposed`/`exploratory` entries like typefix-zero), the boundary-hook `LANGS` list, and `ECOSYSTEM.a2ml` `[language-repos]` keys. - Asserts **superset** for `language-status-tracker.jl` (it also tracks playgrounds/ecosystem/umbrella). Adding a language now fails CI until every surface is updated together — which is exactly the ~10-edits-with-nothing-catching-a-miss problem the original audit found. ## Verification - `bash hooks/validate-language-registry.sh` → **OK (all surfaces agree on the 15-language family)**. - Negative test: dropping a language from any surface makes it exit 1 with the offending surface + id named (verified locally against the hook `LANGS` list). - `bash hooks/validate-coordinator-boundary.sh` → **OK**. - `dogfood-gate.yml` parses; 7 jobs including `language-registry`, wired into the summary's `needs`. ## Notes / earlier open items (unchanged) - The `CLADE.a2ml` `type = "coordinator"` value from #119 still wants confirmation against the external `gv-clade-index` vocabulary. - The guard treats `proposed`/`exploratory` a2ml statuses as pointer-exempt (that's how `typefix-zero` stays registered privately without a `languages/` pointer). 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_016t5KLJDtqdeDi1EMNqNx6K --- _Generated by [Claude Code](https://claude.ai/code/session_016t5KLJDtqdeDi1EMNqNx6K)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent e8c68ac commit 9d0e641

6 files changed

Lines changed: 155 additions & 16 deletions

File tree

.github/workflows/dogfood-gate.yml

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -257,14 +257,36 @@ jobs:
257257
echo "" >> "$GITHUB_STEP_SUMMARY"
258258
echo "Verifies that no language-implementation content (proofs, grammars, compilers, specs, or a re-vendored language directory) has leaked into the coordinator. Language code lives in each \`hyperpolymath/<lang>\` repo, referenced here — not embedded." >> "$GITHUB_STEP_SUMMARY"
259259
260+
# ---------------------------------------------------------------------------
261+
# Job 5b: Language-registry consistency — every surface lists the same family
262+
# ---------------------------------------------------------------------------
263+
language-registry:
264+
name: Language registry consistency
265+
runs-on: ubuntu-latest
266+
timeout-minutes: 15
267+
268+
steps:
269+
- name: Checkout repository
270+
uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
271+
272+
- name: Enforce language-registry consistency
273+
run: bash hooks/validate-language-registry.sh
274+
275+
- name: Write summary
276+
if: always()
277+
run: |
278+
echo "## Language Registry Consistency" >> "$GITHUB_STEP_SUMMARY"
279+
echo "" >> "$GITHUB_STEP_SUMMARY"
280+
echo "Verifies every language appears on all registry surfaces (\`languages/\`, \`LANGUAGES.a2ml\`, the boundary-hook \`LANGS\` list, \`ECOSYSTEM.a2ml\`, and the status tracker), so the family cannot silently drift out of sync. Canonical set: \`languages/*.md\`." >> "$GITHUB_STEP_SUMMARY"
281+
260282
# ---------------------------------------------------------------------------
261283
# Job 6: Dogfooding summary
262284
# ---------------------------------------------------------------------------
263285
dogfood-summary:
264286
name: Dogfooding compliance summary
265287
runs-on: ubuntu-latest
266288
timeout-minutes: 15
267-
needs: [a2ml-validate, k9-validate, empty-lint, groove-check, coordinator-boundary]
289+
needs: [a2ml-validate, k9-validate, empty-lint, groove-check, coordinator-boundary, language-registry]
268290
if: always()
269291

270292
steps:

EXPLAINME.adoc

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -22,20 +22,21 @@ NOTE: `tentacles-agentic-syllabus` is NOT a programming language. It is an
2222
educational framework using My-Lang's dialects as a curriculum vehicle. Never
2323
audit it as a language implementation.
2424

25-
== Claim 1: "Ten languages that cover the full spectrum of modern software challenges"
25+
== Claim 1: "A family of languages covering the full spectrum of modern software challenges"
2626

2727
[quote, README]
2828
____
29-
A coordinated effort to design and develop ten programming languages that
29+
A coordinated effort to design and develop a family of programming languages that
3030
collectively cover the full spectrum of modern software challenges, from
3131
AI-native development to formally verified real-time systems.
3232
____
3333

3434
=== How it works
3535

36-
The eight core languages plus two specialised languages are designed to
37-
complement each other, not compete. They occupy distinct cells in the design
38-
space (each maintained as a standalone `hyperpolymath/<lang>` repo):
36+
The family currently spans fourteen languages plus the KitchenSpeak DSL — the canonical
37+
list is `.machine_readable/LANGUAGES.a2ml`. They are designed to complement each other, not
38+
compete, each occupying a distinct cell in the design space (each maintained as a standalone
39+
`hyperpolymath/<lang>` repo). The table below shows the representative core:
3940

4041
[cols="1,1,2,1"]
4142
|===
@@ -90,9 +91,14 @@ Gossamer backend. Rust compiler, Coq proofs.
9091
| Rust (17 crates), Coq proofs
9192
|===
9293

94+
NOTE: The table shows a representative core. The full family also includes *betlang*
95+
(probabilistic), *JtV* (systems / Harvard architecture), *Haec* (trope-particularity),
96+
*error-lang* (pedagogical), *Tangle* (topological), and *007* (a private agent
97+
meta-language) — see `.machine_readable/LANGUAGES.a2ml` for the canonical registry.
98+
9399
NOTE: *KitchenSpeak* — an experimental applied-type-theory teaching DSL
94100
(seven-type kitchen orchestration: Tropical, Linear, Choreographic, Echo,
95-
Dyadic, Ceremonial, Primitive) — is NOT one of the ten core languages and is
101+
Dyadic, Ceremonial, Primitive) — is NOT one of the core languages above and is
96102
no longer carried in this repo. It is canonical at the standalone
97103
link:https://github.com/hyperpolymath/kitchenspeak[`hyperpolymath/kitchenspeak`]
98104
repository (v2.0: physics-in-the-types, reference OCaml compiler, machine-checked

PROOF-NEEDS.md

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,14 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
66

77
## Current State
88

9-
- **src/abi/*.idr**: YES (in oblibeny) — `Interface.idr`
10-
- **Dangerous patterns**: 4 `Admitted` in ephapax/formal/Semantics.v (ctx_transfer 15/24, subst_lemma, preservation)
11-
- **LOC**: ~456,000 (OCaml + Rust + Coq + Idris2 + Lean)
12-
- **Existing proofs**: Ephapax has Coq proofs, Tangle has Lean proofs, Idris2 in multiple sub-languages
9+
`nextgen-languages` is a pure coordinator and holds **no** proof code. This file tracks the
10+
family's proof gaps across the standalone `hyperpolymath/<lang>` repos; every path below is
11+
relative to the named language's own repo, not this one.
12+
13+
- **Ephapax** — Coq proofs present; 4 `Admitted` remain in `formal/Semantics.v` (ctx_transfer 15/24, subst_lemma, preservation, + one more).
14+
- **Tangle** — Lean proofs present (`Tangle.lean`); coverage partial.
15+
- **Oblíbený** — Idris2 ABI present (`src/abi/Interface.idr`); minimal.
16+
- **AffineScript** — OCaml type checker + Rust runtime; soundness proofs outstanding.
1317

1418
## What Needs Proving
1519

README.adoc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,9 +43,9 @@ Status: design-stage, with partial specifications and experimental implementatio
4343

4444
---
4545

46-
=== KRL — Knot Resolution Language (Tangle)
46+
=== Tangle
4747

48-
A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy.
48+
A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy. Its IR (TangleIR) is consumed by the separate *KRL resolution stack* (`krl → TangleIR → VeriSimCore → Skein.jl / QuandleDB`), which is tracked by the database estate — not part of this coordinator's language family.
4949

5050
* Composition and tensor operations correspond to braid structure
5151
* Formal semantics specified
@@ -141,7 +141,7 @@ Type-theoretic boundaries are made explicit: total proof-like fragments are dist
141141

142142
These languages are designed to work with systems that treat equivalence, provenance, and semantic identity as first-class concepts:
143143

144-
KRL ↔ QuandleDB / Skein
144+
Tangle (via the separate KRL resolution stack) ↔ QuandleDB / Skein
145145
JtV ↔ future equivalence-aware runtime and storage models
146146

147147
See the nextgen-databases repository for details.
@@ -196,7 +196,7 @@ production system. The work it tracks spans, across the individual language repo
196196
Each language lives in its own `hyperpolymath/<lang>` repo; start there. For orientation:
197197

198198
* link:https://github.com/hyperpolymath/tangle[`hyperpolymath/tangle`] — `Tangle.lean`, the
199-
mechanised type-safety proof for the Tangle (KRL) core; topological language design
199+
mechanised type-safety proof for the Tangle core; topological language design
200200
* link:https://github.com/hyperpolymath/jtv[`hyperpolymath/jtv`] — computation as
201201
path-based construction
202202

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
#!/usr/bin/env bash
2+
# SPDX-License-Identifier: MPL-2.0
3+
# Language-registry consistency guard.
4+
#
5+
# nextgen-languages registers its language family across several surfaces. They
6+
# drifted badly before (a language present on one surface, missing on another),
7+
# so this check fails the build when they disagree.
8+
#
9+
# Source of truth: the human-facing pointers in `languages/<id>.md`. Every other
10+
# surface MUST list exactly that same set of ids:
11+
# - .machine_readable/LANGUAGES.a2ml ([[language]] stanzas; forward-looking entries with
12+
# status "proposed"/"exploratory" are exempt — they
13+
# are not yet committed and carry no languages/ pointer)
14+
# - hooks/validate-coordinator-boundary.sh (the LANGS re-vendoring guard list)
15+
# - .machine_readable/6a2/ECOSYSTEM.a2ml ([language-repos] keys)
16+
# - language-status-tracker.jl (const LANGUAGES — must be a SUPERSET;
17+
# it also tracks playgrounds/ecosystem/umbrella)
18+
#
19+
# See 0-AI-MANIFEST.a2ml and EXTRACTION-MANIFEST.md.
20+
set -euo pipefail
21+
22+
cd "$(git rev-parse --show-toplevel)"
23+
24+
ERRORS=0
25+
26+
# ── Source of truth: languages/<id>.md pointers (excluding README) ────────────
27+
family() {
28+
for f in languages/*.md; do
29+
b="$(basename "$f" .md)"
30+
[[ "$b" == "README" ]] || printf '%s\n' "$b"
31+
done | sort -u
32+
}
33+
34+
# ── LANGUAGES.a2ml: committed [[language]] ids (status not proposed/exploratory) ──
35+
a2ml_registered() {
36+
awk '
37+
/^\[\[language\]\]/ { if (id != "") print id, status; id=""; status="" ; next }
38+
/^id[ \t]*=/ { line=$0; sub(/^id[ \t]*=[ \t]*"/,"",line); sub(/".*/,"",line); id=line }
39+
/^status[ \t]*=/ { line=$0; sub(/^status[ \t]*=[ \t]*"/,"",line); sub(/".*/,"",line); status=line }
40+
END { if (id != "") print id, status }
41+
' .machine_readable/LANGUAGES.a2ml \
42+
| awk '$2 != "proposed" && $2 != "exploratory" { print $1 }' | sort -u
43+
}
44+
45+
# ── boundary-hook LANGS list ──────────────────────────────────────────────────
46+
hook_langs() {
47+
grep -E '^LANGS=' hooks/validate-coordinator-boundary.sh \
48+
| sed -E 's/^LANGS="//; s/"[[:space:]]*$//' \
49+
| tr ' ' '\n' | sed '/^$/d' | sort -u
50+
}
51+
52+
# ── ECOSYSTEM.a2ml [language-repos] keys (excluding the `note` key) ───────────
53+
ecosystem_keys() {
54+
awk '
55+
/^\[language-repos\]/ { inblk=1; next }
56+
/^\[/ { inblk=0 }
57+
inblk && /^[^#].*=/ {
58+
key=$0; sub(/[ \t]*=.*/,"",key); gsub(/["[:space:]]/,"",key)
59+
if (key != "note" && key != "") print key
60+
}
61+
' .machine_readable/6a2/ECOSYSTEM.a2ml | sort -u
62+
}
63+
64+
# ── tracker const LANGUAGES vector (quoted ids) ───────────────────────────────
65+
tracker_langs() {
66+
awk '/const LANGUAGES[ \t]*=[ \t]*\[/ { inblk=1; next } inblk && /^\]/ { inblk=0 } inblk' \
67+
language-status-tracker.jl \
68+
| grep -oE '"[^"]+"' | tr -d '"' | sort -u
69+
}
70+
71+
FAMILY="$(family)"
72+
COUNT="$(printf '%s\n' "$FAMILY" | wc -l | tr -d ' ')"
73+
printf 'language-registry: source of truth = languages/*.md (%s entries)\n' "$COUNT"
74+
75+
# report_diff <surface-name> <surface-set> <mode: exact|superset>
76+
report_diff() {
77+
local name="$1" have="$2" mode="$3" missing extra
78+
missing="$(comm -23 <(printf '%s\n' "$FAMILY") <(printf '%s\n' "$have") || true)"
79+
if [[ -n "$missing" ]]; then
80+
printf 'ERROR: %s is MISSING family languages:\n' "$name"
81+
printf '%s\n' "$missing" | sed 's/^/ - /'
82+
ERRORS=$((ERRORS + 1))
83+
fi
84+
if [[ "$mode" == "exact" ]]; then
85+
extra="$(comm -13 <(printf '%s\n' "$FAMILY") <(printf '%s\n' "$have") || true)"
86+
if [[ -n "$extra" ]]; then
87+
printf 'ERROR: %s lists languages NOT in languages/ (add a pointer, or remove them):\n' "$name"
88+
printf '%s\n' "$extra" | sed 's/^/ - /'
89+
ERRORS=$((ERRORS + 1))
90+
fi
91+
fi
92+
}
93+
94+
report_diff ".machine_readable/LANGUAGES.a2ml" "$(a2ml_registered)" exact
95+
report_diff "hooks/validate-coordinator-boundary.sh LANGS" "$(hook_langs)" exact
96+
report_diff ".machine_readable/6a2/ECOSYSTEM.a2ml" "$(ecosystem_keys)" exact
97+
report_diff "language-status-tracker.jl const LANGUAGES" "$(tracker_langs)" superset
98+
99+
if [[ "$ERRORS" -gt 0 ]]; then
100+
printf '\nlanguage-registry check FAILED (%s surface(s) out of sync).\n' "$ERRORS"
101+
printf 'Every language must appear on all registry surfaces. Update them together —\n'
102+
printf 'the canonical set is languages/*.md; see .machine_readable/LANGUAGES.a2ml.\n'
103+
exit 1
104+
fi
105+
106+
printf 'language-registry: OK (all surfaces agree on the %s-language family)\n' "$COUNT"
107+
exit 0

language-status-tracker.jl

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
using Dates
77

8-
const REPOS_DIR = joinpath(homedir(), "Documents/hyperpolymath-repos")
8+
const REPOS_DIR = get(ENV, "HYPERPOLYMATH_REPOS_DIR", joinpath(homedir(), "Documents/hyperpolymath-repos"))
99

1010
# All known language repos
1111
const LANGUAGES = [

0 commit comments

Comments
 (0)