Get started

The scaffold passes the audit without modification.

Build your first site

What you need
elan (the Lean version is pinned by NoGoals), Node (22.22 or newer within 22.x, or 24.8 or newer), and jq. The first build fetches Mathlib and takes a while.
Copy the scaffold
Place the minimal site next to a checkout of NoGoals. It passes the audit without modification.
Shell
```
cp -R nogoals/skills/nogoals/assets my-site
cd my-site && npm ci
```
Run the first audit
A new site has no published URLs yet, so the first run bootstraps the permalink baseline. When a baseline already exists the flag prints a warning and leaves it alone. --offline skips only the external-link liveness check.
Shell
```
./scripts/build.sh --audit --offline --update-baseline
✓ AUDIT PASSED — every publisher gate is green.
```
Add a page
Add one constructor to PageId. The compiler reports every match expression that needs an additional branch for the slug, body or page definition. The build fails if any required branch is missing.
Site/Blocks.lean
```
inductive PageId
  | index
  | about
  | pricing
```
Use an agent
NoGoals includes an agent skill with an explanation of the model, a scaffold and instructions for interpreting build failures. Link the skill, then ask the agent to add a pricing page.
Claude Code
```
mkdir -p ~/.claude/skills
ln -s "$PWD/../nogoals/skills/nogoals" ~/.claude/skills/nogoals
```

No Markdown front-end
Content is represented as Lean data, which forms the basis of the proofs. A site-owned script can generate Lean data from files containing long prose.
Japanese and English only
The text type has exactly two fields, ja and en. Supporting a different set of languages requires changing the generator.
Cloudflare Pages hosting model
The model follows Cloudflare Pages conventions for serving x/index.html at /x/ and for _headers and _redirects. Other hosts can serve the artifact, but link resolution is modelled on Pages.
Design is not formalized
Verification covers structure. Gradients and grids are not formalized.