diff --git a/.github/workflows/ocaml-ci.yml b/.github/workflows/ocaml-ci.yml index c90234b..5188940 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: {} @@ -64,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 @@ -108,6 +121,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."