This commit is contained in:
138
lean/README.md
Normal file
138
lean/README.md
Normal file
@@ -0,0 +1,138 @@
|
||||
# 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.
|
||||
Reference in New Issue
Block a user