feat(deploy): Hetzner deploy unit for api.nesy-prover.dev - #330
Merged
Conversation
Complete single-box deployment for the public API: rootless podman systemd quadlets (echidna API + Caddy TLS proxy), a Caddy image built on-host with mholt/caddy-ratelimit, and an operator runbook. The API is unauthenticated and spawns prover binaries on user input, so it is caged: no published host port (Caddy-only reachability over the quadlet network), 30 req/min/IP rate limit, 1 MB body cap, memory/pids limits, tmpfs /tmp, NoNewPrivileges. Updates roll out via podman-auto-update with healthcheck-gated rollback. Verified locally: quadlet -dryrun generates all three units with zero warnings and correct dependency ordering; the Caddy image builds with podman and 'caddy validate' accepts the Caddyfile with http.handlers.rate_limit present. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ating Adversarial review of this deploy unit found operator-facing defects: - Section 2 ran scp before the target directories existed, so a verbatim run failed on the first copy. Create /opt/echidna (root section) and ~/.config/containers/systemd (deploy user) first. - The auto-update rollback claim was not true as configured: an unhealthy-but-running container satisfies systemd, so nothing would have failed and nothing would have rolled back. Add HealthOnFailure=kill to echidna.container — an unhealthy container now fails the unit, which is what makes both Restart=always and auto-update's rollback fire — and describe the mechanism honestly. - The manual rollback procedure was silently undone by the next podman-auto-update.timer run, which re-pulls registry :latest. Stop the timer first, and document pinned mode as the durable exit. - The podman >= 4.4 floor was a guess that several keys in these units (HealthOnFailure= in particular) would not satisfy. Replace the guess with a measurement: the preflight now runs the quadlet generator in dry-run mode on the target host, which proves every key is understood regardless of version. - Clarify that the 1500m container cap sits deliberately below the 2 GB host requirement to leave headroom, and note that the plaintext isolation probe is asserting a closed port on purpose. Convert the indentation-based literal blocks to delimited source blocks so the runbook renders predictably. Verified: asciidoctor renders with no warnings; quadlet -dryrun generates all three units cleanly with --health-on-failure kill in the resulting ExecStart. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ Approved 1 resolved / 1 findingsAdds the Hetzner deployment configuration and operator runbook for the public ECHIDNA API, but the healthcheck uses ✅ 1 resolved✅ Bug: Healthcheck --version can't detect a broken API server
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
hyperpolymath
added a commit
that referenced
this pull request
Jul 29, 2026
Documents where ECHIDNA actually runs — the map that was missing after the site and deploy work landed in #329/#330. ## What's here **`docs/HOSTING.md`** (humans) — the three public surfaces and how each is built: | Surface | Host | |---|---| | `nesy-prover.dev` — website | Cloudflare Pages, built by `pages.yml` (Ddraig SSG) | | `api.nesy-prover.dev` — HTTP API | Hetzner, rootless podman quadlets behind Caddy | | `sudo@nesy-prover.dev` — contact | Cloudflare Email Routing forwarder | It also captures the two site constraints that bite when editing: the SSG **hard-fails the build** on any a11y violation (more than one `h1`, a skipped heading level, a missing `alt`), and its `copyTree` is **text-only and corrupts binaries** — which is why the playground has a separate `cp` step. **`.machine_readable/deployment.a2ml`** (machines) — the same topology as structured data, including the API's limits (`30/min/ip`, 1 MB body, `--memory=1500m --pids-limit=512`, no published host port) and an explicit risk block: the API has no authentication and spawns prover binaries on user input, rate limiting bounds request *count* rather than the cost of one request, and a per-request prover timeout is outstanding. ## Honest about what is broken Both files record the two live blockers rather than describing an aspirational happy path: 1. **Repository-wide Actions `startup_failure`** — every workflow, including `pages.yml`. A minimal probe workflow containing one SHA-pinned `actions/checkout` fails identically, so this is *not* a workflow-file fault. 2. **The apex has no origin** — `nesy-prover.dev` resolves to Cloudflare, the TLS handshake completes, and the request then hangs. The DNS records are likely already right; the Pages project behind them is what is missing. Both also carry the diagnostic that keeps costing time here: **a workflow that fails at startup registers no check run**, so `gh pr checks` reports success while every real gate is dead — and a workflow listed by *path* instead of *name* has never been parsed. ## Stale doc neutralised `docs/deployment/DEPLOYMENT_GUIDE.md` becomes a superseded stub. It described a 2025-11 v0.1.0 deployment whose next step was "deploy to GitLab", referenced an unrelated `zotero-voyant-export` migration, and quoted a fixed prover count that the canonical-reference policy forbids in prose. Kept as a stub so existing links don't dead-end. ## Verification `.githooks/validate-a2ml.sh` passes (exit 0) with the new manifest present — the same validator the dogfood gate runs. Note that CI cannot verify this PR: see blocker 1 above.
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.
Adds
deploy/hetzner/— the complete unit for running the public ECHIDNA API on a single server behind Caddy, plus an operator runbook.echidna(ghcr.io/hyperpolymath/echidna:latest,server --port 8081) andcaddy(built on-box withmholt/caddy-ratelimit) run as rootless podman systemd quadlets on a shared network. Caddy terminates TLS forapi.nesy-prover.devand is the only thing that can reach the API.Caging an unauthenticated prover service
The API has no authentication and spawns prover binaries on user-supplied input with no per-request timeout, so the deployment constrains it: no published host port, 30 req/min/IP rate limit, 1 MB request-body cap,
--memory=1500m --pids-limit=512,tmpfs /tmp,NoNewPrivileges, rootless. (A server-side prover timeout belongs in the code — worth a follow-up issue.)Review fixes already applied
scpbefore the target directories existed — a verbatim run failed on the first copyHealthOnFailure=killnow fails the unit on an unhealthy container, which is what makes bothRestart=alwaysand auto-update's rollback firepodman-auto-update.timerrun re-pulling:latest— the procedure now stops the timer first and documents pinned mode as the durable exitpodman >= 4.4floor was a guess these units do not satisfy. It is replaced by a measurement: preflight runs the quadlet generator in dry-run mode on the target host, proving every key is understood regardless of versionVerification
quadlet -dryrungenerates all three units with no warnings; the resultingExecStartcarries--health-on-failure kill, tmpfs,no-new-privileges, the autoupdate label, and both limitscaddy validateaccepts the Caddyfile withhttp.handlers.rate_limitpresentghcr.io/hyperpolymath/echidna:latestconfirmed anonymously pullable — no registry credentials needed on the serverasciidoctorrenders the runbook with no warningsDeployment itself is not part of this PR: it needs the server's SSH details and a Cloudflare token for the
apiA record.