diff --git a/contractiles/must/clade-hygiene.a2ml b/contractiles/must/clade-hygiene.a2ml index 4a9668c..1e040ff 100644 --- a/contractiles/must/clade-hygiene.a2ml +++ b/contractiles/must/clade-hygiene.a2ml @@ -34,6 +34,35 @@ scope = "pre-commit" command = "grep 'primary = ' .machine_readable/CLADE.a2ml | grep -qE '\"(fv|nl|rm|gv|db|ap|ix|dx|pt|ax|gm|sc)\"'" message = "CLADE.a2ml primary clade code not in valid set: fv nl rm gv db ap ix dx pt ax gm sc" +[must] +id = "CLADE-006" +name = "clade-name-matches-code" +description = "primary-name must be the taxonomy's name for the declared primary code" +severity = "BLOCK" +scope = "pre-commit" + +# WHY THIS EXISTS. +# +# CLADE-003 checks the code is one of the 12. It cannot check the AUTHOR MEANT +# that clade — every code is valid whatever you thought it stood for. So these +# passed every gate: +# +# paint-type primary = "pt" believing "PainT-type" +# -- pt is Protocols & Interop; paint-type is an image editor +# gossamer primary = "gv" believing "Graphical/Visual" +# -- gv is GoVernance & Standards; there is no graphical clade +# +# The two letters abbreviate the CLADE's name, never the REPO's name. Requiring +# the name alongside the code makes the mistaken belief WRITABLE, and therefore +# CHECKABLE: primary = "pt" + primary-name = "PainT-type" now fails here, +# instead of being filed silently under Protocols & Interop. +# +# The pairs below are the authority in verisim/seed/clades.a2ml. Keep in sync. + +[must.check] +command = '''p=$(sed -n 's/^primary = "\(.*\)".*/\1/p' .machine_readable/CLADE.a2ml | head -1); n=$(sed -n 's/^primary-name = "\(.*\)".*/\1/p' .machine_readable/CLADE.a2ml | head -1); case "$p|$n" in 'fv|Formal Verification & Proofs'|'nl|Nextgen Languages'|'rm|Repo Management & Tooling'|'gv|Governance & Standards'|'db|Databases'|'ap|Applications'|'ix|Infrastructure & Cloud'|'dx|Developer Ecosystem'|'pt|Protocols & Interop'|'ax|AI & Neurosymbolic'|'gm|Games & Interactive'|'sc|Security') exit 0 ;; *) exit 1 ;; esac''' +message = "CLADE.a2ml primary-name does not match primary code. The 2 letters abbreviate the CLADE's name, not the repo's. Valid pairs: fv=Formal Verification & Proofs, nl=Nextgen Languages, rm=Repo Management & Tooling, gv=Governance & Standards, db=Databases, ap=Applications, ix=Infrastructure & Cloud, dx=Developer Ecosystem, pt=Protocols & Interop, ax=AI & Neurosymbolic, gm=Games & Interactive, sc=Security" + [must] id = "CLADE-004" name = "clade-status-phase-set" diff --git a/docs/SPEC-clade-verisim-portal.adoc b/docs/SPEC-clade-verisim-portal.adoc index 74853dd..41e7b13 100644 --- a/docs/SPEC-clade-verisim-portal.adoc +++ b/docs/SPEC-clade-verisim-portal.adoc @@ -70,6 +70,46 @@ the current repository name unchanged. **Rationale**: 2 characters provide 676 possible codes (far more than needed), are short enough to avoid bloating names, and cause natural alphabetical grouping when sorted. +[IMPORTANT] +==== +*The two letters abbreviate the name of the CLADE. They never abbreviate the name of the +repo.* This is a closed taxonomy of twelve categories, not an abbreviation scheme: you +choose the category a repo belongs to, then write down that category's code. You do not +look at the repo's name and find two letters that fit it. + +This is stated because the opposite was done, more than once: + +[cols="1,1,2,2"] +|=== +| Repo | Code | Read as | Actually means + +| `paint-type` | `pt` | "*P*ain*T*-type" | Protocols & Interop — an image editor is `ap` +| `gossamer` | `gv` | "*G*raphical/*V*isual" | Governance & Standards — there is no graphical clade +|=== + +Both codes were *valid*, so every check passed and the repos were filed under categories +they have nothing to do with. A code alone cannot express a wrong belief about what it +means, so it cannot be checked for one. + +Therefore every `CLADE.a2ml` MUST declare the clade's name alongside its code: + +[source,toml] +---- +[clade] +primary = "ap" +primary-name = "Applications" # must be the taxonomy's name for `primary` +---- + +The redundancy is the point: the *pair* can express the wrong belief, and so the pair can +be rejected. `primary = "pt"` with `primary-name = "PainT-type"` now fails +<> instead of passing silently. `primary-name` must match the `name` +field for that code in `verisim/seed/clades.a2ml`, which is the authority. + +[[clade-006]] +Enforced by CLADE-006 in `contractiles/must/clade-hygiene.a2ml` (severity BLOCK, scope +pre-commit). +==== + === Clade Definitions [cols="1,3,4"] diff --git a/sync/deploy-clade-a2ml.sh b/sync/deploy-clade-a2ml.sh index 9433a8f..637b862 100755 --- a/sync/deploy-clade-a2ml.sh +++ b/sync/deploy-clade-a2ml.sh @@ -37,6 +37,32 @@ parse_repos() { bash "$REPOS_DIR/gv-clade-index/sync/parse-repos.sh" "$SEED_FILE" } +# The taxonomy's name for a clade code. Authority: verisim/seed/clades.a2ml. +# +# Emitted into every CLADE.a2ml as `primary-name` so the code never travels +# without its meaning. CLADE-003 can only check a code is one of the 12 — it +# cannot check the author meant that clade, which is how `pt` ("PainT-type", +# actually Protocols & Interop) and `gv` ("Graphical/Visual", actually +# GoVernance) were filed under categories they have nothing to do with. Writing +# the name down makes the belief checkable; CLADE-006 enforces the pair. +clade_name() { + case "$1" in + fv) echo "Formal Verification & Proofs" ;; + nl) echo "Nextgen Languages" ;; + rm) echo "Repo Management & Tooling" ;; + gv) echo "Governance & Standards" ;; + db) echo "Databases" ;; + ap) echo "Applications" ;; + ix) echo "Infrastructure & Cloud" ;; + dx) echo "Developer Ecosystem" ;; + pt) echo "Protocols & Interop" ;; + ax) echo "AI & Neurosymbolic" ;; + gm) echo "Games & Interactive" ;; + sc) echo "Security" ;; + *) echo "" ;; + esac +} + deploy_clade() { local repo_name="$1" local primary="$2" @@ -120,6 +146,17 @@ deploy_clade() { # Determine prefixed name local prefixed="${primary}-${repo_name}" + # Refuse to write an identity we cannot name. An unknown code here means the + # seed disagrees with the taxonomy — fail loudly rather than emit a CLADE.a2ml + # that would fail CLADE-006 downstream in someone else's repo. + local primary_name + primary_name=$(clade_name "$primary") + if [[ -z "$primary_name" ]]; then + echo "ERROR: $repo_name — clade code '$primary' is not one of the 12 in clades.a2ml. Skipping." >&2 + ((FAILED++)) + return + fi + # Ensure .machine_readable/ exists mkdir -p "$repo_path/.machine_readable" @@ -137,7 +174,10 @@ canonical-name = "$repo_name" prefixed-name = "$prefixed" [clade] +# The 2 letters abbreviate the CLADE's name below — never the repo's name. +# See gv-clade-index: verisim/seed/clades.a2ml for all 12 codes. primary = "$primary" +primary-name = "$primary_name" secondary = $secondary assigned = "2026-03-16" rationale = "$description" @@ -186,9 +226,33 @@ echo "Repos dir: $REPOS_DIR" [[ "$DRY_RUN" == "--dry-run" ]] && echo "MODE: DRY RUN" echo "" -while IFS=$'\t' read -r name primary secondary lineage parent description owner; do +# Read the parser's TSV with the tabs translated to US (0x1f) first. +# +# TAB IS IFS WHITESPACE, so `IFS=$'\t' read` COLLAPSES a run of tabs into one +# delimiter and empty fields vanish, shifting every field after them. 316 of the +# 319 seed entries have an empty `parent`, so for nearly the whole registry: +# +# proven fv [] standalone Formally verified… hyperpolymath +# ^^ empty parent collapses +# -> parent="Formally verified…" description="hyperpolymath" owner="" +# +# The damage is real and committed: 153 CLADE.a2ml files across the estate carry +# `rationale = ""` with the repo's DESCRIPTION sitting in `parent` (panic-attack, +# flat-mate, rpa-elysium, live-files, …). Repairing those files is a separate, +# owner-facing job — this only stops the script producing more. +# +# It also silently defeated the `owner` support added in #48: $7 was always empty, +# so `owner` always fell back to "hyperpolymath" and an explicit +# `owner = "metadatastician"` in the seed was ignored. export-json.sh never had +# this bug — awk -F'\t' does not collapse — which is why the two derivation sites +# disagreed and why #48's byte-identical regression test did not catch it. +# +# US (0x1f) is not IFS whitespace, so runs are not collapsed and empty fields +# survive. It cannot occur in the data (checked: 0 occurrences in repos.a2ml) and +# is exactly what the ASCII unit separator is for. +while IFS=$'\037' read -r name primary secondary lineage parent description owner; do deploy_clade "$name" "$primary" "$secondary" "$lineage" "$parent" "$description" "$owner" -done < <(parse_repos) +done < <(parse_repos | tr '\t' '\037') echo "" echo "=== Summary ===" diff --git a/verisim/seed/clades.a2ml b/verisim/seed/clades.a2ml index f048ab5..d05f232 100644 --- a/verisim/seed/clades.a2ml +++ b/verisim/seed/clades.a2ml @@ -1,6 +1,56 @@ # SPDX-License-Identifier: MPL-2.0 # Clade taxonomy definitions for the hyperpolymath ecosystem # 12 top-level clades — each repo gets exactly one primary clade +# +# =========================================================================== +# READ THIS BEFORE ASSIGNING A CLADE — HUMAN OR BOT +# +# THIS IS A CLOSED TAXONOMY OF CATEGORIES. It is not an abbreviation scheme. +# +# The two letters abbreviate the NAME OF THE CLADE. They never abbreviate the +# name of the repo. There are exactly 12 codes and no thirteenth may be coined: +# +# fv Formal Verification & Proofs nl Nextgen Languages +# rm Repo Management & Tooling gv Governance & Standards +# db Databases ap Applications +# ix Infrastructure & Cloud dx Developer Ecosystem +# pt Protocols & Interop ax AI & Neurosymbolic +# gm Games & Interactive sc Security +# +# You pick the CATEGORY the repo belongs to, then write down that category's +# code. You do NOT look at the repo's name and find two letters that fit it. +# +# This warning exists because that is exactly what happened, more than once: +# +# paint-type chose `pt` reading it as "PainT-type" +# -- `pt` is Protocols & Interop. paint-type is an image +# editor. It is `ap` (Applications). +# gossamer chose `gv` reading it as "Graphical/Visual" +# -- `gv` is GoVernance & Standards. There is no graphical +# clade. A webview shell is `dx` (Developer Ecosystem). +# +# Both codes were VALID, so every check passed. The repos were simply filed +# under a category they have nothing to do with. `primary-name` (below) exists +# to make that failure impossible; see CLADE-006 in +# contractiles/must/clade-hygiene.a2ml. +# +# HOW TO CHOOSE. From the spec (docs/SPEC-clade-verisim-portal.adoc): +# "The primary clade reflects the project's core value proposition, not its +# implementation details." Ask what the repo is FOR, not what it is built with. +# A game written in Idris2 is `gm`, not `fv`. A webview shell with formal ABI +# proofs is what developers build on, not a proof project. +# +# EVERY CLADE.a2ml MUST DECLARE BOTH: +# +# [clade] +# primary = "ap" +# primary-name = "Applications" # must match `name` below for that code +# +# The redundancy is deliberate: the code alone cannot express a wrong belief +# about what it means, but the pair can — and CLADE-006 rejects a pair that +# disagrees with this file. Writing primary = "pt" while believing it means +# "paint-type" now fails a gate instead of passing silently. +# =========================================================================== [meta] version = "1.0.0"