Skip to content

Commit e9811d1

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: document hosting topology for humans and machines
Adds the missing map of where ECHIDNA actually runs, in both registers: - docs/HOSTING.md — the three public surfaces (Cloudflare Pages for the site, Hetzner behind Caddy for the API, Cloudflare Email Routing for contact), how each is built, and the two constraints that bite when editing the site: the SSG hard-fails on a11y violations, and its copyTree is text-only so binaries need cp. - .machine_readable/deployment.a2ml — the same topology as structured data, including the API's limits and the risks of exposing an unauthenticated service that spawns provers on user input. Both record the two current blockers honestly: repository-wide Actions startup_failure (a minimal probe workflow fails identically, so it is not a workflow-file fault), and an apex that resolves to Cloudflare but has no origin behind it. Both also carry the diagnostic that keeps catching people out: a workflow which fails at startup registers no check run, so gh pr checks reports success while every gate is dead — and a workflow listed by path rather than name has never been parsed. docs/deployment/DEPLOYMENT_GUIDE.md is reduced to a superseded stub. It described a 2025-11 v0.1.0 deployment whose next step was 'deploy to GitLab', referenced an unrelated migration, and quoted a fixed prover count that the canonical-reference policy forbids in prose. Kept as a stub so existing links do not dead-end. Verified: .githooks/validate-a2ml.sh passes (exit 0) with the new manifest present. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
1 parent 3e3f81a commit e9811d1

3 files changed

Lines changed: 254 additions & 630 deletions

File tree

‎.machine_readable/deployment.a2ml‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# deployment.a2ml — public hosting topology for ECHIDNA.
5+
# Human-facing companion: docs/HOSTING.md (keep the two in step).
6+
7+
[metadata]
8+
version = "1.0.0"
9+
last-updated = "2026-07-29"
10+
maintainer = "Jonathan D.A. Jewell (hyperpolymath)"
11+
companion-doc = "docs/HOSTING.md"
12+
13+
[dns]
14+
zone = "nesy-prover.dev"
15+
provider = "cloudflare"
16+
17+
[surfaces.website]
18+
hostname = "nesy-prover.dev"
19+
host = "cloudflare-pages"
20+
built-by = ".github/workflows/pages.yml"
21+
generator = "ddraig-ssg"
22+
generator-language = "idris2"
23+
content-root = "site/"
24+
extra-assets = "echidna-playground/"
25+
output-dir = "_site"
26+
status = "content-merged-not-live"
27+
# The build must remain in GitHub Actions: it requires Idris2, which managed
28+
# build images do not provide. CI produces _site and publishes that directory.
29+
build-must-stay-in-ci = true
30+
31+
[surfaces.website.constraints]
32+
# The SSG hard-fails the build on any accessibility violation.
33+
a11y-gate = "hard-fail"
34+
a11y-rules = ["exactly-one-h1-per-page", "no-skipped-heading-levels", "alt-required"]
35+
# Its copyTree is text-only and corrupts binaries; binary assets need `cp`.
36+
copytree-is-text-only = true
37+
link-extension = "html"
38+
39+
[surfaces.api]
40+
hostname = "api.nesy-prover.dev"
41+
host = "hetzner"
42+
runtime = "podman-rootless-quadlets"
43+
proxy = "caddy"
44+
image = "ghcr.io/hyperpolymath/echidna:latest"
45+
image-published-by = ".github/workflows/ghcr-publish.yml"
46+
image-public = true
47+
deploy-unit = "deploy/hetzner/"
48+
runbook = "deploy/hetzner/README.adoc"
49+
canonical-api-doc = "site/docs/api/core.md"
50+
status = "ready-not-deployed"
51+
52+
[surfaces.api.limits]
53+
rate-limit = "30/min/ip"
54+
request-body-max = "1MB"
55+
memory = "1500m"
56+
pids = 512
57+
tmpfs = "/tmp"
58+
no-new-privileges = true
59+
published-host-port = false # reachable only via caddy
60+
update-policy = "auto-update-registry"
61+
rollback-trigger = "HealthOnFailure=kill"
62+
63+
[surfaces.api.risks]
64+
# The API has no auth and spawns prover binaries on user input. Rate limiting
65+
# bounds request COUNT, not the cost of a single request. Lean accepts #eval,
66+
# i.e. arbitrary code at elaboration time.
67+
authentication = "none"
68+
per-request-prover-timeout = "absent"
69+
outstanding-work = "add server-side timeout around prover subprocess in src/rust/server.rs"
70+
71+
[surfaces.email]
72+
address = "sudo@nesy-prover.dev"
73+
host = "cloudflare-email-routing"
74+
mode = "forwarder"
75+
status = "not-configured"
76+
77+
[retired.fly-io]
78+
app = "echidna-nesy"
79+
reason = "cost"
80+
action = "delete fly.toml and .github/workflows/fly-deploy.yml"
81+
note = "the fly deploy action was never on the repository permitted-actions list"
82+
83+
[known-issues.actions-startup-failure]
84+
severity = "blocking"
85+
scope = "repository-wide"
86+
detected = "2026-07-27T22:45Z"
87+
symptom = "every workflow returns startup_failure, including pages.yml"
88+
# A minimal probe workflow (one SHA-pinned actions/checkout + echo) fails
89+
# identically, so this is not a fault in any workflow file.
90+
probe-also-fails = true
91+
ruled-out = [
92+
"workflow-yaml-validity",
93+
"unresolvable-action-shas",
94+
"billing-or-visibility",
95+
"ruleset-required-workflow",
96+
"account-wide-outage",
97+
"scalar-permissions-yaml-break",
98+
"actions-policy", # byte-identical to a healthy sibling repo
99+
]
100+
reason-not-exposed-by-api = true
101+
next-action = "read the banner on an Actions run page; it exists nowhere else"
102+
103+
[known-issues.apex-no-origin]
104+
severity = "blocking-website"
105+
symptom = "TLS to cloudflare completes, request then hangs"
106+
cause = "cloudflare proxying to an origin that does not exist"
107+
note = "DNS records are likely already correct; the Pages project is what is missing"
108+
109+
[diagnostics]
110+
# A startup-failed workflow registers NO check run, so `gh pr checks` reports
111+
# success while every real gate is dead. Always use `gh run list`.
112+
trust-gh-pr-checks = false
113+
liveness-command = "gh run list --branch main --json workflowName,conclusion"
114+
# A workflow displayed by PATH instead of NAME has never been parsed.
115+
never-parsed-tell = "workflowName equals .github/workflows/<file>.yml"
116+
never-parsed-confirm = "gh api repos/OWNER/REPO/actions/runs/<id>/jobs --jq '.jobs|length' == 0"

‎docs/HOSTING.md‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
<!--
2+
SPDX-License-Identifier: CC-BY-SA-4.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
6+
# Hosting and deployment topology
7+
8+
Where each public-facing piece of ECHIDNA runs, how it is published, and what
9+
state each piece is currently in. This is the human-facing companion to
10+
[`.machine_readable/deployment.a2ml`](../.machine_readable/deployment.a2ml);
11+
keep the two in step.
12+
13+
## The three surfaces
14+
15+
| Surface | Host | Built by | Source |
16+
|---|---|---|---|
17+
| `nesy-prover.dev` — website | **Cloudflare Pages** | `.github/workflows/pages.yml` (Ddraig SSG) | [`site/`](../site) + [`echidna-playground/`](../echidna-playground) |
18+
| `api.nesy-prover.dev` — HTTP API | **Hetzner**, rootless podman behind Caddy | `ghcr-publish.yml` → `ghcr.io/hyperpolymath/echidna` | [`deploy/hetzner/`](../deploy/hetzner) |
19+
| `sudo@nesy-prover.dev` — contact | **Cloudflare Email Routing** (forwarder) | n/a — DNS only | n/a |
20+
21+
DNS for the zone is on Cloudflare.
22+
23+
## Website
24+
25+
Content lives in [`site/`](../site) as Markdown and is rendered by **Ddraig
26+
SSG** (an Idris2 static site generator) inside `pages.yml`. The playground is
27+
copied in as static assets afterwards.
28+
29+
Two properties of the generator matter when editing:
30+
31+
- It **hard-fails the build** on any accessibility violation — more than one
32+
`<h1>` per page, a skipped heading level, or a missing `alt`. A page that
33+
fails prints `[a11y FAIL]` and the workflow exits non-zero. Every page must
34+
print `[a11y ok]`.
35+
- Its internal `copyTree` is **text-only and corrupts binary files**. Anything
36+
binary must be copied with `cp` in the workflow, never placed where the SSG
37+
will walk it. This is why the playground has its own copy step.
38+
39+
Build it locally exactly as CI does:
40+
41+
```bash
42+
ddraig build site _site https://nesy-prover.dev
43+
```
44+
45+
Links between pages are authored with `.html` extensions, because the SSG
46+
renders `foo.md` to `foo.html` at the same path and does not rewrite link
47+
targets.
48+
49+
### Publishing target
50+
51+
The apex is served by **Cloudflare Pages**. The build must stay in GitHub
52+
Actions because it requires Idris2, which managed build images do not provide;
53+
CI produces `_site` and publishes that directory.
54+
55+
> **Current state:** the content is merged and `pages.yml` is enabled, but the
56+
> site is not yet live — see *Known issues* below.
57+
58+
## API
59+
60+
The deployed service is the `echidna` binary's `server` subcommand. Its routes,
61+
request shapes and response shapes are documented in
62+
[`site/docs/api/core.md`](../site/docs/api/core.md), which was written from the
63+
route table and types in `src/rust/server.rs` — **that page is the accurate
64+
one**. The separate REST, GraphQL and gRPC interface binaries are optional and
65+
documented alongside it.
66+
67+
The full deployment procedure, including preflight gates, is
68+
[`deploy/hetzner/README.adoc`](../deploy/hetzner/README.adoc). In outline:
69+
70+
- `echidna` and `caddy` run as **rootless podman systemd quadlets** on a shared
71+
network; the API publishes **no host port** and is reachable only through Caddy
72+
- Caddy terminates TLS and applies a **30 req/min per-IP rate limit** and a
73+
**1 MB request body cap**
74+
- the container is capped at `--memory=1500m --pids-limit=512`, with a tmpfs
75+
`/tmp` and `NoNewPrivileges`
76+
- `AutoUpdate=registry` plus `HealthOnFailure=kill` means a new release rolls
77+
out unattended and an unhealthy container **fails the unit**, which is what
78+
makes rollback actually fire
79+
80+
### Why the caging matters
81+
82+
The API has **no authentication** and executes prover binaries on
83+
user-supplied input. Rate limiting bounds how *many* requests arrive; it does
84+
not bound the cost of a single one, and Lean accepts `#eval` — arbitrary code
85+
at elaboration time. A per-request server-side prover timeout is outstanding
86+
work (`src/rust/server.rs` spawns provers with no deadline).
87+
88+
## Known issues
89+
90+
1. **Repository Actions are failing at startup.** Every workflow in this
91+
repository currently returns `startup_failure`, including `pages.yml`. This
92+
is repo-level, not a fault in any workflow file — a minimal probe workflow
93+
containing a single SHA-pinned `actions/checkout` fails identically. Until
94+
it is resolved, nothing builds or deploys and **no gate verifies anything**.
95+
2. **The apex has no origin yet.** `nesy-prover.dev` resolves to Cloudflare
96+
proxy addresses; the TLS handshake completes and the request then hangs,
97+
because Cloudflare is proxying to an origin that does not exist. The DNS
98+
records are likely already correct — what is missing is the Pages project
99+
behind them.
100+
101+
### Diagnosing "the board is green but nothing ran"
102+
103+
A workflow that fails at startup registers **no check run at all**, so it
104+
cannot show up as missing or failing. `gh pr checks` will report success while
105+
every real gate is dead. Always confirm with:
106+
107+
```bash
108+
gh run list --branch main --json workflowName,conclusion
109+
```
110+
111+
A related tell: when `gh run list` shows a workflow by its **path**
112+
(`.github/workflows/x.yml`) instead of its **name**, that file has never been
113+
parsed successfully. Confirm with
114+
`gh api repos/OWNER/REPO/actions/runs/<id>/jobs --jq '.jobs|length'` returning `0`.
115+
116+
## Retired
117+
118+
**fly.io** — the `echidna-nesy` app is no longer used, for cost reasons.
119+
Any remaining `fly.toml` or `fly-deploy.yml` is dead weight and should be
120+
removed; the Fly deploy action was never on the repository's permitted-actions
121+
list in any case.

0 commit comments

Comments
 (0)