185 lines
9.2 KiB
Markdown
185 lines
9.2 KiB
Markdown
# 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. The manifest
|
|
`lake update` resolved gets saved into the volume and re-applied at every
|
|
start, so the packages in the volume and the manifest in the image never tell
|
|
different stories (an unsynced pair would try to re-fetch Mathlib from GitHub
|
|
at each session). 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. The production stack does
|
|
the latter: nginx serves it at `https://mathew.aranroig.com/api/lean` and
|
|
proxies to `lean:8080`; the compose service publishes 8080 on loopback only
|
|
(dev's frontend), so the public way in is that one address. Note that the
|
|
bundled classic client expects to sit at the server root — under `/api/lean`
|
|
its assets resolve against the wiki and 404; the wiki's own editor is fine.
|
|
|
|
## 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 inside one workflow and one deploy job:
|
|
`.gitea/workflows/deploy.yml` gates the lean build steps on the pushed diff — it rebuilds,
|
|
pushes and redeploys the lean image **only when `lean/**` changed** — while an app change
|
|
skips them and just pulls whatever `mathew-lean:latest` the registry holds, and a lean-only
|
|
change skips the app builds. (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.
|