docs: de-conflate KRL from Tangle, restate the readiness grade honestly#54
Merged
Conversation
The three projects are distinct and were built for different purposes. QuandleDB is the knot database. KRL is its resolution language, developed alongside it. Tangle is a separate, general language for knot mathematics that happens to share the subject matter. Documentation in this repository had fused KRL and Tangle into a single compilation pipeline that does not exist. README.md * Removed the claim that KRL "lowers through TangleIR into Tangle-level computation", and the layer table presenting Tangle as KRL's substrate. `TangleIR` appears 0 times in the KRL implementation; the struct definitions the README documented as "the single hardest-designed artifact in the stack" correspond to no code. * Removed `KRLAdapter.jl` as the named canonical implementation. It no longer exists. A short note records that both claims were false, so the correction is legible rather than silent. * Removed the `TanglePL` usage example, which imports packages that do not exist. * Restated what the repository actually holds, and what it does not: there is no parser here, so nothing in this tree can execute a KRL program. * Added the known divergence between this repository's grammar and QuandleDB's — disjoint on core vocabulary, with `|` bound to opposite meanings. * Restructured to a single <h1>. Ddraig SSG certifies pages against a decidable a11y predicate requiring exactly one <h1> and no heading-level skips; the old README had 8, which is why GitHub Pages was failing. Verified by compiling Ddraig locally and running it: old README FAIL (exit 1), new README ok (exit 0). READINESS.md * Grade D -> E. The entire evidence base for D was a parser, AST, lowering pass and 57-test matrix in `KRLAdapter.jl`, which no longer exists, so none of it can be checked. The CRG demotion table gives `D -> E` for "the scope narrows so far that the component barely does anything", which is what happened. * Replaced the evidence section with checks that were executed on 2026-07-21: grammar smoke 20/20, zig build test 3/3, aspect 4/4, e2e 4/4. * Documented the limitations plainly, including that no conformance suite exists, so "conforms to the KRL spec" is not currently a checkable claim. * Removed the duplicated "Path to C"/"Path to B" sections. ASSUMPTIONS.md * Added a Status column. Seven DESIGN assumptions named code in `KRLAdapter.jl`. A DESIGN assumption is defined in this file as "true by construction in our code" — with the code gone there is no construction left to be true by. * A-KR-1.1, 1.2, 2.1, 3.2, 4.1 marked UNANCHORED; A-KR-6.1 and 6.2 marked VOID (both presuppose two implementations, and only one exists). * Verified that no re-anchoring is possible: `sigma`, `cup`, `cap`, `r1_simplify` and any pretty-printer appear 0 times in `quandledb/server/krl/`. The braid generators these assumptions describe are implemented nowhere. * The four MATH assumptions are untouched — they rest on external theorems. TOPOLOGY.md * Was pure RSR-template residue describing the template itself, its dogfood gate, and "500+ RSR-based repositories" downstream. Replaced with KRL's actual topology: the three project boundaries, the ABI/FFI layering, and the spec/implementation seam that no conformance suite currently checks. * States that this repository exposes no Groove service and has no `.well-known/groove/manifest.json`, rather than implying one exists.
|
hyperpolymath
marked this pull request as ready for review
July 21, 2026 13:08
This was referenced Jul 21, 2026
Merged
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…ed (#55) Follows #53 and #54. The Dogfood Gate **could not parse** before #53, so it never ran. Now that it parses, it runs — and immediately reported **2 A2ML errors and 4 K9 errors** on `main`. That's the gate working as intended; this PR clears what it found. Each fix was verified by running the **actual validator** locally, not by reading its source. ## A2ML: 2 errors → 0 ### `docs/governance/TSDM.a2ml` was not defective — the pin was stale This is the [SHA-pinning-defeats-upstream-fixes](https://github.com/hyperpolymath/krl) pattern, caught red-handed: | | | |---|---| | Pinned | `6bff6ec` — PR **#26**, *"recognise s-expression identity/version fields"* | | Fix needed | `6c47174` — PR **#41**, *"recognise colon/brace-block identity"* | TSDM.a2ml declares `id: "tsdm-standard"`, the colon/brace-block form. The validator's own source comment **names this exact file** as the motivating case — so the fix existed upstream, and the pin predated it. Confirmed before changing anything: running the newer validator locally drops the count **2 → 1**. Bumped to current main (`5468b7f`). ### `docs/governance/MAINTENANCE-CHECKLIST.a2ml` genuinely lacked identity The validator exempts four categories — `*AI-MANIFEST*` files, `.machine_readable/` (structural identity), contractile `@directive` shape, and named typed manifests. **None applies here**, and the file has no `name`/`project`/`agent-id`. Added `name` to its `[metadata]` block. ## K9: 4 errors → 0 Unlike the A2ML case, these are **genuine file defects** — the current validator reports the same 4 errors as the pinned one, so pin staleness is ruled out. - Both `container/deploy.k9.ncl` and `.machine_readable/self-validating/methodology-guard.k9.ncl` were missing the mandatory **`K9!` magic number** on line 1. - `deploy.k9.ncl` had `pedigree = component_pedigree,` where the canonical template (`rsr-julia-library-template-repo`) has `pedigree = component_pedigree & { name = "…" },`. Without the merge the pedigree carries no name. Matched to the template. - `methodology-guard.k9.ncl` had **no pedigree block at all**. Added one. > This is template rot with a measurable blast radius: `container/deploy.k9.ncl` is missing the `K9!` line in **6 repos** (lucidscript, pandoc-k9, pseudoscript, squeakwell, stateful-artefacts, systemet) while the newer template has it. ##⚠️ `K9!` and Nickel contradict each other, estate-wide Worth recording, and **not** changed here: ```console $ nickel typecheck container/deploy.k9.ncl error: unexpected token 1 │ K9! │ ^ ``` The magic number **is not valid Nickel**, so `nickel typecheck` fails on *every* `.k9.ncl` in the estate that carries it — including the canonical template and every currently-passing file. `k9-svc` evidently strips the line before parsing. The consequence is that the `nickel typecheck container/deploy.k9.ncl` usage line **in these files' own headers can never succeed as written**. Pre-existing and estate-wide, so left alone. But I used it as a check: both files were typechecked with the magic line stripped, and **that caught a real error in my first draft**, where the new pedigree block sat at top level in a file whose body is `let … in …` — invalid Nickel. Moved inside the record; the validator matches at any indent. ## Verified | Check | Result | |---|---| | K9 validator | **0 errors** (8 files) | | A2ML validator | **0 errors** (121 files) | | `actionlint` | **0 errors** | | `tests/aspect_tests.sh` | 4/4 | | `tests/e2e.sh` | 4/4 | | `tests/smoke/grammar_smoke.sh` | 20/20 |
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…andards pins (#56) Both failing Governance jobs are root-caused and fixed. Follows #53, #54, #55. ## `Workflow security linter` ``` ERROR: .github/workflows/pages.yml missing SPDX header ``` `pages.yml` arrived in #51 and begins directly at `name:`. Every other workflow already carries the header; this was the only one. > **Recording a correction against myself.** Earlier in this programme I audited all workflows, reported that every one had both an SPDX header *and* a top-level `permissions:` block, and marked the SPDX hypothesis **disproved**. That audit was wrong — it must have run against a tree without `pages.yml`. The real cause is exactly the one first suspected. A "disproved" hypothesis is only as good as the test that disproved it. ## `Check Workflow Staleness` ``` governance-reusable.yml pin d7c22711e830 is 63 commit(s) / 24d behind standards HEAD — outside the recency window (>50 commits AND >14d). Refresh toward f9dca6ded2ca ``` Three callers were pinned at `d7c22711e830`: | Workflow | From | To | |---|---|---| | `governance-reusable.yml` | `d7c22711e830…` | `f9dca6ded2cad8ab54044c1cb0489b558ae2682b` | | `hypatia-scan-reusable.yml` | `d7c22711e830…` | `f9dca6ded2cad8ab54044c1cb0489b558ae2682b` | | `scorecard-reusable.yml` | `d7c22711e830…` | `f9dca6ded2cad8ab54044c1cb0489b558ae2682b` | Full 40-char SHAs — the gate's message quotes the abbreviated form, which would weaken the pin. ### Deliberately not touched - **`mirror-reusable.yml`** (`d135b05`) and **`secret-scanner-reusable.yml`** (`c65436e`) — neither was flagged by the staleness gate, and the secret-scanner pin in particular **should not be moved independently of the gitleaks allowlist work**, since re-pinning consumers ahead of the config work reintroduces false positives. - **`scorecard-enforcer.yml`** — the gate asks for its removal, but **this repo doesn't have that file**. That clause is generic advice in the reusable's message, not a finding against krl. ## Note on bumping toward standards HEAD The newer `governance-reusable` has *more* real checks than the pinned one (its previously-dead docs and Guix/Nix jobs were made real, warn-first until 2026-08-21). So this bump may surface new warnings. That is the gate working, and warn-first means it should not turn the build red. ## Verified `actionlint` **0 errors** · all **18** workflows carry an SPDX header
hyperpolymath
added a commit
to hyperpolymath/tangle
that referenced
this pull request
Jul 21, 2026
…ws (#78) The tangle half of a coordinated two-repo de-conflation pass. The krl half is hyperpolymath/krl#53 (merged) and hyperpolymath/krl#54. ## The three projects are separate **Tangle** is a general language for knot mathematics — topological, algebraic, geometric, logical. **QuandleDB** is a knot database. **KRL** is QuandleDB's resolution language, developed jointly with it. They share a subject matter, not an architecture. Documentation here presented Tangle as the substrate of a KRL compilation stack. That is false in both directions, and the connecting layer does not exist: > **`TangleIR` appears in NO source file in this repository** — 0 hits across `.rs`, `.zig` and `.lean` — **and in NO source file in the KRL implementation.** It existed only in prose, in both repos. The relationship between the projects is left intact. What is removed is a claimed architectural dependency that was never built. ## README.adoc - Retitled from *"Tangle / KRL — Topological Programming Language"* to **"Tangle — a general language for knot mathematics"**; removed *"Tangle (via KRL — Knot Resolution Language) is…"* from the opening line. - Removed the `KRL → TangleIR → Tangle core → QuandleDB + Skein.jl` ladder. - Removed the `== KRL — Knot Resolution Language` section, which restated KRL's four operations as though KRL were *this* project's surface language. - **Strengthened the formal core with a result rather than a claim** (below). - Added an explicit note that only the Lean proofs are CI-gated. ## The formal core is real — and now verified I ran the repository's own documented oracle: ```console $ cd proofs && lean Tangle.lean $ echo $? 0 ``` | Check | Result | |---|---| | `lean Tangle.lean` (pinned `leanprover/lean4:v4.14.0`) | **exit 0, no errors** | | `sorry` count | **0** | | `axiom` count | **0** | | `import` lines | **0** — self-contained, no Mathlib | | `progress`, `preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete`, `infer_iff_hasType` | all present with real proof terms | This is worth stating precisely: an `axiom` stub compiles cleanly while proving nothing, so *"the Lean build is green"* and *"the theorems are proved"* are different claims in general. **Here they coincide, and that was checked rather than assumed.** This is Tangle's strongest asset and the README now leads with it. ## AFFIRMATION.adoc — erratum, not edit An affirmation is a dated claim about a past state (`102499d`, 2026-06-19); amending it in place would falsify a record. So the original text is untouched and an erratum is appended. It corrects the *"maintainer-confirmed"* `KRL → TangleIR → VerisimCore → Skein/QuandleDB` stack, and flags that the quotable one-line characterisation shouldn't be quoted while it calls Tangle *"the … TangleIR of the KRL stack"*. It also **discharges one of the affirmation's own acknowledged gaps** — it recorded *"OCaml + Lean not run (absent)"* and concluded *"structure + the repo's proof records are confirmed, not a fresh green build."* The Lean half is now closed, with command and exit code recorded. ## READINESS.md — Grade C → D Grade C means *self-validated in the home context*; the `D → C` trigger is *"dogfood it hard in the home context."* The assessment cited **exactly one** piece of dogfooding evidence: > **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL That is false — KRL is not built on Tangle. With it withdrawn, C is unsupported. Two further corrections: - **"CI: Clean" was false** — `main` was failing Governance and both Jekyll workflows. - **The test suites are not run by CI.** Eight OCaml test files exist under `compiler/test/`, but **no workflow invokes `dune` or `cargo test`**. The cheapest available uplift is named explicitly: add a workflow running `dune build && dune test`. Eight suites already exist and nothing executes them. ## dialects/README.md - Removed KRL from the dialect table — it was listed as a dialect that had "graduated", and it was never a Tangle dialect. - Replaced the dead absolute path `/var/mnt/eclipse/repos/krl` (another machine) with the GitHub URL. - Dropped "wire through to TangleIR" from the maturation pattern. ## Workflows — two deleted `jekyll.yml` and `jekyll-gh-pages.yml` are GitHub's **sample** Jekyll workflows. This repo has **no `_config.yml` and no `Gemfile`** — there is no Jekyll site to build, so both fail on every push. `pages.yml` (Ddraig SSG, #73) is the real one; three workflows were competing for the same Pages deployment. ##⚠️ Owner action — GitHub Pages is not enabled `pages.yml` will **still** fail at the deploy step after this PR. Its build succeeds and certifies a11y, but: ``` GET /repos/hyperpolymath/tangle/pages -> 404 Not Found ``` which surfaces as `HttpError: Not Found / Creating Pages deployment failed`. **The same is true of `hyperpolymath/krl`.** Pages needs enabling with source = GitHub Actions on both. That publishes a public site, so I've left it to you rather than doing it. ## Verified on this branch `actionlint` 0 errors · `asciidoctor` renders `README.adoc` and `AFFIRMATION.adoc` clean · `lean Tangle.lean` exit 0
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Follows #53. Same Part 1 remit: make
maingreen and honest. This half is the documentation de-conflation.The three projects are distinct
QuandleDB is the knot database. KRL is its resolution language, developed alongside it. Tangle is a separate project — a general language for knot mathematics (topological, algebraic, geometric, logical) that happens to share the subject matter. Documentation here had fused KRL and Tangle into a single compilation pipeline that does not exist.
The relationship between KRL and QuandleDB is left intact — it is real and deliberate. What is removed is the false identity with Tangle, not the shared domain.
README.md
TangleIRappears 0 times in the KRL implementation — the struct definitions the README documented as "the single hardest-designed artifact in the stack" correspond to no code.KRLAdapter.jlas the named canonical implementation. It no longer exists.TanglePLusage example, which imports packages that don't exist.|is bound to opposite meanings (tensor here, pipeline there).This also fixes the GitHub Pages failure
Root cause was not generic: Ddraig SSG certifies pages against a decidable a11y predicate requiring exactly one
<h1>and no heading-level skips. The old README had 8<h1>s:Verified by compiling Ddraig locally (Idris2) and running the real certifier:
origin/main(old)[a11y FAIL]— exit 1[a11y ok]— exit 0READINESS.md — Grade D → E
The entire evidence base for Grade D was a parser, AST, lowering pass and 57-test matrix in
KRLAdapter.jl. That repository no longer exists, so none of it can be checked. The CRG demotion table givesD → Efor "the scope narrows so far that the component barely does anything" — which is exactly what happened.Replaced with evidence executed on 2026-07-21: grammar smoke 20/20,
zig build test3/3, aspect 4/4, e2e 4/4. Limitations stated plainly, including that no conformance suite exists, so "conforms to the KRL spec" is not currently a checkable claim.This is a correction to the record, not a regression in the work.
ASSUMPTIONS.md
Seven DESIGN assumptions named code in
KRLAdapter.jl. The file defines a DESIGN assumption as "true by construction in our code" — with the code gone, there is no construction left to be true by.Verified that no re-anchoring is possible:
sigma,cup,cap,r1_simplifyand any pretty-printer appear 0 times inquandledb/server/krl/. The braid generators these assumptions describe are implemented nowhere.The four MATH assumptions are untouched — they rest on external theorems.
TOPOLOGY.md
Was pure RSR-template residue describing the template itself, its dogfood gate, and "500+ RSR-based repositories" downstream. Replaced with KRL's actual topology: the three project boundaries, the ABI/FFI layering, and the spec/implementation seam that no conformance suite currently checks.
States that this repo exposes no Groove service and has no
.well-known/groove/manifest.json, rather than implying one exists.Verified on this branch
actionlint0 errors · aspect 4/4 · e2e 4/4 · smoke 20/20 · Ddraig a11y okThe matching de-conflation pass on
hyperpolymath/tangle(whose README is titled "Tangle / KRL") follows separately.