feat(site): real multi-page site for nesy-prover.dev - #329
Conversation
Build the Pages artifact from a dedicated site/ content tree instead of the Rust src/ tree (which leaked five src/**/README.html pages onto the live site) and set the Ddraig base URL to the custom domain so canonical URLs, sitemap, and feed stop pointing at github.io. - site/index.md: landing page with live-API examples - site/docs/: platform docs + REST/GraphQL/gRPC references adapted from docs-site/content (prover counts stripped per R5a count-drift policy; licence corrected to AGPL-3.0-or-later) - pages.yml: build from site/, copy the playground in binary-safe with cp (ddraig copyTree is text-only) - playground: wire jsCoq 0.17.1 via jsdelivr ES module with a visible fallback banner; replace the mathcomp demo with a stdlib-only proof (the CDN package ships no mathcomp); drop dead scratchpad/favicon references; repoint deno dev/serve tasks at jsr:@std/http/file-server (server.ts never existed) Verified locally: ddraig build exits 0 with [a11y ok] on all five pages; sitemap URLs use https://nesy-prover.dev. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The @std/yaml lockfile entry was an accidental side effect of a local validation run, not a dependency of this change. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
An adversarial review of this branch confirmed that the API pages
carried over from docs-site/content described an API that does not
exist: GraphQL was documented at /graphql and /playground (both 404 —
the service serves POST and the playground at /), suggestTactics was
shown as a Query when it is a Mutation with different arguments, REST
documented timeout_ms instead of timeout_seconds and a tactic body of
{tactic} instead of the required {name, args}, gRPC showed a
SubmitProofResponse and a ProofUpdate shape neither of which is in the
proto, and every quick-start curl used https:// against services that
bind plain HTTP on loopback. Every copy-pasted example failed.
Rewrite all three interface references from source
(src/interfaces/{rest,graphql,grpc}), and add a core server reference
documenting what is actually deployed at api.nesy-prover.dev, taken
from the route table and request/response types in src/rust/server.rs.
Drop the stale 30-row prover table that claimed every backend is tier
'core' and point at the canonical tier table instead.
Also fix the playground fallback banner: the jsCoq import was static,
so a CDN fetch failure aborted module instantiation and the .catch
that reveals the banner never ran — precisely the case the banner
advertises. Use a dynamic import inside try/catch.
Verified: ddraig builds 6/6 pages [a11y ok]; every absolute internal
link resolves in the assembled artifact (including /playground/); the
playground references no asset beyond the styles.css that ships with it.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The site was dead for a reason outside this diffWhile verifying, I found the actual reason
I have re-enabled that one workflow ( An audit of both repos found three workflows silently off:
The two I left alone look deliberately disabled, so I have not touched them — worth confirming that is still the intent. Remaining blocker for the live site: apex DNSWith Pages building again, the apex still needs fixing. Cure: point the apex at the GitHub Pages addresses DNS-only (grey cloud) — A to |
![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 a multi-page site for nesy-prover.dev with landing, docs, and playground pages, but the jsCoq 0.17.1 initialization API entry point may not match usage in the playground script. ✅ 1 resolved✅ Bug: jsCoq 0.17.1 init API/entry point may not match usage
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
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.
1 participant
Turns the Pages output at nesy-prover.dev from a README dump into an actual site: landing page, platform docs, an accurate API reference, and a working in-browser Coq playground.
Why the build changed
pages.ymlbuilt fromsrc/— the Rust source tree — with a README shim. That published five straysrc/**/README.htmlpages to the live site and set the Ddraig base URL tohyperpolymath.github.io/echidna, so every canonical URL, sitemap entry and feed link pointed at the wrong host. It now builds from a dedicatedsite/tree with the custom domain as base, and copies the playground in withcp(Ddraig'scopyTreeis text-only and corrupts binaries).No
CNAMEfile is needed:build_typeisworkflow, so the custom domain lives in the Pages settings, where it is already verified.The API reference was wrong in every example
An adversarial review confirmed the pages inherited from
docs-site/contentdocumented an API that does not exist:/graphqland/playground— both 404; the service serves POST and the playground at/suggestTacticsshown as a Query; it is a Mutation taking(prover, context, goalState). The query issuggestTacticsByProofIdproofState(sessionId:)→id,submitProof(proverKind:)→prover+goal,applyTactic(sessionId:)→proofId+tactic+requiredargs)timeout_ms; the field istimeout_seconds(serde silently drops the unknown key, so an operator's timeout vanishes — and 30000 s vs ms is a 1000× trap if they only fix the name). Tactic body is{name, args}, not{tactic}SubmitProofResponseand aProofUpdateshape that are not in the protocurlusedhttps://against services that bind plain HTTP on loopbackAll three interface references are rewritten from source, and a new core server reference documents what is actually deployed at
api.nesy-prover.dev, taken from the route table and types insrc/rust/server.rs. The stale 30-row prover table claiming every backend is tier "core" is gone; the canonical tier table is linked instead.Playground
echidna-playground/index.htmlnever loaded jsCoq at all — the init block was commented out behind annpm installnote. It now loads jsCoq 0.17.1 from jsdelivr as an ES module. The bundled demo was Mathematical Components, which the CDN package does not ship, so the example is a stdlib-only induction proof (n + 0 = n) that actually runs.The load-failure banner uses a dynamic
import()insidetry/catch: with a static import, a failed CDN fetch aborts module instantiation, so the handler that reveals the banner would never run — in exactly the case the banner exists for.Verification
ddraig buildlocally: 6/6 pages[a11y ok](the SSG hard-fails on multiple h1s, skipped heading levels, or missing alt text)/playground/styles.cssshipped alongside itsitemap.xmlentries usehttps://nesy-prover.devNote on DNS (separate from this PR)
nesy-prover.devcurrently resolves to Cloudflare proxy IPs and does not answer (curlhangs), whilehyperpolymath.github.io/echidna301s to it. The apex records need reconciling to GitHub Pages before this site is reachable.