ci: deploy docs via Ddraig SSG#73
Merged
Merged
Conversation
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…ws (#78) The tangle half of a coordinated two-repo de-conflation pass. The krl half is hyperpolymath/krl#53 (merged) and hyperpolymath/krl#54. ## The three projects are separate **Tangle** is a general language for knot mathematics — topological, algebraic, geometric, logical. **QuandleDB** is a knot database. **KRL** is QuandleDB's resolution language, developed jointly with it. They share a subject matter, not an architecture. Documentation here presented Tangle as the substrate of a KRL compilation stack. That is false in both directions, and the connecting layer does not exist: > **`TangleIR` appears in NO source file in this repository** — 0 hits across `.rs`, `.zig` and `.lean` — **and in NO source file in the KRL implementation.** It existed only in prose, in both repos. The relationship between the projects is left intact. What is removed is a claimed architectural dependency that was never built. ## README.adoc - Retitled from *"Tangle / KRL — Topological Programming Language"* to **"Tangle — a general language for knot mathematics"**; removed *"Tangle (via KRL — Knot Resolution Language) is…"* from the opening line. - Removed the `KRL → TangleIR → Tangle core → QuandleDB + Skein.jl` ladder. - Removed the `== KRL — Knot Resolution Language` section, which restated KRL's four operations as though KRL were *this* project's surface language. - **Strengthened the formal core with a result rather than a claim** (below). - Added an explicit note that only the Lean proofs are CI-gated. ## The formal core is real — and now verified I ran the repository's own documented oracle: ```console $ cd proofs && lean Tangle.lean $ echo $? 0 ``` | Check | Result | |---|---| | `lean Tangle.lean` (pinned `leanprover/lean4:v4.14.0`) | **exit 0, no errors** | | `sorry` count | **0** | | `axiom` count | **0** | | `import` lines | **0** — self-contained, no Mathlib | | `progress`, `preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete`, `infer_iff_hasType` | all present with real proof terms | This is worth stating precisely: an `axiom` stub compiles cleanly while proving nothing, so *"the Lean build is green"* and *"the theorems are proved"* are different claims in general. **Here they coincide, and that was checked rather than assumed.** This is Tangle's strongest asset and the README now leads with it. ## AFFIRMATION.adoc — erratum, not edit An affirmation is a dated claim about a past state (`102499d`, 2026-06-19); amending it in place would falsify a record. So the original text is untouched and an erratum is appended. It corrects the *"maintainer-confirmed"* `KRL → TangleIR → VerisimCore → Skein/QuandleDB` stack, and flags that the quotable one-line characterisation shouldn't be quoted while it calls Tangle *"the … TangleIR of the KRL stack"*. It also **discharges one of the affirmation's own acknowledged gaps** — it recorded *"OCaml + Lean not run (absent)"* and concluded *"structure + the repo's proof records are confirmed, not a fresh green build."* The Lean half is now closed, with command and exit code recorded. ## READINESS.md — Grade C → D Grade C means *self-validated in the home context*; the `D → C` trigger is *"dogfood it hard in the home context."* The assessment cited **exactly one** piece of dogfooding evidence: > **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL That is false — KRL is not built on Tangle. With it withdrawn, C is unsupported. Two further corrections: - **"CI: Clean" was false** — `main` was failing Governance and both Jekyll workflows. - **The test suites are not run by CI.** Eight OCaml test files exist under `compiler/test/`, but **no workflow invokes `dune` or `cargo test`**. The cheapest available uplift is named explicitly: add a workflow running `dune build && dune test`. Eight suites already exist and nothing executes them. ## dialects/README.md - Removed KRL from the dialect table — it was listed as a dialect that had "graduated", and it was never a Tangle dialect. - Replaced the dead absolute path `/var/mnt/eclipse/repos/krl` (another machine) with the GitHub URL. - Dropped "wire through to TangleIR" from the maturation pattern. ## Workflows — two deleted `jekyll.yml` and `jekyll-gh-pages.yml` are GitHub's **sample** Jekyll workflows. This repo has **no `_config.yml` and no `Gemfile`** — there is no Jekyll site to build, so both fail on every push. `pages.yml` (Ddraig SSG, #73) is the real one; three workflows were competing for the same Pages deployment. ##⚠️ Owner action — GitHub Pages is not enabled `pages.yml` will **still** fail at the deploy step after this PR. Its build succeeds and certifies a11y, but: ``` GET /repos/hyperpolymath/tangle/pages -> 404 Not Found ``` which surfaces as `HttpError: Not Found / Creating Pages deployment failed`. **The same is true of `hyperpolymath/krl`.** Pages needs enabling with source = GitHub Actions on both. That publishes a public site, so I've left it to you rather than doing it. ## Verified on this branch `actionlint` 0 errors · `asciidoctor` renders `README.adoc` and `AFFIRMATION.adoc` clean · `lean Tangle.lean` exit 0
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Mass rollout for Ddraig SSG