# lean/ — the Lean server

This folder builds [lean4web](https://github.com/leanprover-community/lean4web) —
whose server runs a real Lean process (with Mathlib) for every session — as a
Docker image serving websocket sessions on port `8080`. That is why it does not
live in the backend or the frontend: upstream asks for **a dedicated machine**.

The wiki's `/lean` page talks to this server **itself**: `frontend/app/utils/lean/`
implements a Lean language client (JSON-RPC over the websocket), and the page's
Monaco editor, Goals and Messages panes (`LeanWorkbench.vue`) are the wiki's own —
styled by the wiki, themed live. lean4web's bundled client is still built and
served at the port's root (dressed in the wiki's skin, see below); the editor's
status bar links to it for features the wiki client does not chase — live
collaboration and interactive widgets.

## Build & run

```bash
docker compose build lean            # long: fetches Mathlib and unpacks its cache
docker compose up -d lean            # → http://localhost:8080 (and the wiki's /lean)
docker compose logs -f lean

# or plain docker
docker build -t mathew-lean ./lean
docker run --rm -p 8080:8080 mathew-lean
```

The build is **multi-stage**: compilers, dev dependencies and build caches stay
in the builder, and the pushed image is a slim runtime carrying only what
sessions need — the node server, the elan toolchain, the built client, and
Mathlib's precompiled cache (the bulk of it, ~7GB of olean files; total image
~11GB). The upstream "Stable" demo project is dropped: it pinned a second
~3GB toolchain, and the wiki only ever opens the default project
(`MathlibDemo`).

`GET http://localhost:8080/health` answers when the server is up — the image
carries a `HEALTHCHECK` for it. The frontend finds the server at
`NUXT_PUBLIC_LEAN_URL` (default `http://localhost:8080`, dev included), so out
of the box there is nothing else to configure.

To build against a fixed lean4web release rather than its `main`:

```bash
docker build --build-arg LEAN4WEB_REF=v0.2.2 -t mathew-lean ./lean
```

(any branch or tag; the clone is shallow, so commit SHAs are not offered.)

## Keeping Mathlib out of the image

Mathlib's compiled cache is what makes this image (and pushing it) heavy. If
the registry or the CI runner chokes on it, build without Mathlib and let a
volume hold it instead:

```bash
docker build --build-arg BAKE_MATHLIB=false -t mathew-lean ./lean   # ~4GB
docker run --rm -p 8080:8080 -v lean-mathlib:/opt/lean4web/Projects/MathlibDemo/.lake mathew-lean
```

The `BAKE_MATHLIB=false` image still ships the pinned elan toolchain, but not
the project's `.lake`: the entrypoint notices a fresh volume and fills it once
at first start — `lake update` fetches the sources pinned in
`lake-manifest.json`, Mathlib's post-update hook downloads the matching
precompiled cache, `lake build` writes the project's own module. Expect ~10
minutes and a few hundred MB of download; restarts after that are instant,
and **image rebuilds never touch Mathlib again** (the volume stays). The
trade: the cache must survive on the host, first start needs network, and it
redoes once if you recreate with a clean volume — hence the default staying
`BAKE_MATHLIB=true`. The commented blocks in `docker-compose.yml` wire this
up for the production stack.

## The protocol the wiki's client speaks

The websocket endpoint is `/websocket/<project>` (project names come from
`GET /api/projects`, answered only same-origin — the REST endpoints carry no
CORS headers, so the wiki falls back to `MathlibDemo` when reaching the
server across origins; the websocket itself is CORS-free).
One JSON-RPC message per frame — the Lean 4 language
server protocol, which the server forwards raw to a per-session `lake serve`.
What `frontend/app/utils/lean/lsp.ts` + `useLeanSession.ts` do with it:

1. `initialize` — and Lean is strict here: `rootUri` must be a **string** (the
   server's URI rewriter throws on `null` and the message vanishes silently),
   `window.showDocument` must be `{ support: … }`, `insertTextFormat` must be
   `{ valueSet: [...] }`; the Lean watchdog exits the session on anything it
   cannot parse. Positions negotiate as `utf-16`, which matches Monaco.
2. `initialized`, then `textDocument/didOpen` a single document named
   `<project>/Main.lean`; edits go as debounced whole-document `didChange`s.
3. Goals: the custom request `$/lean/plainGoal` at the cursor answers
   `{ goals: string[], rendered }`. (`$/lean/plainMessages` no longer exists —
   Lean puts `#check`-style output in **severity-3 `publishDiagnostics`**,
   which is what the wiki's Messages pane reads; elaboration busy-state comes
   from `$/lean/fileProgress`.)
4. Server→client requests (`client/registerCapability`, `*/refresh`,
   `workspace/configuration`) get automatic `null` acknowledgements — a
   single-document client must still answer, or Lean waits.

## The skinned classic client

Reaching the server's own address (the wiki editor's status-bar link, or a
direct visit) opens lean4web's bundled client — and the image builds it
**wearing the wiki**. `theme/` holds the layer: `mathew.css` redefines the
`--vscode-*` custom properties lean4web itself paints with (top bar, menus,
modals, its Monaco editor) in Mathew's tokens — Computer Modern for the
chrome, the paper/slate surfaces, the violet accent — and bundles the CMU
fonts (with their SIL license); `theme-init.js` records the theme on
`<html data-mathew-theme>` before the first paint, taking `?theme=light|dark`
or the browser's preference. The `Dockerfile` copies both into the client's
`public/`, links them from `index.html`, and retitles the tab.

To re-skin or extend: edit `theme/mathew.css` and rebuild — the patch lands
after the cached Mathlib steps, so it is only a client rebuild.

## The server's own knobs

lean4web reads these from the environment — pass them with `-e` / compose
`environment` if you change them:

| Variable | Default here | Meaning |
| --- | --- | --- |
| `PORT` | `8080` | The one port for the editor client **and** its websocket |
| `NO_BWRAP` | `true` | Run Lean without bubblewrap — see Security below |
| `SSL_CRT_FILE` / `SSL_KEY_FILE` | unset | Serve HTTPS directly (the server also redirects :80 → https) |
| `PROJECTS_BASE_PATH` | `Projects` | Where the Lean projects live, relative to the repo root |
| `VITE_COLLAB` | `true` | lean4web's collaboration feature (set at build time) |

## Security

Upstream wraps each Lean session in [Bubblewrap](https://github.com/containers/bubblewrap);
that needs nested user namespaces, which a plain container does not have — so
this image sets `NO_BWRAP=true` and lets **Docker itself be the sandbox**. The
consequence to keep in mind: whoever can reach port `8080` can run Lean code
on this machine, inside the container. Keep the port on the LAN / VPN, or put
it behind a proxy with authentication, before exposing it past your network.

**TLS matters to the wiki page too**: if Mathew is served over HTTPS, the
browser will refuse the editor's `ws://` connection to an `http://` server
(mixed content). Serve the
Lean server over HTTPS — either its own `SSL_CRT_FILE`/`SSL_KEY_FILE`, or a
reverse proxy in front (websocket upgrade on the same path) — and point
`NUXT_PUBLIC_LEAN_URL` at the `https://` address.

## Updating

The image clones lean4web at build time, so a rebuild is an update:

```bash
docker compose build --pull lean && docker compose up -d lean
```

Rebuilding also re-runs the project build — Mathlib's pin moves with upstream
and its cache re-downloads, so treat this like the heavy build it is (run it
on the machine that hosts the editor; pin `LEAN4WEB_REF` for a build that
stands still).

CI follows the same split: `.gitea/workflows/deploy-lean.yml` rebuilds, pushes
and redeploys the lean image **only when `lean/**` changes**; the regular
deploy pipeline ignores `lean/**` entirely and just pulls whatever
`mathew-lean:latest` the registry holds. (In volume mode the pushed image is
~4GB and a lean rebuild doesn't fetch Mathlib at all.)

## Adding Lean projects

Anything under `Projects/` of the *running image* becomes a selectable project
(`#project=<name>`). To ship one with the image, add it in the Dockerfile's
builder stage, before the project build step:

```dockerfile
# in lean/Dockerfile, build stage, before the BAKE_MATHLIB step
COPY MyProject /opt/lean4web/Projects/MyProject
RUN cd Projects/MyProject && lake build
```

See upstream's [Adding Projects](https://github.com/leanprover-community/lean4web/blob/main/doc/Projects.md)
for the `leanweb-config.json` each project needs.