From 558f6318fa7fc4fddb360a671ded6f2cb11714bd Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 15:55:19 +0100 Subject: [PATCH 1/3] docs: de-conflate Tangle from KRL; drop two dead Jekyll Pages workflows MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tangle, KRL and QuandleDB are three separate projects that share a subject matter. Documentation here presented Tangle as the substrate of a KRL compilation stack, which is not true in either direction. 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 sentence and the "Tangle/KRL" framing from the status and summary sections. * Removed the architecture ladder KRL -> TangleIR -> Tangle core -> QuandleDB + Skein.jl. `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 repositories. * Removed the "== KRL — Knot Resolution Language" section, which restated KRL's four operations as though KRL were this project's surface language. Replaced with a "Relationship to KRL and QuandleDB" section stating the three projects' actual boundaries. The relationship is left intact — what is removed is a claimed architectural dependency that does not exist. * Strengthened the formal-core section with a result rather than a claim: the repository's own oracle, `cd proofs && lean Tangle.lean`, was executed on 2026-07-21 and exits 0. The proofs are self-contained (Tangle.lean has no import lines, so no Mathlib) and contain 0 `sorry` and 0 `axiom` across 2,128 lines, with progress, preservation, determinism, type_safety, infer_sound, infer_complete and infer_iff_hasType all carrying real proof terms. "Builds" and "proved" coincide here, which is not automatic. * Added an explicit note that only the Lean proofs are CI-gated: the OCaml compiler, the Rust components and the Zig components are built by no workflow. AFFIRMATION.adoc * Appended an erratum rather than editing the text. An affirmation is a dated claim about a past state; amending it in place would falsify a record. * Corrects the "maintainer-confirmed" stack KRL -> TangleIR -> VerisimCore -> Skein/QuandleDB, and flags that the quotable one-line characterisation should not be quoted while it describes Tangle as "the ... TangleIR of the KRL stack". * 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 of that gap is now closed, with the command and exit code recorded. READINESS.md — grade C -> D * Grade C means self-validated in the home context, and the D -> C trigger is "dogfood it hard in the home context". The assessment cited exactly one piece of dogfooding evidence: "Used internally as host for the KRL DSL". That is false, so C is unsupported. * "CI: Clean" was also false — main was failing Governance and both Jekyll Pages workflows. * The 8 OCaml test suites under compiler/test/ are real but are run by no workflow, so their passing state is unverified by this repo's own CI. * Recorded the verified Lean result as the evidence that does hold, and named the cheapest uplift: add a workflow that runs `dune build && dune test`. dialects/README.md * Removed KRL from the dialect table. It was listed as a dialect that had "graduated" to its own repo; it was never a Tangle dialect. * Replaced the dead absolute path /var/mnt/eclipse/repos/krl with the GitHub URL. * Dropped "wire through to TangleIR" from the maturation pattern, and noted that no dialect has yet made that journey, so there is no precedent. * Softened the multi-DSL-host claim: the sketches set out what such a host would cover, but nothing is implemented and nothing is built on Tangle, so they do not yet evidence it. Workflows * Deleted .github/workflows/jekyll.yml and .github/workflows/jekyll-gh-pages.yml. Both are GitHub's sample Jekyll workflows; this repository has no _config.yml and no Gemfile, so there is no Jekyll site to build and both fail on every push to main. pages.yml (Ddraig SSG, landed in #73) is the real one, and three workflows were competing for the same Pages deployment. NOTE: pages.yml will still fail at the deploy step. Its build succeeds and certifies a11y, but GitHub Pages is not enabled for this repository — /repos/hyperpolymath/tangle/pages returns 404, which surfaces as "HttpError: Not Found / Creating Pages deployment failed". That is a repository setting, not a code change, and is left for the owner. --- .github/workflows/jekyll-gh-pages.yml | 48 ----- .github/workflows/jekyll.yml | 62 ------- AFFIRMATION.adoc | 64 +++++++ READINESS.md | 115 +++++++++--- README.adoc | 247 ++++++++++++-------------- dialects/README.md | 36 ++-- 6 files changed, 299 insertions(+), 273 deletions(-) delete mode 100644 .github/workflows/jekyll-gh-pages.yml delete mode 100644 .github/workflows/jekyll.yml diff --git a/.github/workflows/jekyll-gh-pages.yml b/.github/workflows/jekyll-gh-pages.yml deleted file mode 100644 index cd05ddc..0000000 --- a/.github/workflows/jekyll-gh-pages.yml +++ /dev/null @@ -1,48 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Sample workflow for building and deploying a Jekyll site to GitHub Pages -name: Deploy Jekyll with GitHub Pages dependencies preinstalled -on: - # Runs on pushes targeting the default branch - push: - branches: ["main"] - # Allows you to run this workflow manually from the Actions tab - workflow_dispatch: -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: - contents: read - pages: write - id-token: write -# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. -# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. -concurrency: - group: "pages" - cancel-in-progress: false -jobs: - # Build job - build: - runs-on: ubuntu-latest - timeout-minutes: 15 - steps: - - name: Checkout - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - - name: Setup Pages - uses: actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d # v6.0.0 - - name: Build with Jekyll - uses: actions/jekyll-build-pages@44a6e6beabd48582f863aeeb6cb2151cc1716697 # v1 - with: - source: ./ - destination: ./_site - - name: Upload artifact - uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v4 - # Deployment job - deploy: - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - runs-on: ubuntu-latest - timeout-minutes: 15 - needs: build - steps: - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5.0.0 diff --git a/.github/workflows/jekyll.yml b/.github/workflows/jekyll.yml deleted file mode 100644 index f097625..0000000 --- a/.github/workflows/jekyll.yml +++ /dev/null @@ -1,62 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# This workflow uses actions that are not certified by GitHub. -# They are provided by a third-party and are governed by -# separate terms of service, privacy policy, and support -# documentation. - -# Sample workflow for building and deploying a Jekyll site to GitHub Pages -name: Deploy Jekyll site to Pages -on: - # Runs on pushes targeting the default branch - push: - branches: ["main"] - # Allows you to run this workflow manually from the Actions tab - workflow_dispatch: -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: - contents: read - pages: write - id-token: write -# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. -# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. -concurrency: - group: "pages" - cancel-in-progress: false -jobs: - # Build job - build: - runs-on: ubuntu-latest - timeout-minutes: 15 - steps: - - name: Checkout - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - - name: Setup Ruby - # https://github.com/ruby/setup-ruby/releases/tag/v1.207.0 - uses: ruby/setup-ruby@003a5c4d8d6321bd302e38f6f0ec593f77f06600 - with: - ruby-version: '3.1' # Not needed with a .ruby-version file - bundler-cache: true # runs 'bundle install' and caches installed gems automatically - cache-version: 0 # Increment this number if you need to re-download cached gems - - name: Setup Pages - id: pages - uses: actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d # v6.0.0 - - name: Build with Jekyll - # Outputs to the './_site' directory by default - run: bundle exec jekyll build --baseurl "${{ steps.pages.outputs.base_path }}" - env: - JEKYLL_ENV: production - - name: Upload artifact - # Automatically uploads an artifact from the './_site' directory by default - uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v4 - # Deployment job - deploy: - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - runs-on: ubuntu-latest - timeout-minutes: 15 - needs: build - steps: - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5.0.0 diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 265e72b..8b4dec1 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -220,3 +220,67 @@ un-run toolchains stated rather than implied. `-S`; the signed git commit over this content, at the SHA above, is the authoritative form. * *Signed-off-date:* (fill on signing) + +''' + +== Erratum — 2026-07-21 + +This section corrects the affirmation above. The original text is left intact: +an affirmation is a dated claim about a past state, and amending it in place +would falsify a record. Two of its claims have since been shown to be wrong, +and one of its acknowledged gaps has since been closed. + +=== Correction 1 — the stack does not exist + +The affirmation records, as *maintainer-confirmed*, the ladder: + +[literal] +KRL -> TangleIR -> VerisimCore -> Skein/QuandleDB + +`TangleIR` does not exist. The identifier appears in *no source file* in this +repository (0 hits across `.rs`, `.zig` and `.lean`) and in *no source file* in +the KRL implementation at `quandledb/server/krl/`. It existed only in prose, in +both repositories, and has been removed from `README.adoc`. + +Nor is KRL a surface language for Tangle. KRL is QuandleDB's resolution +language, developed jointly with QuandleDB; it neither compiles to nor depends +on Tangle. The three projects share a subject matter, not an architecture. + +The confirmation recorded on 2026-06-19 was a confirmation of the README's +diagram, and that diagram was wrong. Nothing here suggests bad faith — the +affirmation is careful, and states plainly which of its checks were not run. + +=== Correction 2 — the "one-line characterisation" should not be quoted as-is + +The characterisation invites quotation. It should not be quoted while it +describes Tangle as "the proven type-safe small-step core + TangleIR of the KRL +stack". Everything else in that sentence survives: the OCaml compiler, the Rust +LSP/WASM targets, the Lean 4 proofs and the five dialects are all real. + +=== Discharge — the Lean proofs have now been run + +The affirmation states: *"OCaml + Lean not run (absent)"*, and concludes that +*"structure + the repo's proof records are confirmed, not a fresh green build"*. + +That gap is now closed for Lean. On 2026-07-21 the repository's own documented +oracle was executed: + +[source,console] +---- +$ cd proofs && lean Tangle.lean +$ echo $? +0 +---- + +Exit 0, no errors, using the pinned toolchain from `proofs/lean-toolchain` +(`leanprover/lean4:v4.14.0`). The proofs are self-contained — `Tangle.lean` has +no `import` lines at all, so no Mathlib — and contain *zero* occurrences of +`sorry` and *zero* `axiom` declarations across 2,128 lines. `progress`, +`preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete` +and `infer_iff_hasType` are all present with real proof terms. + +This matters because "the Lean build is green" and "the theorems are proved" are +not the same claim in general: an `axiom` stub compiles cleanly while proving +nothing. Here they coincide, and that was checked rather than assumed. + +The OCaml compiler remains unbuilt — no workflow in this repository builds it. diff --git a/READINESS.md b/READINESS.md index 699ec03..c150e38 100644 --- a/READINESS.md +++ b/READINESS.md @@ -6,45 +6,116 @@ Copyright (c) Jonathan D.A. Jewell # Component Readiness — Tangle (language) -**Current Grade:** C -**Assessed:** 2026-04-05 +**Current Grade:** D +**Assessed:** 2026-07-21 (demoted C → D) **Standard:** [CRG v2.0 STRICT](../standards/component-readiness-grades/) -## Grade rationale (evidence for C) +## Why the grade moved C → D -Works reliably on own project + annotated. Tangle is a Turing-complete -topological programming language with a compiler, LSP, and wasm backend. +Grade C means *self-validated in the home context*; the D → C promotion trigger +is *"dogfood it hard in the home context."* The previous assessment cited +exactly one piece of dogfooding evidence: -### Evidence +> **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL -- **Tests:** 6 dune test suites (parser, typecheck, eval, e2e, property, compositional) -- **Annotation:** 8 per-directory READMEs across compiler/, lib/, examples/, docs/ -- **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL -- **RSR compliance:** 0-AI-MANIFEST.a2ml, `.machine_readable/6a2/`, 14+ workflows, SECURITY/CONTRIBUTING/CODE_OF_CONDUCT, EXPLAINME.adoc, TEST-NEEDS.md, PROOF-NEEDS.md -- **Formal proofs:** Lean 4 proofs for progress, preservation, determinism -- **WASM backend:** Compositional PD compiler with wasm codegen -- **CI:** Clean; panic-attack assail 0 findings +**That is not true.** KRL is not built on Tangle. KRL is QuandleDB's resolution +language, developed jointly with QuandleDB; it neither compiles to nor depends +on Tangle, and the `TangleIR` layer that was supposed to connect them does not +exist in any source file in either repository. See the erratum in +`AFFIRMATION.adoc`. + +With that claim withdrawn there is no dogfooding evidence, so C is not +supported. Two further corrections to the previous assessment: + +- **"CI: Clean" was false.** At the time of this assessment `main` was failing + Governance and both Jekyll Pages workflows. +- **The test suites are not run by CI.** Eight OCaml test files exist under + `compiler/test/`, but no workflow in this repository invokes `dune` or + `cargo test`. Their passing state is unverified by this repository's own CI. + +This is a correction to the record, not a regression in the work. The formal +core in particular got *stronger* this cycle — see below. + +--- + +## Grade rationale (evidence for D) + +Grade D: *"works on some inputs, some cases, or some configurations, but not +systematically … either needs to be narrowed in scope so that its documented +capabilities match its actual capabilities, or needs the inconsistencies +fixed."* Narrowing the documented scope is exactly what this revision does. + +### Verified evidence + +| Artefact | Check | Result | +|---|---|---| +| `proofs/Tangle.lean` | `cd proofs && lean Tangle.lean` (the repo's own documented oracle) | **exit 0, no errors** | +| `proofs/Tangle.lean` | `sorry` count | **0** | +| `proofs/Tangle.lean` | `axiom` count | **0** | +| Theorems | `progress`, `preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete`, `infer_iff_hasType` | all present with real proof terms | +| Dependencies | `import` lines in `Tangle.lean` | **0** — self-contained, no Mathlib | + +Run on 2026-07-21 with the pinned toolchain (`leanprover/lean4:v4.14.0`). This +is worth stating precisely: a Lean file full of `axiom` stubs compiles cleanly +while proving nothing, so "the build is green" and "the theorems are proved" are +different claims. Here they coincide, and that was checked. + +### Present but unverified + +- **OCaml compiler** (`compiler/`) — lexer, parser, AST, typechecker, evaluator, + pretty-printer, REPL, braid equivalence, LSP and WASM targets. Not built by + any workflow. +- **Test suites** — 8 files under `compiler/test/` (`test_parser`, + `test_typecheck`, `test_eval`, `test_e2e`, `test_property`, + `test_compositional`, `test_check`, `test_roundtrip`) plus `tg3`/`tg5`/`tg7`/ + `tg8` directories. Not run by any workflow. +- **Rust / Zig components** — 18 `.rs`, 3 `.zig`. Not built by any workflow. +- **Five dialects** — grammar sketches only. + +### Structural evidence + +- Per-directory README annotation across `compiler/`, `dialects/`, `docs/`. +- RSR compliance: `0-AI-MANIFEST.a2ml`, `.machine_readable/6a2/`, workflows, + SECURITY / CONTRIBUTING / CODE_OF_CONDUCT, `EXPLAINME.adoc`, `TEST-NEEDS.md`, + `PROOF-NEEDS.md`. + +--- ## Gaps preventing higher grades +### Blocks C (self-validated in the home context) + +1. **No CI gate on the implementation.** The OCaml compiler, its 8 test suites, + and the Rust and Zig components are not built or run by any workflow. Until + they are, "works reliably" is not an evidenced claim. This is the single + highest-value fix available to this repository. +2. **No dogfooding.** Nothing is currently built on Tangle. The previous claim + to the contrary was false. + ### Blocks B (6+ diverse external targets) + - No external language users outside hyperpolymath. -- KRL is the only DSL built on Tangle so far — need 5 more distinct domain DSLs - to demonstrate the host-language claim. - No external submissions to language research venues confirming the phase separation or compositional PD model. ### Blocks A + - Requires B first. -## What to do for B +--- + +## What to do next -1. Build 5 more DSLs on top of Tangle (not just KRL) — e.g. a braid-group - calculus, a category-theory calculus, a quantum-circuit calculus. -2. Get external feedback on the surface syntax and compiler from language - researchers. -3. Track the 6 targets here. +1. **Add a workflow that runs `dune build && dune test`.** Eight test suites + already exist; nothing executes them. This is the cheapest available uplift + and is a precondition for any claim above D. +2. Add a workflow that builds the Rust and Zig components. +3. Build something real on Tangle, in its own right — a braid-group calculus, a + category-theory calculus, a quantum-circuit calculus. The five dialects are + the natural candidates and currently exist only as grammar sketches. + Note that this must be genuine dogfooding of *Tangle*; KRL does not count and + never did. ## Review cycle -Reassess per release. Next review: on any compiler/LSP/wasm behavioural change. +Reassess when the compiler is built and its tests are run by CI. diff --git a/README.adoc b/README.adoc index bcb98df..9b2ad85 100644 --- a/README.adoc +++ b/README.adoc @@ -2,37 +2,39 @@ // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell -= Tangle / KRL — Topological Programming Language += Tangle — a general language for knot mathematics image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/tangle"] image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] image:https://api.thegreenwebfoundation.org/greencheckimage/github.com[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url=github.com"] -A research language exploring *computation as topology*, where programs are structured objects and equivalence is defined by transformation. +A research language for knots and their mathematics — topological, algebraic, +geometric and logical — in which programs are structured objects and equivalence +is defined by transformation. --- == Overview -Tangle (via KRL — Knot Resolution Language) is an experimental programming language in which: +Tangle is an experimental, Turing-complete programming language in which: -> *programs are structured as tangles (braids), and program equivalence is defined by isotopy.* +> *programs are structured as tangles (braids), and program equivalence is +> defined by isotopy.* -Rather than treating programs as sequences of instructions, Tangle treats them as *composable topological objects*. +Rather than treating programs as sequences of instructions, Tangle treats them +as *composable topological objects*. This allows reasoning about programs in +terms of structure, equivalence under transformation, and invariants of +representation. -This allows reasoning about programs in terms of: - -* structure -* equivalence under transformation -* invariants of representation +Its remit is deliberately broad: Tangle aims to be a general language for doing +mathematics *about* knots — not a front end to any particular knot database. --- -== Core Idea - -The central idea of Tangle is: +== Core idea -> *computation is construction of structured objects, and meaning is preserved under valid transformations.* +> *computation is construction of structured objects, and meaning is preserved +> under valid transformations.* In this setting: @@ -40,140 +42,148 @@ In this setting: * execution corresponds to transformation * equivalence is not syntactic equality, but *structural equivalence* -This aligns with concepts from: - -* knot theory (Reidemeister moves) -* category theory (morphisms and composition) -* algebraic invariants (classification via structure) +This aligns with concepts from knot theory (Reidemeister moves), category theory +(morphisms and composition), and algebraic invariants (classification via +structure). --- -== KRL — Knot Resolution Language - -KRL is the surface language used to interact with the system — a *resolution DSL*, -*not merely* a query language. +== Relationship to KRL and QuandleDB -It is organised around four fundamental operations: +Tangle is a *separate project* from KRL and QuandleDB. The three share a subject +matter, not an architecture. [cols="1,3"] |=== -|Operation |Role +|Project |What it is -|Construct -|Create or declare presentations, structures, claims, datasets +|*Tangle* (this repository) +|A general language for knot mathematics. Turing-complete. Independent of any + database. -|Transform -|Rewrite, normalize, compose, concatenate, permute, mutate +|https://github.com/hyperpolymath/quandledb[*QuandleDB*] +|A knot database — stores presentations, invariants, fingerprints, equivalence + classes and witnesses. -|Resolve -|Decide / disambiguate / evaluate equivalence or identity questions - -|Retrieve -|Inspect, fetch, project, explain, or return stored/computed results +|https://github.com/hyperpolymath/krl[*KRL*] +|QuandleDB's resolution language, developed jointly with it. Specified in the + `krl` repository, implemented in `quandledb/server/krl/`. |=== -KRL is not a general-purpose language; it is a *domain language for structured -objects and their equivalence*. *Retrieve* recovers resolution-relevant artefacts -(presentations, invariants, witnesses, equivalence classes, prior resolutions, -explanations, provenance) — it is *not* arbitrary database querying. See krl -`docs/decisions/0002-query-language-deferred.adoc`. - ---- +[IMPORTANT] +==== +Earlier revisions of this README were titled *"Tangle / KRL"* and described +Tangle as the substrate of a `KRL -> TangleIR -> Tangle core -> QuandleDB` +stack. That was wrong on both counts. -== Architecture +* KRL is not Tangle's surface language. It is QuandleDB's, and it neither + compiles to nor depends on Tangle. +* There is no `TangleIR`. The identifier appears in *no source file* in this + repository, nor in the KRL implementation — it existed only in prose. -Tangle is part of a layered system: +The projects remain related by domain and are developed by the same author; +what is removed here is a claimed architectural dependency that does not exist. +==== --- -KRL (surface language — resolution DSL, not merely a query language) -↓ -TangleIR (canonical interchange representation) -↓ -Tangle core (this repo — proven type-safe small-step semantics) -↓ -QuandleDB + Skein.jl (persistence + invariant/equivalence; computational engine) -------------------------------------------- +== Formal core -* *TangleIR* is the central representation shared across layers -* other components provide views, transformations, or storage +A core fragment of the language is formalised and mechanised in Lean 4. ---- +Verified on 2026-07-21 by running the repository's own oracle, +`cd proofs && lean Tangle.lean` — exit 0, no errors: -== Formal Core +[cols="2,1"] +|=== +|Property |Status + +|`progress` +|proved -A core fragment of the language has been formalised and mechanised. +|`preservation` +|proved -This includes: +|`determinism` +|proved -* a typed core language (braid words, composition, tensor) -* small-step operational semantics -* mechanised proofs in Lean 4: +|`type_safety` +|proved - * progress - * preservation - * determinism - * type safety - * decidability of type checking (`infer` ≡ `HasType`) +|Decidability of type checking (`infer` == `HasType`) +|proved +|=== -* *echo types* — structured loss as a type-system feature: `close` (braid - closure) is the canonical lossy map, and `echoClose`/`lower`/`residue` make - that loss recoverable at the type level (a simply-typed shadow of - hyperpolymath/echo-types). All four safety theorems cover them. +The proofs are self-contained (no Mathlib dependency) and contain *zero* uses of +`sorry` and *zero* `axiom` declarations across 2,128 lines — so "builds" and +"proved" mean the same thing here, which is not automatic. -See: +They cover *echo types*: structured loss as a type-system feature. `close` +(braid closure) is the canonical lossy map, and `echoClose`/`lower`/`residue` +make that loss recoverable at the type level — a simply-typed shadow of +https://github.com/hyperpolymath/echo-types[echo-types]. All four safety +theorems cover them. -* `proofs/Tangle.lean` (and `proofs/README.md` to build/verify) -* `docs/spec/FORMAL-SEMANTICS.md` -* `PROOF-NARRATIVE.md` / `PROOF-NEEDS.md` +See `proofs/Tangle.lean`, `proofs/README.md`, `docs/spec/FORMAL-SEMANTICS.md`, +and `PROOF-NARRATIVE.md` / `PROOF-NEEDS.md`. -This formal core covers the *structural heart of the language*, though not all surface features. +This formal core covers the structural heart of the language, though not all +surface features. --- -== Current Status +== Dialects -Tangle/KRL is an *active research system*. +Tangle's breadth is expressed as dialects, each with its own grammar sketch +under `dialects/`: -At present: +* `braid-calculus` — braid words and their relations +* `skein-algebra` — skein relations and invariant computation +* `string-diagram` — monoidal-category string diagrams +* `virtual-knot` — virtual knot theory +* `quantum-circuit` — circuits as topological objects -* grammar is defined (EBNF / PEG in progress) -* AST and type system are partially implemented -* compiler pipeline (AST → TangleIR) is in development -* decompilation (IR → source) is incomplete -* database integration (Skein / QuandleDB) is planned or partial +--- -It should be read as: +== Current status -> a formally grounded core with an evolving implementation and surrounding research system. +Tangle is an active research system. Read it as *a formally grounded core with +an evolving implementation around it*. ---- +[cols="1,2"] +|=== +|Area |State -== Scope +|Lean 4 formal core +|Verified — see above -=== Implemented / Grounded +|Grammars +|`src/tangle.ebnf`, `src/tangle-jtv.ebnf`, `spec/grammar.ebnf`, plus five + dialect sketches -* core grammar (defined) -* AST and type structure -* Lean formalisation of core fragment -* partial compiler pipeline -* example programs +|OCaml compiler (`compiler/`) +|Lexer, parser, AST, typechecker, evaluator, pretty-printer, REPL, braid + equivalence, plus LSP and WASM targets. *Not built by CI* ---- +|Rust / Zig components +|18 `.rs`, 3 `.zig`. *Not built by CI* -=== In Progress +|Database integration +|Not implemented +|=== -* parser and full compiler -* IR integration across components -* equivalence resolution via QuandleDB -* invariant-based querying +[NOTE] +==== +Only the Lean proofs are gated by CI (`.github/workflows/lean-proofs.yml`). +The OCaml compiler, the Rust components and the Zig components are not built by +any workflow, so their state is unverified by this repository's own CI. +==== --- -=== Research Directions +== Research directions * richer categorical abstractions -* deeper integration with algebraic databases * optimisation via equivalence classes * alternative evaluation models based on rewriting @@ -181,36 +191,15 @@ These are not yet stable features. --- -== Relationship to Other Projects - -Tangle is closely connected to: - -* *QuandleDB* — equivalence and classification via algebraic invariants -* *Skein.jl* — persistence and indexing of structured objects -* *Nextgen Languages* — broader research context - ---- - -== How to Read This Repository - -Recommended entry points: +== How to read this repository -* `Tangle.lean` — mechanised type safety proof +* `proofs/Tangle.lean` — mechanised type-safety proof (the load-bearing artefact) * `docs/spec/FORMAL-SEMANTICS.md` — formal model -* grammar files (`src/tangle.ebnf` or equivalent) -* examples demonstrating composition and transformation - ---- - -== Summary - -Tangle/KRL is best understood as: - -> a research language that treats programs as structured objects, with meaning defined by transformation and equivalence, supported by a partially mechanised formal core and an evolving implementation. - - -== License +* `src/tangle.ebnf` — surface grammar +* `dialects/` — the breadth of the language +* `compiler/lib/` — the OCaml front end -This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details. +== Licence -SPDX-License-Identifier: CC-BY-SA-4.0 +This project is licensed under the Mozilla Public License, v. 2.0. See the +`LICENSE` file for details. This document is CC-BY-SA-4.0. diff --git a/dialects/README.md b/dialects/README.md index 62a5641..1cc271e 100644 --- a/dialects/README.md +++ b/dialects/README.md @@ -15,23 +15,27 @@ coherent and could be built out, not a complete implementation. ## The pattern -When a DSL matures from sketch → alpha implementation, it should follow -the KRL precedent: +When a DSL matures from sketch → alpha implementation: 1. Start with an EBNF grammar sketch here (`grammar-sketch.ebnf`) 2. Write 1-3 example programs -3. When ready to implement: graduate to its own top-level repo (like `krl/`) -4. Implement parser in Tangle OCaml or sibling language -5. Wire through to TangleIR or its own IR type +3. When ready to implement, decide whether it stays in-tree or graduates to + its own repository +4. Implement the parser in Tangle's OCaml front end or a sibling language +5. Define its IR type -Keeping sketches here demonstrates Tangle's claim to be a general -multi-DSL host, not a single-purpose language. +No dialect has yet made this journey, so there is no precedent to follow — +these are all still at step 1. + +These sketches set out what a general multi-DSL host *would* cover. They do not +yet evidence the claim: nothing here is implemented, and nothing is currently +built on Tangle. Implementing one of them end to end is what would turn the +claim into evidence. ## Current scaffolds | Dialect | Status | Domain | |---|---|---| -| [krl](../../krl/) (separate repo) | grade E → D (v0.2 parser 2026-04-12) | Knot resolution — construct, transform, resolve, retrieve | | [braid-calculus](braid-calculus/) | sketch | Artin braid group Bn calculus | | [quantum-circuit](quantum-circuit/) | sketch | Quantum circuit compositional calculus | | [string-diagram](string-diagram/) | sketch | Monoidal/braided category string diagrams | @@ -40,10 +44,18 @@ multi-DSL host, not a single-purpose language. ## Relationship to KRL -KRL lives at `/var/mnt/eclipse/repos/krl` (sibling top-level repo), NOT -here. This is intentional: KRL has graduated past the scaffold stage and -earned its own repo. These scaffolds represent future candidates that -may graduate similarly. +**KRL is not a Tangle dialect and never was.** It was previously listed here as +one that had "graduated" to its own repository; that was part of a wider +conflation of the two projects, corrected in `README.adoc` and in the erratum to +`AFFIRMATION.adoc`. + +KRL is the resolution language for +[QuandleDB](https://github.com/hyperpolymath/quandledb), developed jointly with +it, and lives at [hyperpolymath/krl](https://github.com/hyperpolymath/krl). It +does not compile to, lower into, or otherwise depend on Tangle. The two share a +subject matter, not an architecture. + +The scaffolds listed above are Tangle's own dialects. ## Contribution From 2369299d62eff2d32118d3c049e706e1799abd50 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 16:10:36 +0100 Subject: [PATCH 2/3] fix(governance): SPDX header + SHA pins in pages.yml, refresh stale standards pins MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both Governance failures on this branch are the same two faults found and fixed in krl (#56), so the same remedy applies here. Workflow security linter * pages.yml carried no SPDX header. Every other workflow in the repo has one; this was the only omission. Added. * pages.yml used floating tags where every other workflow pins by SHA: actions/checkout@v7 -> 3d3c42e5... # v7 actions/upload-pages-artifact@v5 -> fc324d35... # v5 actions/deploy-pages@v5 -> cd2ce8fc... # v5 Kept on the same major versions, so this changes pinning only, not behaviour. Check Workflow Staleness * governance-reusable.yml, hypatia-scan-reusable.yml and scorecard-reusable.yml were pinned at d7c22711e830 — 63 commits / 24 days behind standards HEAD, outside the gate's recency window. Refreshed to f9dca6ded2cad8ab54044c1cb0489b558ae2682b (full 40-char SHA). Not touched: mirror-reusable.yml (d135b05) and secret-scanner-reusable.yml (c65436e). Neither was flagged, and the secret-scanner pin should not move independently of the gitleaks allowlist work. Verified: all workflows carry an SPDX header; no unpinned third-party actions remain; actionlint 0 errors. --- .github/workflows/governance.yml | 2 +- .github/workflows/hypatia-scan.yml | 2 +- .github/workflows/pages.yml | 10 ++++++---- .github/workflows/scorecard.yml | 2 +- 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 13327b9..3f783fa 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -13,4 +13,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b \ No newline at end of file diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 02b0e9c..637e90d 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -16,4 +16,4 @@ permissions: jobs: scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b \ No newline at end of file diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index f95bced..b3d9333 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -1,3 +1,5 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) name: GitHub Pages (Ddraig SSG) on: push: @@ -18,9 +20,9 @@ jobs: image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - name: Checkout Site - uses: actions/checkout@v7 + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 - name: Checkout Ddraig SSG - uses: actions/checkout@v7 + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 with: repository: hyperpolymath/ddraig-ssg path: .ddraig-ssg @@ -37,7 +39,7 @@ jobs: fi ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} - name: Upload artifact - uses: actions/upload-pages-artifact@v5 + uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5 with: path: '_site' deploy: @@ -50,4 +52,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v5 + uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5 diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 4ecc2ad..db25ae8 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -13,7 +13,7 @@ permissions: jobs: scorecard: - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e + uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b permissions: contents: read security-events: write From d090ff2a300f030d155e31221b11e56c813d3ffc Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 16:13:23 +0100 Subject: [PATCH 3/3] fix(ci): grant security-events: write to the Hypatia caller MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Refreshing hypatia-scan-reusable.yml to standards HEAD turned the run into a startup_failure — zero jobs, no log. The newer reusable declares permissions: contents: read security-events: write because it uploads SARIF, while the caller granted security-events: read. A called workflow cannot escalate beyond its caller's grant, so GitHub rejects the whole run at parse time rather than failing a job. This is the failure mode where refreshing a pin BREAKS a caller that was previously fine: the old pin needed only read. Checked the other two bumped reusables the same way — governance-reusable and scorecard-reusable both declare only contents: read, which the callers already grant, so no change was needed there. --- .github/workflows/hypatia-scan.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 637e90d..42fed59 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -12,7 +12,10 @@ on: permissions: contents: read - security-events: read + # The reusable declares security-events: write (it uploads SARIF). A called + # workflow cannot escalate beyond the caller's grant, so `read` here makes the + # whole run a startup_failure with zero jobs and no log. + security-events: write jobs: scan: