139 lines
6.5 KiB
Markdown
139 lines
6.5 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
|
|
```
|
|
|
|
`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.)
|
|
|
|
## 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 `Projects/*/leanweb-build.sh` — the demo projects are
|
|
rebuilt and Mathlib's cache re-fetched, so treat this like the heavy build it
|
|
is (several GB of image; run it on the machine that hosts the editor).
|
|
|
|
## Adding Lean projects
|
|
|
|
Anything under `Projects/` of the *image source* becomes a selectable project
|
|
(`#project=<name>`). To ship one with the image, build a custom image that
|
|
copies it in before the project build step:
|
|
|
|
```dockerfile
|
|
FROM mathew-lean AS base # or edit lean/Dockerfile directly
|
|
COPY MyProject /opt/lean4web/Projects/MyProject
|
|
WORKDIR /opt/lean4web/Projects/MyProject
|
|
RUN 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.
|