From 84e1cf9d57c0029617d541768c782d17d20f5997 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 01:17:06 +0100 Subject: [PATCH 1/2] fix(rsr): finish template instantiation + enforce it (#56) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes both acceptance criteria of #56, though the second turned out to be already satisfied and the first was mis-scoped. ## Criterion 1 — template residue The issue recorded "5 {{PLACEHOLDER}} files + 8 rsr-template-repo references". Re-measured: 8 files matched `{{...}}` and 21 lines matched the template name — but most were META-REFERENCES, files describing the debt rather than carrying it. Three would have been damaged by a naive search-and-replace: * src/rust/src/eval.rs — `"...add{{}} block"` is a Rust format! ESCAPE (`{{}}` renders as literal `{}`) naming the `add{}` language construct. It is working code. * methodology.a2ml — the token appears inside reject-if-contains, the rule that FORBIDS it. * AFFIRMATION.adoc, docs/identity-fabric/ — prose recording the debt. The genuine residue, now cleared: * QUICKSTART-MAINTAINER: {{DEPS}}, {{BUILD_OUTPUT_PATH}}, {{PACKAGE_NAME}} * QUICKSTART-DEV: {{LANG_STACK}}, {{BUILD_CMD}}, {{TEST_CMD}}, {{MUST_INVARIANTS}} * methodology.a2ml: {{PROJECT_UNIQUE_STRENGTH}} * Intentfile / Trustfile / Mustfile / Adjustfile — whose SUBJECT was still the template. Intentfile asserted "This repository is the canonical template for Rhodium Standard Repository compliance." * docs/CITATIONS.adoc — every format credited "Polymath, Hyper" for "RSR-template-repo", wrong project and wrong author. ## A worse class, found while fixing it All three QUICKSTARTs documented commands that DO NOT EXIST: `just build`, `just test`, `just lint`, `just panic-scan`, `just setup-dev`, `just build-release`, `just install`, `just run`, `just heal`, `just setup`, `just uninstall`, `just stapeln-run` — and asserted an `$XDG_CONFIG_HOME/tangle/config.toml` the compiler never reads, plus a "Multi-Instance Deployment" section for what is a single stateless binary. Documentation that fails when followed is worse than none. Every command now shown is verified to exist, and the one worked example's output is the REAL output (8 `assertion passed` lines, exit 0) rather than the template's invented "Tangle started successfully." ## Criterion 2 — already satisfied The stack-diagram reconciliation was done by #78: README.adoc carries the correction and AFFIRMATION.adoc has "Erratum — 2026-07-21 / Correction 1 — the stack does not exist". Note the criterion as worded ("does the simplified diagram supersede, or re-state, the nuance?") presupposed the stack was real; both options were wrong, because `KRL -> TangleIR -> ...` describes a dependency that never existed. Withdrawn, not reconciled. ## Making the rule real methodology.a2ml has always declared `reject-if-contains = [..., "rsr-template-repo"]` and NOTHING enforced it, which is how the contractiles stayed mis-instantiated. Adds scripts/check-rsr-instantiation.sh (+ `just rsr-check`, + a CI step) which enforces it, using an explicit allowlist so legitimate meta-references and the Rust escape are not false-positived. Verified adversarially: reintroducing a placeholder, claiming to be the template, and documenting a phantom recipe are each caught; the Rust format! escape is correctly ignored. The guard found a file I had not inspected (QUICKSTART-USER.adoc, six phantom recipes) on its first run. AFFIRMATION.adoc gains a dated Erratum — 2026-07-29 (Corrections 3-5) recording the residue clearance, that the OCaml compiler is no longer unbuilt (#87/#89), and that `==` is no longer list equality (#50/#87). Co-Authored-By: Claude Opus 5 --- .github/workflows/ocaml-ci.yml | 20 +++ .../bot_directives/methodology.a2ml | 16 ++- .../contractiles/Adjustfile.a2ml | 4 +- .../contractiles/Intentfile.a2ml | 40 +++--- .machine_readable/contractiles/Mustfile.a2ml | 4 +- .machine_readable/contractiles/Trustfile.a2ml | 6 +- AFFIRMATION.adoc | 71 +++++++++++ Justfile | 4 + QUICKSTART-DEV.adoc | 118 ++++++++++++++---- QUICKSTART-MAINTAINER.adoc | 99 +++++++++------ QUICKSTART-USER.adoc | 57 ++++++--- docs/CITATIONS.adoc | 24 ++-- scripts/check-rsr-instantiation.sh | 110 ++++++++++++++++ 13 files changed, 459 insertions(+), 114 deletions(-) create mode 100755 scripts/check-rsr-instantiation.sh diff --git a/.github/workflows/ocaml-ci.yml b/.github/workflows/ocaml-ci.yml index c90234b..b137426 100644 --- a/.github/workflows/ocaml-ci.yml +++ b/.github/workflows/ocaml-ci.yml @@ -32,6 +32,10 @@ on: - 'examples/**' - 'conformance/**' - 'scripts/check-corpus.sh' + - 'scripts/check-rsr-instantiation.sh' + - 'QUICKSTART-*.adoc' + - 'Justfile' + - '.machine_readable/**' - '.github/workflows/ocaml-ci.yml' pull_request: paths: @@ -39,6 +43,10 @@ on: - 'examples/**' - 'conformance/**' - 'scripts/check-corpus.sh' + - 'scripts/check-rsr-instantiation.sh' + - 'QUICKSTART-*.adoc' + - 'Justfile' + - '.machine_readable/**' - '.github/workflows/ocaml-ci.yml' workflow_dispatch: {} @@ -108,6 +116,18 @@ jobs: # sat failing its own assertions until TG-7 (#87) fixed `~`. bash scripts/check-corpus.sh + - name: RSR instantiation guard + run: | + set -euo pipefail + # methodology.a2ml has always declared a reject-if-contains rule for + # template residue, and nothing enforced it — so four contractiles + # named the upstream template as their SUBJECT indefinitely. This + # makes the repo's own rule real. It also checks the docs only name + # `just` recipes that exist: the QUICKSTARTs documented nine that + # never did. (Deliberately worded without the literal tokens, so the + # guard need not allowlist its own caller.) + bash scripts/check-rsr-instantiation.sh + - name: TG-7 semantics guard working-directory: compiler run: | diff --git a/.machine_readable/bot_directives/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml index 754f357..5995328 100644 --- a/.machine_readable/bot_directives/methodology.a2ml +++ b/.machine_readable/bot_directives/methodology.a2ml @@ -52,10 +52,20 @@ perfective = 10 # % for SPDX headers, doc updates, formatting, style # UNIQUE STRENGTH (when mode = divergent) # ============================================================================ # What makes this project special. Agents should DEEPEN this, not broaden it. -# Customise this per project — the template default is generic. - [methodology.unique-strength] -description = "{{PROJECT_UNIQUE_STRENGTH}}" +description = """ +Tangle's distinctive asset is that its central claim is MECHANISED rather +than asserted. Progress, Preservation, Determinism and Type Safety are +proven in Lean 4 over the same core the OCaml compiler implements, and the +two are tied together by translation validation (TG-3: 496 kernel-checked +obligations asserting OCaml infer_expr refines the Lean spec). + +Since TG-7 (#50) the language's `==` decides braid-GROUP equivalence, so +"equivalence is isotopy" is executable rather than aspirational. + +Deepen this, do not broaden it: the value is the proof-to-implementation +tie, and every claim carries an explicit trusted base (ASSUMPTIONS.md). +""" deepen-not-broaden = true # ============================================================================ diff --git a/.machine_readable/contractiles/Adjustfile.a2ml b/.machine_readable/contractiles/Adjustfile.a2ml index 6f01e89..84e56b7 100644 --- a/.machine_readable/contractiles/Adjustfile.a2ml +++ b/.machine_readable/contractiles/Adjustfile.a2ml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# Adjustfile — Drift-tolerance contract for rsr-template-repo +# Adjustfile — Drift-tolerance contract for tangle # Author: Jonathan D.A. Jewell # # Cumulative-drift catchment: tolerance bands + corrective actions. @@ -8,7 +8,7 @@ # Fix with: adjust fix (applies deterministic patches; advisory otherwise) @abstract: -Drift tolerances and corrective actions for rsr-template-repo. Unlike +Drift tolerances and corrective actions for tangle. Unlike MUST (hard gate), ADJUST tracks cumulative drift against tolerance bands and proposes corrective actions. Advisory — it warns and trends, it does not block. diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/.machine_readable/contractiles/Intentfile.a2ml index ef74f45..5476ec4 100644 --- a/.machine_readable/contractiles/Intentfile.a2ml +++ b/.machine_readable/contractiles/Intentfile.a2ml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# Intentfile (A2ML Canonical) — north-star contractile for rsr-template-repo +# Intentfile (A2ML Canonical) — north-star contractile for tangle # Author: Jonathan D.A. Jewell # # Paired runner: intend.ncl @@ -20,28 +20,40 @@ # contractile for hard gates. @abstract: -North-star contractile for rsr-template-repo. This repository is the -canonical template for Rhodium Standard Repository compliance. It provides -the scaffold that all hyperpolymath repos should copy and customize. +North-star contractile for tangle — a research language in which programs +are structured as tangles (braids) and program equivalence is isotopy, not +syntactic equality. Ships an OCaml compiler, mechanised Lean 4 metatheory +(Progress / Preservation / Determinism / Type Safety), a Rust LSP and WASM +backend, and a conformance corpus. @end ## Purpose -The rsr-template-repo serves as the master template for all hyperpolymath -repositories. It contains the complete set of contractile files, machine-readable -specifications, and governance documentation that define the Rhodium Standard. +tangle exists to make one claim precise and then hold itself to it: +computation is the construction of structured objects, and meaning is +preserved under valid transformation. Concretely that means equivalence is +decided by braid-group equality (TG-7, #50) rather than by comparing +representations, and that the core metatheory is machine-checked rather than +asserted. -Every new repository in the hyperpolymath estate should be initialized by -copying this template and substituting the placeholder values with -repo-specific content. +The proof ladder (TG-0..TG-10, see PROOF-NEEDS.md) is the spine: each rung is +either LANDED with a named artefact in proofs/Tangle.lean, or explicitly +recorded as research-grade. Claims that are trusted rather than proven are +registered in ASSUMPTIONS.md — currently A-TG-7.2, the correctness of the +Dehornoy decision procedure that `==` now depends on. ## Anti-Purpose This repository is NOT: -- A general-purpose project scaffold for external use (hyperpolymath-only) -- A replacement for per-repo customization (all files must be bespoke) -- A static template that never changes (evolves with RSR spec) -- A runtime library or framework (build-time only) +- A backend for KRL. KRL is QuandleDB's resolution language; it neither + compiles to nor depends on tangle, and the `TangleIR` layer that was + supposed to connect them exists in no source file in either repo. See the + erratum in AFFIRMATION.adoc and the de-conflation in #78. +- A knot database. That is QuandleDB. +- A production language. It is a research vehicle; the readiness grade is + tracked honestly in READINESS.md. +- A proof of its own decision procedures. The metatheory is proven RELATIVE + to `braidEquiv`; see ASSUMPTIONS.md A-TG-7.2. ## If In Doubt diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml index 55f8ab4..8ab8dd0 100644 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# Mustfile — Physical state contract for rsr-template-repo +# Mustfile — Physical state contract for tangle # Author: Jonathan D.A. Jewell # # What MUST be true about this repository. Hard requirements. @@ -7,7 +7,7 @@ # Fix with: must fix (where a deterministic fix exists) @abstract: -Physical-state invariants for rsr-template-repo. This is the canonical +Physical-state invariants for tangle. This is the canonical RSR template repository. These are hard requirements — CI and pre-commit hooks fail if any check fails. @end diff --git a/.machine_readable/contractiles/Trustfile.a2ml b/.machine_readable/contractiles/Trustfile.a2ml index e2028b5..66983b0 100644 --- a/.machine_readable/contractiles/Trustfile.a2ml +++ b/.machine_readable/contractiles/Trustfile.a2ml @@ -1,12 +1,12 @@ # SPDX-License-Identifier: MPL-2.0 -# Trustfile — Trust boundaries and integrity invariants for rsr-template-repo +# Trustfile — Trust boundaries and integrity invariants for tangle # Author: Jonathan D.A. Jewell # # Defines what LLM/SLM agents are trusted to do without asking, and # integrity invariants that verify the repo has not been tampered with. @abstract: -Trust boundaries and integrity checks for rsr-template-repo. This file +Trust boundaries and integrity checks for tangle. This file combines the trust-level definitions from the original TRUST.contractile with the integrity invariants from the old Trustfile.a2ml. It defines what AI agents may do autonomously and what requires human approval, @@ -15,7 +15,7 @@ plus checks that verify repository integrity. ## Trust Levels -The rsr-template-repo operates at trust level: maximal +tangle operates at trust level: maximal Trust levels: - maximal: Agent may read, build, test, lint, format, heal freely. diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 8b4dec1..100e624 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -284,3 +284,74 @@ 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. + +== Erratum — 2026-07-29 + +A second dated correction, appended under the same convention: the text above +is left intact, because an affirmation is a claim about a past state and +amending it in place would falsify a record. + +=== Correction 3 — the template residue is cleared + +The affirmation records as honest debt: + +[quote] +5 `{{PLACEHOLDER}}` files + 8 `rsr-template-repo` references + +Both counts were low, and the classification conflated two different things. +Re-measured 2026-07-29: *8* files matched `{{...}}` and *21* lines matched +`rsr-template-repo` — but most were *meta-references*, i.e. files describing +the debt rather than carrying it. Three are worth naming, because a naive +search-and-replace would have damaged them: + +* `src/rust/src/eval.rs` — `"...add{{}} block"` is a Rust `format!` *escape* + (`{{}}` renders as a literal `{}`) describing the `add{}` language + construct. It is code, not a placeholder. +* `.machine_readable/bot_directives/methodology.a2ml` — the string appears + inside `reject-if-contains`, which exists precisely to *forbid* it. +* `AFFIRMATION.adoc` (this file) and `docs/identity-fabric/` — prose recording + the debt. + +The *genuine* residue was: `{{DEPS}}`, `{{BUILD_OUTPUT_PATH}}`, +`{{PACKAGE_NAME}}` in `QUICKSTART-MAINTAINER.adoc`; `{{LANG_STACK}}`, +`{{BUILD_CMD}}`, `{{TEST_CMD}}`, `{{MUST_INVARIANTS}}` in +`QUICKSTART-DEV.adoc`; `{{PROJECT_UNIQUE_STRENGTH}}` in `methodology.a2ml`; +and four contractiles (`Intentfile`, `Trustfile`, `Mustfile`, `Adjustfile`) +plus `docs/CITATIONS.adoc` whose *subject was still rsr-template-repo* — +`Intentfile` asserted "This repository is the canonical template for Rhodium +Standard Repository compliance", and the citation guide credited +"Polymath, Hyper" for "RSR-template-repo". All are now instantiated for +tangle. + +A worse class surfaced while fixing it: both QUICKSTARTs documented *commands +that do not exist* — `just build`, `just test`, `just lint`, `just panic-scan`, +`just setup-dev`, `just build-release`, `just install`, `just run`, +`just stapeln-export` — and asserted an `$XDG_CONFIG_HOME/tangle/config.toml` +that the compiler never reads. Documentation that fails when followed is worse +than none, so the recipe lists are now checked against `just --list` by +`scripts/check-rsr-instantiation.sh`. + +=== Correction 4 — the OCaml compiler is no longer unbuilt + +The closing line of the 2026-07-21 erratum reads: + +[quote] +The OCaml compiler remains unbuilt — no workflow in this repository builds it. + +That was true when written and is no longer. `.github/workflows/ocaml-ci.yml` +(added 2026-07-29, PR #87) builds the compiler and runs the full suite — over +4,000 assertions — on every relevant push and PR, and PR #89 added a gate over +the runnable corpus (`examples/` + `conformance/`). + +That gate immediately earned itself: `examples/isotopy.tangle`, the program +whose purpose is to demonstrate the language's central claim, was *failing its +own assertions* and had been for as long as `~` used free reduction. It passes +only since TG-7 (#50/#87) made `~` decide real braid-group equivalence. + +=== Correction 5 — `==` is no longer list equality + +Anywhere the affirmation or its sources describe braid `==` as list equality: +that ceased to be true on 2026-07-29. Owner ruling #50 chose braid-*group* +equivalence, implemented in PR #87 across both engines. The metatheory is +proven *relative to* the decision procedure; its correctness is registered as +assumption *A-TG-7.2* and is not claimed as proven. diff --git a/Justfile b/Justfile index f4a648b..64693f5 100644 --- a/Justfile +++ b/Justfile @@ -84,3 +84,7 @@ corpus: check-all: @cd compiler && dune build && dune test --force @bash scripts/check-corpus.sh + +# Verify this repo is instantiated, not a copy of the RSR template +rsr-check: + @bash scripts/check-rsr-instantiation.sh diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc index ed9a2c1..066a5a8 100644 --- a/QUICKSTART-DEV.adoc +++ b/QUICKSTART-DEV.adoc @@ -1,14 +1,23 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -// Template: QUICKSTART-DEV.adoc — clone → build → test → PR -// Replace tangle, {{BUILD_CMD}}, {{TEST_CMD}}, {{LANG_STACK}} with actuals +// QUICKSTART-DEV.adoc — clone → build → test → PR (instantiated for tangle, #56) = tangle — Quick Start for Developers :toc: :toclevels: 2 == Tech Stack -{{LANG_STACK}} +* *OCaml* (27 files) — the compiler: lexer (`ocamllex`), parser (`menhir`), + typechecker, tree-walking interpreter, and the TG-3/5/7/8 checkers. + Built with *dune*. +* *Lean 4* (pinned `leanprover/lean4:v4.14.0`) — the mechanised proofs in + `proofs/Tangle.lean`: Progress, Preservation, Determinism, Type Safety, plus + the TG-2 decidability results and the TG-7 braid-group equivalence port. +* *Rust* (18 files) — `compiler/tangle-lsp` (language server) and + `compiler/tangle-wasm` (WASM backend + differential tests). +* *Zig* (3 files) — `ffi/` bridge. + +Guix is the primary environment (`guix.scm`). == Set Up Development Environment @@ -32,21 +41,46 @@ nix develop ---- git clone https://github.com/hyperpolymath/tangle.git cd tangle -just setup-dev + +# OCaml toolchain (Debian/Ubuntu). `just setup-dev` never existed. +sudo apt-get install -y ocaml ocaml-dune menhir +cd compiler && dune build + +# Lean toolchain, pinned — only needed if you touch proofs/ +bash proofs/bootstrap-lean.sh ---- == Build [source,bash] ---- -{{BUILD_CMD}} +cd compiler && dune build # the OCaml compiler -> _build/default/bin/main.exe +---- + +The Lean proofs are checked separately (they need the pinned toolchain): + +[source,bash] +---- +bash proofs/bootstrap-lean.sh # installs the pinned Lean, or reuses it +cd proofs && lean Tangle.lean # must report 0 errors ---- == Test [source,bash] ---- -{{TEST_CMD}} +just check-all # build + full suite (4,000+ assertions) + corpus gate +---- + +Or the pieces individually: + +[source,bash] +---- +cd compiler && dune test --force # TG-3 1008, TG-5 189, TG-7 2220, TG-8 2311, + # plus parser/typecheck/eval/e2e/property suites +just corpus # run the language's OWN programs + # (examples/ + conformance/) — see #89 +bash proofs/check-tg3-differential.sh # 496 kernel-checked TG-3 obligations ---- == Project Structure @@ -54,15 +88,22 @@ just setup-dev [source] ---- tangle/ -├── src/ # Source code -├── src/abi/ # Idris2 ABI definitions (if applicable) -├── ffi/zig/ # Zig FFI bridge (if applicable) -├── tests/ # Test suite -├── docs/ # Documentation -├── .machine_readable/ # Checkpoint files (STATE, META, ECOSYSTEM) -├── Justfile # Task runner recipes -├── guix.scm # Guix environment -├── flake.nix # Nix environment (fallback) +├── compiler/ # THE compiler (OCaml, dune) +│ ├── lib/ # lexer, parser, typecheck, eval, braid_equiv, dialects +│ ├── bin/main.ml # CLI: | --eval | --check | --compile-pd | --repl +│ ├── test/ # suites incl. tg3/ tg5/ tg7/ tg8/ +│ ├── tangle-lsp/ # language server (Rust) +│ └── tangle-wasm/ # WASM backend + differential tests (Rust) +├── proofs/ # Lean 4 — Tangle.lean, TG3Differential.lean +├── examples/ # runnable .tangle programs (gated, see #89) +├── conformance/ # valid/ + invalid/ corpus + runner +├── dialects/ # per-dialect specs (TG-8) +├── spec/ # language specification +├── ffi/ # Zig FFI bridge +├── scripts/ # check-corpus.sh, check-rsr-instantiation.sh +├── .machine_readable/ # A2ML checkpoints + contractiles +├── Justfile # task runner (authoritative recipe list) +├── guix.scm # Guix environment (primary) └── 0-AI-MANIFEST.a2ml # AI agent entry point ---- @@ -70,29 +111,56 @@ tangle/ [source,bash] ---- -just build # Build the project -just test # Run tests -just doctor # Self-diagnostic -just lint # Lint and format -just panic-scan # Security scan via panic-attacker -just tour # Guided tour of the codebase +just check-all # build + full test suite + corpus gate (the one to use) +just corpus # run examples/ + conformance/ against the built compiler +just doctor # self-diagnostic +just tour # guided tour of the codebase +just must-check # all MUST invariants +just trust-verify # all TRUST invariants +just crg-grade # current readiness grade +just llm-context # dump context for an LLM agent ---- +NOTE: `just --list` is authoritative. This list is checked by +`scripts/check-rsr-instantiation.sh`, so a recipe named here that does not +exist fails CI — the previous version of this file advertised `just build`, +`just test`, `just lint` and `just panic-scan`, none of which were ever +recipes. + == Before Submitting a PR [source,bash] ---- -just lint # Format and lint -just test # All tests pass -just panic-scan # No new security issues +just check-all # build + all suites + corpus gate must be green +just must-check # MUST invariants +just trust-verify # TRUST invariants ---- +If you touched `proofs/`, also run `cd proofs && lean Tangle.lean` (0 errors) +and `bash proofs/check-tg3-differential.sh`. + == Contractile Invariants Read `.machine_readable/MUST.contractile` before making changes. Key invariants that must never be violated: -{{MUST_INVARIANTS}} +Run `just must-check` to verify all of them: + +* `must-license-present` — a `LICENSE` file exists. +* `must-readme-present` — a `README` exists. +* `must-spdx-headers` — source files carry SPDX licence headers. +* `must-no-banned-files` — no `Dockerfile`s or `Makefile`s (estate policy: + Containerfile + Justfile). + +Beyond the Mustfile, two invariants are enforced by CI and matter most here: + +* *The proofs must stay clean.* `proofs/Tangle.lean` must report *0 errors* and + contain no `sorry` / `axiom` / `admit` outside comments. Note this proves the + metatheory *relative to* `braidEquiv` — see `PROOF-NARRATIVE.md` §TG-7 and + assumption A-TG-7.2 for what is trusted rather than proven. +* *The corpus must keep running.* `examples/` and `conformance/` are gated by + `scripts/check-corpus.sh` as a ratchet: nothing working may break, and + anything that starts working must be promoted out of the known-bad list. == LLM/AI Agent Development diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc index 3649869..ef07ff5 100644 --- a/QUICKSTART-MAINTAINER.adoc +++ b/QUICKSTART-MAINTAINER.adoc @@ -1,7 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // Template: QUICKSTART-MAINTAINER.adoc — packaging, deploying, and maintaining -// Replace tangle, {{PACKAGE_NAME}}, {{DEPS}} with actuals = tangle — Quick Start for Platform Maintainers :toc: :toclevels: 2 @@ -13,18 +12,50 @@ distribution on your platform. == Runtime Dependencies -{{DEPS}} +The built compiler is a single self-contained OCaml native executable; at +*runtime* it needs nothing beyond libc. + +*Build-time* dependencies: OCaml (>= 4.14; 5.3 tested), dune (>= 3.x), and +menhir (parser generator for `compiler/lib/parser.mly`). + +On Debian/Ubuntu: + +[source,bash] +---- +apt-get install -y ocaml ocaml-dune menhir +---- + +Optional, per component: *Lean 4* pinned `leanprover/lean4:v4.14.0` for +re-checking `proofs/` (NOT required to build or run the compiler); a *Rust* +toolchain for `compiler/tangle-lsp` and `compiler/tangle-wasm`; *Zig* for the +`ffi/` bridge. == Build from Source [source,bash] ---- git clone https://github.com/hyperpolymath/tangle.git -cd tangle -just build-release +cd tangle/compiler +dune build --profile release ---- -Output: `{{BUILD_OUTPUT_PATH}}` +Output: `compiler/_build/default/bin/main.exe` + +NOTE: there is no `just build-release` recipe — `just --list` is +authoritative. The binary is named `main.exe` (see `compiler/bin/dune`); the +conformance runner assumed a `tangle` binary for a long time and silently +failed because of it. + +The CLI: + +[source,bash] +---- +main.exe # parse + pretty-print +main.exe --eval # evaluate +main.exe --check # parse + type diagnostics (LSP backend) +main.exe --compile-pd # compile compositional defs to PD/Skein payloads +main.exe --repl # interactive REPL +---- == Packaging @@ -46,7 +77,8 @@ nix build [source,bash] ---- -just stapeln-export # Generates Containerfile +# NOTE: `just stapeln-export` does not exist. Write the Containerfile by +# hand, or add the recipe first. `just --list` is authoritative. podman build -t tangle . ---- @@ -54,7 +86,8 @@ podman build -t tangle . [source,bash] ---- -just install --prefix=/usr/local +# No `just install` recipe — install by copying the built binary: +install -Dm755 compiler/_build/default/bin/main.exe /usr/local/bin/tanglec ---- Files installed: @@ -63,35 +96,32 @@ Files installed: |=== | Path | Contents -| `$PREFIX/bin/` -| Executables - -| `$PREFIX/share/{{PACKAGE_NAME}}/` -| Data files, assets - -| `$PREFIX/share/doc/{{PACKAGE_NAME}}/` -| Documentation +| `$PREFIX/bin/tanglec` +| The compiler binary — this is the whole install -| `$PREFIX/share/applications/` -| .desktop file (Linux, if GUI) - -| `$PREFIX/share/man/man1/` -| Man pages +| `$PREFIX/share/doc/tangle/` +| Documentation, if you choose to ship it |=== == Configuration -Default config location: `$XDG_CONFIG_HOME/{{PACKAGE_NAME}}/config.toml` +None. `tanglec` reads no configuration file — verified: nothing under +`compiler/lib/` or `compiler/bin/` references `config.toml` or +`XDG_CONFIG_HOME`. Behaviour is determined entirely by the CLI flag and the +input file. -Fallback: `$HOME/.config/{{PACKAGE_NAME}}/config.toml` +(The template asserted an `$XDG_CONFIG_HOME/tangle/config.toml`. It does not +exist and never has.) == Health Checks [source,bash] ---- -just doctor # Full diagnostic -just run --version # Version check -just run --selftest # Built-in self-test +just doctor # full diagnostic +just check-all # build + all suites + corpus gate +tanglec --repl # smoke-test the installed binary +# NOTE: there is no `just run`, no `--version`, no `--selftest`. The CLI +# accepts: | --eval | --check | --compile-pd | --repl. ---- == Updating @@ -99,11 +129,11 @@ just run --selftest # Built-in self-test [source,bash] ---- git pull -just build-release -just install --prefix=/usr/local +cd compiler && dune build --profile release +install -Dm755 _build/default/bin/main.exe /usr/local/bin/tanglec ---- -Or via OPSM: `opsm update {{PACKAGE_NAME}}` +Or via OPSM: `opsm update tangle` == Security Notes @@ -114,15 +144,12 @@ Or via OPSM: `opsm update {{PACKAGE_NAME}}` == Multi-Instance Deployment -For deploying multiple instances (e.g., different users or tenants): - -[source,bash] ----- -just install --prefix=/opt/{{PACKAGE_NAME}}-instance1 --config=/etc/{{PACKAGE_NAME}}/instance1.toml -just install --prefix=/opt/{{PACKAGE_NAME}}-instance2 --config=/etc/{{PACKAGE_NAME}}/instance2.toml ----- +Not applicable. `tanglec` is a compiler: a single stateless binary invoked per +file. There is no daemon, no per-instance state, and nothing to isolate — +install as many copies at different prefixes as you like, and they cannot +interfere. -Each instance has isolated config, data, and logs. +(The template this file came from assumed a long-running service.) == Reporting Issues diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc index b1005e2..c91e985 100644 --- a/QUICKSTART-USER.adoc +++ b/QUICKSTART-USER.adoc @@ -1,7 +1,7 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // Template: QUICKSTART-USER.adoc — 5-minute path to working software -// Replace tangle, Tangle — See README.adoc for details., just run, Tangle started successfully. with actuals +// QUICKSTART-USER.adoc — instantiated for tangle (#56) = tangle — Quick Start for Users :toc: :toclevels: 2 @@ -40,45 +40,63 @@ Before you begin, ensure you have: # Clone and set up git clone https://github.com/hyperpolymath/tangle.git cd tangle -just setup ----- -The setup script will: +# Build the compiler (`just setup` never existed) +sudo apt-get install -y ocaml ocaml-dune menhir +cd compiler && dune build +---- -* Detect your platform and shell -* Install missing dependencies (with your permission) -* Configure the application -* Offer install location choices -* Run a self-diagnostic to verify everything works +There is no setup script — the build IS the setup. `dune build` produces a +single self-contained native executable at +`compiler/_build/default/bin/main.exe`, which needs nothing at runtime beyond +libc. There is no configuration step and no install location to choose. === Option 2: Container (via Stapeln) [source,bash] ---- -just stapeln-run +# `just stapeln-run` does not exist. Run the built binary: +./compiler/_build/default/bin/main.exe --repl ---- === Option 3: Portable (no system changes) [source,bash] ---- -just install --portable --prefix=./tangle-portable +# No `just install` recipe — the build IS the artefact: +cp ./compiler/_build/default/bin/main.exe ./tanglec ---- == First Run [source,bash] ---- -just run +# `just run` does not exist. Invoke the compiler on a file: +./compiler/_build/default/bin/main.exe --eval examples/isotopy.tangle ---- -Expected output: +Expected output — one line per assertion, exit 0 (verified, not assumed): -[source] +[source,bash] ---- -Tangle started successfully. +$ ./compiler/_build/default/bin/main.exe --eval examples/isotopy.tangle +assertion passed +assertion passed +assertion passed +assertion passed +assertion passed +assertion passed +assertion passed +assertion passed +$ echo $? +0 ---- +That file is worth reading: it asserts Reidemeister II cancellation and far +commutation, and it only passes because `~` decides braid-group equivalence +(TG-7, #50). Before that change it failed with `Runtime error: Assertion +failed`. + == Self-Diagnostic If something isn't working: @@ -95,12 +113,14 @@ To attempt automatic repair: [source,bash] ---- -just heal +# `just heal` does not exist. The real self-checks are: +just doctor # diagnostic +just check-all # build + full suite + corpus gate ---- == Get Help -* **In-app**: `just run --help` +* **CLI**: `./compiler/_build/default/bin/main.exe --repl` then explore; see README.adoc * **Guided tour**: `just tour` * **Report a problem**: `just help-me` (pre-fills diagnostic context) * **Wiki**: https://github.com/hyperpolymath/tangle/wiki @@ -109,7 +129,8 @@ just heal [source,bash] ---- -just uninstall +# Nothing is installed system-wide: delete the clone and any copy you made. +rm -f ./tanglec ---- You will be asked: diff --git a/docs/CITATIONS.adoc b/docs/CITATIONS.adoc index 8cb2e4e..82e26df 100644 --- a/docs/CITATIONS.adoc +++ b/docs/CITATIONS.adoc @@ -1,36 +1,38 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -= RSR-template-repo - Citation Guide += Tangle — Citation Guide :toc: == BibTeX [source,bibtex] ---- -@software{rsr-template-repo_2025, - author = {Polymath, Hyper}, - title = {RSR-template-repo}, - year = {2025}, - url = {https://github.com/hyperpolymath/RSR-template-repo}, - license = {MPL-2.0} +@software{tangle_2026, + author = {Jewell, Jonathan D. A.}, + title = {Tangle: a topological programming language}, + year = {2026}, + url = {https://github.com/hyperpolymath/tangle}, + license = {MPL-2.0}, + note = {Programs are structured as braids; equivalence is isotopy. + Core metatheory mechanised in Lean 4.} } ---- == Harvard Style -Polymath, H. (2025) _RSR-template-repo_ [Computer software]. Available at: https://github.com/hyperpolymath/RSR-template-repo +Jewell, J.D.A. (2026) _Tangle: a topological programming language_ [Computer software]. Available at: https://github.com/hyperpolymath/tangle == OSCOLA -Hyper Polymath, 'RSR-template-repo' (2025) +Jonathan D A Jewell, 'Tangle: a topological programming language' (2026) == MLA -Polymath, Hyper. "RSR-template-repo." 2025, github.com/hyperpolymath/RSR-template-repo. +Jewell, Jonathan D. A. "Tangle: a topological programming language." 2026, github.com/hyperpolymath/tangle. == APA 7 -Polymath, H. (2025). _RSR-template-repo_ [Computer software]. GitHub. https://github.com/hyperpolymath/RSR-template-repo +Jewell, J. D. A. (2026). _Tangle: a topological programming language_ [Computer software]. GitHub. https://github.com/hyperpolymath/tangle == See Also diff --git a/scripts/check-rsr-instantiation.sh b/scripts/check-rsr-instantiation.sh new file mode 100755 index 0000000..0c687fd --- /dev/null +++ b/scripts/check-rsr-instantiation.sh @@ -0,0 +1,110 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# check-rsr-instantiation.sh — enforce that this repo is INSTANTIATED, not a +# copy of the RSR template wearing tangle's name. +# +# ── Why this exists ──────────────────────────────────────────────────────── +# `.machine_readable/bot_directives/methodology.a2ml` already declares: +# +# reject-if-contains = ["{{PLACEHOLDER}}", "{{PROJECT}}", "rsr-template-repo"] +# +# ...and NOTHING enforced it, so the repository violated its own stated rule +# indefinitely: four contractiles still named `rsr-template-repo` as their +# SUBJECT (`Intentfile` asserted "This repository is the canonical template for +# Rhodium Standard Repository compliance"), and the citation guide credited +# "Polymath, Hyper" for "RSR-template-repo". Fixed under #56; this makes the +# rule real so it cannot come back. +# +# ── Two checks, because two different things went wrong ──────────────────── +# 1. TEMPLATE RESIDUE — unfilled `{{...}}` placeholders and files whose subject +# is still the template. +# 2. PHANTOM COMMANDS — the QUICKSTARTs documented `just build`, `just test`, +# `just lint`, `just panic-scan`, `just setup-dev`, `just build-release`, +# `just install`, `just run`, `just stapeln-export`. None were recipes. +# Documentation that fails when followed is worse than none, so every +# `just ` named in the docs is checked against `just --list`. +# +# ── Why an ALLOWLIST rather than a bare grep ─────────────────────────────── +# A naive search-and-replace would have corrupted working code. In particular +# `src/rust/src/eval.rs` contains `"...add{{}} block"`, which is a Rust +# `format!` ESCAPE (`{{}}` renders as a literal `{}`) describing the `add{}` +# language construct — not a placeholder. Files that legitimately *mention* +# the forbidden tokens (this script, the rule that forbids them, and the +# errata recording the debt) are listed explicitly below. +# +# USAGE: scripts/check-rsr-instantiation.sh +# EXIT: 0 = instantiated; 1 = template residue or phantom commands found + +set -uo pipefail +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "${ROOT}" || exit 1 + +fail=0 + +# Paths permitted to contain the forbidden tokens, with the reason. +# AFFIRMATION.adoc — dated errata recording the debt +# docs/identity-fabric/ — the task description +# methodology.a2ml — the reject-if-contains rule itself +# contractiles/Adjustfile.a2ml — the corrective-action text +# contractiles/dust/Dustfile.a2ml — note about generic templates +# scripts/check-rsr-instantiation.sh — this file +# src/rust/src/eval.rs — Rust format! escape, NOT a placeholder +# .github/workflows/dogfood-gate.yml, .githooks/, self-validating/ — links to +# the upstream template as an external resource, which is legitimate +ALLOW_RE='^(AFFIRMATION\.adoc|docs/identity-fabric/|docs/CHANGELOG|\.machine_readable/bot_directives/methodology\.a2ml|\.machine_readable/contractiles/Adjustfile\.a2ml|\.machine_readable/contractiles/dust/Dustfile\.a2ml|\.machine_readable/self-validating/|scripts/check-rsr-instantiation\.sh|src/rust/src/eval\.rs|\.github/workflows/dogfood-gate\.yml|\.githooks/)' + +echo "== template residue ==" +# Unfilled placeholders: {{UPPER_SNAKE}}. Deliberately does NOT match `{{}}`. +residue="$(grep -rn --binary-files=without-match \ + --exclude-dir=.git --exclude-dir=_build --exclude-dir=target \ + --exclude-dir=.claude --exclude-dir=node_modules \ + -E '\{\{[A-Z][A-Z_]*\}\}' . 2>/dev/null \ + | sed 's|^\./||' | grep -vE "${ALLOW_RE}" || true)" +if [[ -n "${residue}" ]]; then + echo "::error::Unfilled template placeholders:"; printf '%s\n' "${residue}"; fail=1 +else + echo " no unfilled {{PLACEHOLDER}} tokens" +fi + +# Files whose SUBJECT is still the template. +subject="$(grep -rn --binary-files=without-match \ + --exclude-dir=.git --exclude-dir=_build --exclude-dir=target \ + --exclude-dir=.claude --exclude-dir=node_modules \ + -F 'rsr-template-repo' . 2>/dev/null \ + | sed 's|^\./||' | grep -vE "${ALLOW_RE}" \ + | grep -viE 'https?://' || true)" +if [[ -n "${subject}" ]]; then + echo "::error::Files still describing rsr-template-repo as their subject:" + printf '%s\n' "${subject}" + echo " (A bare URL to the upstream template is fine; naming it as THIS repo is not.)" + fail=1 +else + echo " no file claims to be rsr-template-repo" +fi + +echo "== documented commands exist ==" +if ! command -v just >/dev/null 2>&1; then + echo "::warning::\`just\` not installed — skipping the phantom-command check." + echo " (Not a pass: the check did not run.)" +else + recipes="$(just --list 2>/dev/null | tail -n +2 | awk '{print $1}')" + missing=0 + while IFS= read -r doc; do + [[ -f "$doc" ]] || continue + while IFS= read -r r; do + [[ -z "$r" || "$r" == --* ]] && continue + if ! printf '%s\n' "${recipes}" | grep -qx -- "$r"; then + echo "::error::${doc} documents \`just ${r}\`, which is not a recipe" + missing=1 + fi + done < <(grep -oE '^just [a-z][a-z-]*' "$doc" | awk '{print $2}' | sort -u) + done < <(printf '%s\n' QUICKSTART-DEV.adoc QUICKSTART-MAINTAINER.adoc QUICKSTART-USER.adoc README.adoc) + if [[ "$missing" -eq 0 ]]; then echo " every documented \`just\` recipe exists"; else fail=1; fi +fi + +echo +if [[ "$fail" -ne 0 ]]; then + echo "::error::repo is not fully instantiated — see above." + exit 1 +fi +echo "RSR instantiation OK: no template residue, and the docs only name commands that exist." From 569a53f817e2956a4b661e2314f1ee04bd3192e4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 01:19:28 +0100 Subject: [PATCH 2/2] fix(ci): install just so the phantom-command check actually runs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The RSR guard's second half checks that every `just ` named in the docs exists. On the runner `just` was absent, so it emitted its warning and SKIPPED — announcing itself rather than silently passing, but skipping all the same. A check that never executes in CI is half a gate, and this is the exact half that would have caught the twelve phantom recipes. Co-Authored-By: Claude Opus 5 --- .github/workflows/ocaml-ci.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ocaml-ci.yml b/.github/workflows/ocaml-ci.yml index b137426..5188940 100644 --- a/.github/workflows/ocaml-ci.yml +++ b/.github/workflows/ocaml-ci.yml @@ -72,10 +72,15 @@ jobs: run: | set -euo pipefail sudo apt-get update -qq - sudo apt-get install -y --no-install-recommends ocaml ocaml-dune menhir + # `just` is needed by the RSR guard's phantom-command check. Without + # it that half of the guard skips (loudly, but it still does not run) + # — which is how the QUICKSTARTs accumulated a dozen commands that + # were never recipes. + sudo apt-get install -y --no-install-recommends ocaml ocaml-dune menhir just ocaml -version dune --version menhir --version + just --version - name: Build working-directory: compiler