diff --git a/AGENTS.md b/AGENTS.md index 83942b6..e5d63b9 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -6,9 +6,10 @@ The interface itself speaks five languages (en, es, ca, fr, de), chosen per acco ``` mathew/ -├── dev.sh # starts/stops both dev servers together +├── dev.sh # starts/stops all three services together (lean via docker compose) ├── backend/ Express 5 + Mongoose API (port 5000) -└── frontend/ Nuxt 4 / Vue 3 wiki UI (port 3000) +├── frontend/ Nuxt 4 / Vue 3 wiki UI (port 3000) +└── lean/ lean4web editor server — its own Docker image (port 8080) ``` ## Running the project @@ -16,13 +17,16 @@ mathew/ Requires MongoDB on `localhost:27017` (database `mathew`). ```bash -./dev.sh # both dev servers in foreground (Ctrl+C stops both) +./dev.sh # all three services in foreground (Ctrl+C stops all) ./dev.sh start|stop|restart|status -./dev.sh logs [all|backend|frontend] +./dev.sh logs [all|backend|frontend|lean] ``` Or per-service: `npm run dev` inside `backend/` or `frontend/` -(backend uses `node --watch`; backend has no build step). +(backend uses `node --watch`; backend has no build step). The Lean editor +(`/lean`) is the third service: `dev.sh` brings it up through docker compose +alongside the npm pair — the first build fetches Mathlib and takes a while, +and when docker is unavailable dev.sh says so and still starts the other two. Seed sample articles: `npm run seed` in `backend/`. @@ -36,7 +40,10 @@ Production (`docker-compose.yml`) points the backend at the LAN MongoDB server with the dev key). The stack's nginx resolves `backend`/`frontend` through Docker's DNS per request, so container recreates cannot leave it on a stale IP. Frontend API URL comes from `NUXT_PUBLIC_API_BASE` -(default `http://localhost:5000`, read via `runtimeConfig.public.apiBase`). The frontend image +(default `http://localhost:5000`, read via `runtimeConfig.public.apiBase`). The Lean +editor's address comes from `NUXT_PUBLIC_LEAN_URL` (default `http://localhost:8080`, +read via `runtimeConfig.public.leanUrl`) — on an HTTPS site it must be an https:// +address too, or the browser blocks it (and the `wss://` derived from it) as mixed content (see `lean/README.md`). The frontend image builds it empty: the browser then calls `/api` on its own origin, which nginx routes to `backend:5000`, while the Nuxt server's own (SSR) `/api` calls go through a `routeRules` proxy aimed at `NUXT_API_PROXY_TARGET` (`https://mathew.aranroig.com` baked in at image build — the @@ -45,6 +52,40 @@ by service name). There is **no test suite, linter, or typecheck script** configured — don't invent commands. +## Lean editor (`lean/`) + +`/lean` is now a **native editor**, not an iframe. The frontend speaks to the lean4web +server (`lean/`) directly over its websocket (`ws(s):///websocket/`), +carrying the Lean 4 **language server protocol** (LSP): the client sends `initialize`, +`didOpen`/`didChange`, `$/lean/plainGoal`; the server streams back `publishDiagnostics` +and goal answers. That replaces the old frame entirely — the wiki owns the editor (Monaco), +its theme (live, same page), and the Goals/Messages pane. + +`lean/Dockerfile` still builds lean4web (upstream's real Lean + Mathlib per session; +`--build-arg LEAN4WEB_REF=` pins it) and runs its websocket server on port 8080; +the compose `lean` service runs it. Upstream asks for a dedicated machine, and the image is +heavy (Mathlib). It runs `NO_BWRAP=true` — bubblewrap cannot nest in a container, so Docker +itself is the sandbox; whoever reaches the port can run Lean. Build/run, TLS, security and +projects: `lean/README.md`. + +- `frontend/app/utils/lean/lsp.ts` — a minimal LSP JSON-RPC client over a websocket + (request/response pairing, notification dispatch, and auto-ack of the server→client + requests a single-document client has no use for). It negotiates `utf-16` positions, + matching Monaco's column model. +- `frontend/app/utils/lean/lean-language.ts` — registers the `lean4` language with a + Monarch tokenizer and Monaco themes rebuilt from the wiki's live tokens: light/dark surfaces + plus the chosen `--accent`, so the caret, selection, active line number and keywords follow + the accent (`applyLeanTheme()` re-reads the tokens and switches on a live change; themes are + named by their palette, so a redefinition never races one Monaco has already cached). +- `frontend/app/composables/useLeanSession.ts` — the session: connect to a project, open + `Main.lean`, send debounced whole-document `didChange`s, track the cursor for `$/lean/plainGoal`, + split diagnostics into editor marks vs. Messages (severity 3 = Lean's `#check`-style info), + read elaboration progress. Lives at module scope so the running elaboration outlives the + book moving the page between hosts. +- `frontend/app/components/LeanWorkbench.vue` — Monaco + the Goals/Messages sidebar; loads + Monaco (and the worker) client-side only. Provides completions, hover, `\`→unicode input, + and the "open the classic lean4web client" escape link. + ## Backend (`backend/`) Plain JavaScript, ESM (`"type": "module"`, `.js` files with relative `.js` import specifiers). @@ -156,7 +197,7 @@ properties so themes swap at runtime via `data-theme`/`data-accent` attributes (set pre-paint by an inline script in `nuxt.config.ts`). UI wording is localized with `@nuxtjs/i18n` (`frontend/i18n/`): `i18n.config.ts` plus -one JSON catalog per language in `i18n/locales/` (all 350 keys, kept in parity with +one JSON catalog per language in `i18n/locales/` (all 405 keys, kept in parity with `en.json`). `strategy: 'no_prefix'` — the interface language never appears in a URL (`/wiki//` is the *article's* language) — with cookie detection (`mathew-locale`, `fallbackLocale: 'en'`) so the server renders in the right language @@ -200,6 +241,26 @@ copy + an `APP_LANGUAGES` entry + the code in the backend's `SUPPORTED_LOCALES`. *calc*, *plot*, *map*) and opening one lays the live surface on a page of the book beside the articles — `ToolPane.vue` is that page (spine, ×, `inert` when not in view), holding the surface extracted as `GraphStage.vue` / `CalculatorStage.vue`. + The 3D plotter is a third page of its own, `/calculator3d` — sidebar link + and all — drawn by `Calculator3DStage.vue` over `Scene3D.vue`: surfaces + z = f(x, y), a sampled mesh projected and shaded by hand onto one canvas, + quads laid farthest-first, no 3D library (`compileSurfaceExpression` in + `utils/plot-expression.ts` is its algebra). The two calculators share the + dock's shapes but never rows — each keeps its own, in localStorage. + A name in a field that is none of x, y, a constant or a called function + is a slider: a lone `k` or a `k = 2` claims one (plots nothing), and every + expression speaking the name answers to its value — the compile pass hands + each result its `vars`, and `useVarSliders` (values, each slider anchored + under the row that claims it, persistence) and `VarSliders.vue` are shared + by both calculators. + The Lean editor is a fourth page, `/lean`: `LeanWorkbench.vue` *is* the editor — Monaco + (loaded client-side; the `lean4` language and two wiki-matched themes live in + `utils/lean/lean-language.ts`) beside a native infoview of Goals, Messages and a status + line. `useLeanSession` speaks the Lean language protocol to the lean4web server (`lean/`, + address `runtimeConfig.public.leanUrl`) over one websocket, and lives at module scope so a + running elaboration survives the book remounting the page. A dead server answers with the + unreachable banner and a retry; a status-bar link opens the classic lean4web client in its + own tab. `useArticleTabs` files such a page under the identity `page:` and finds it at its own address (`tabAt`/`tabHref` know `toolFromPath`); while its page is open, the plain route hosts defer to the book and draw nothing, and asked plain @@ -349,5 +410,20 @@ copy + an `APP_LANGUAGES` entry + the code in the backend's `SUPPORTED_LOCALES`. the folder tallies come from `/articles/facets` rather than from the cards on screen — counting the loaded batch would let "40 topics" and the tallies grow as the reader scrolls. +- **`/lean` speaks to a server outside the stack.** The wiki does not use an iframe: the + frontend speaks Lean itself (see the **Lean editor** section) — the browser opens + `/websocket/` (`NUXT_PUBLIC_LEAN_URL`, default `http://localhost:8080` + — an address for the browser, not a server-side proxy target to fix up). The Lean server + is strict about the handshake: `rootUri` must be a *string* (the server's URI rewriter + throws on a null and the message vanishes), and capabilities like `showDocument.support` + and `insertTextFormat.valueSet` must be shaped objects — the Lean watchdog quits the + session otherwise. The Messages pane reads severity-3 diagnostics (that is where Lean + puts `#check` output; there is no `$/lean/plainMessages` anymore). Dev runs the server + with `./dev.sh` (via docker compose; or lean4web natively: `NO_BWRAP=true PORT=8080 npm run prod`). + On an HTTPS site the address must be https (its `wss://` is derived from it — an `http://` + Lean server refuses an https wiki outright). + A tool page like this is wired in step: `ToolPage`/`TOOL_PAGE_PATHS` + (`utils/routes.ts`), the page file, `TOOL_LABEL_KEYS`, the `ToolPane` branch and spine + glyph, the sidebar link, and the `PAGE_TOOLS` entry. - Frontend dev server may fall back to port 3001 if 3000 is taken. - `frontend/types/markdown-it-texmath.d.ts` provides types for the untyped texmath package. diff --git a/README.md b/README.md index ae3ccba..c487406 100644 --- a/README.md +++ b/README.md @@ -11,11 +11,12 @@ languages, each with its own address. ``` mathew/ -├── dev.sh # start/stop both dev servers together +├── dev.sh # start/stop all three services together (lean via docker compose) ├── docker-compose.yml # nginx + frontend + backend (prebuilt images) ├── nginx.conf # reverse proxy: / → frontend, /api/ → backend ├── backend/ # Express 5 + Mongoose API (port 5000) -└── frontend/ # Nuxt 4 / Vue 3 wiki UI (port 3000) +├── frontend/ # Nuxt 4 / Vue 3 wiki UI (port 3000) +└── lean/ # Lean editor server (lean4web) — its own Docker image (port 8080) ``` ## Quick start @@ -36,19 +37,23 @@ npm install npm run dev # → http://localhost:3000 ``` -Or run both together from the repo root: +Or run everything together from the repo root: ```bash -./dev.sh # both dev servers in the foreground (Ctrl+C stops both) +./dev.sh # all three services in the foreground (Ctrl+C stops all) ./dev.sh start|stop|restart|status -./dev.sh logs [all|backend|frontend] +./dev.sh logs [all|backend|frontend|lean] ``` +The third service is the **Lean editor server** (`lean/`), run through docker compose +alongside the two npm dev servers — the image's first build fetches Mathlib, so give it +time; without docker, `dev.sh` warns and starts backend + frontend anyway. + ### Scripts | Where | Command | What it does | | --- | --- | --- | -| root | `./dev.sh [dev]` | Both dev servers, foreground, tagged output, one Ctrl+C stops both | +| root | `./dev.sh [dev]` | All three services, foreground, tagged output, one Ctrl+C stops them all | | `backend/` | `npm run dev` | API with `node --watch` (no build step) | | `backend/` | `npm start` | API without watch | | `backend/` | `npm run seed` | A handful of sample articles | @@ -66,6 +71,7 @@ There is **no test suite, linter, or typecheck script** configured. | `backend/.env` | `JWT_SECRET` | *(insecure dev key)* | Signs session tokens — set this in production | | `backend/.env` | `AUTH_TOKEN_TTL` | `7d` | How long a session lasts | | `frontend` env | `NUXT_PUBLIC_API_BASE` | `http://localhost:5000` | Where the UI calls the API | +| `frontend` env | `NUXT_PUBLIC_LEAN_URL` | `http://localhost:8080` | The Lean server (`lean/`) the editor talks to | ## How it works @@ -117,6 +123,7 @@ first paint so there is no flash. Colours are CSS custom properties swapped by | `/` | Search, recently viewed, a way into the shelf | | `/articles` | The shelf, filed by topic — one folder per topic, opening onto a batch-at-a-time grid of cards; language and topic filters are applied by the API | | `/graph` | The wiki's link map: one node per article, one edge per linked pair | +| `/lean` | The Lean 4 editor — Monaco with a live Goals/Messages infoview, talking to its own Lean server (`lean/`) | | `/wiki//` | One language version of an article, drawn as a page of the book with its table of contents | | `/wiki/` | The short form, naming no language — turned onto the version the slug speaks | | `/wiki//edit` | Markdown editor with live preview (Write / Split / Preview) | @@ -197,6 +204,13 @@ passing the standard forwarded headers. Point `NUXT_PUBLIC_API_BASE` and `MONGO_ deployment's real addresses and set a real `JWT_SECRET` — the fallback key is a development convenience only, and anyone holding it can mint a session. +The stack also runs `lean` — the Lean server built from [`lean/`](lean/README.md), +listening on `8080` with its websocket on that one port; the wiki's editor speaks the +Lean language protocol to it directly. It keeps no +state of the wiki's, but it runs real Lean for every session, so plan the machine +accordingly; point `NUXT_PUBLIC_LEAN_URL` at the address the browser reaches (https if +the site is https — the `wss://` is derived from it, and mixed content is blocked). + ## Notes for contributors [`AGENTS.md`](AGENTS.md) is the working map of the codebase: file-by-file layout, the diff --git a/dev.sh b/dev.sh index 060c050..841781b 100755 --- a/dev.sh +++ b/dev.sh @@ -1,20 +1,40 @@ #!/usr/bin/env bash -# dev.sh — start/stop the frontend (Nuxt) and backend (Express) together. +# dev.sh — start/stop the frontend (Nuxt), backend (Express) and the Lean +# editor server (lean4web via docker compose) together. # # Usage: -# ./dev.sh Start both in the foreground (Ctrl+C stops both) -# ./dev.sh start Start both dev servers in the background -# ./dev.sh stop Stop both dev servers +# ./dev.sh Start everything in the foreground (Ctrl+C stops all) +# ./dev.sh start Start everything in the background +# ./dev.sh stop Stop everything # ./dev.sh restart Stop then start -# ./dev.sh status Show which services are running -# ./dev.sh logs [service] Follow logs (all, backend, or frontend) +# ./dev.sh status Show what is running +# ./dev.sh logs [service] Follow logs (all, backend, frontend, or lean) +# +# backend and frontend are npm dev servers; lean is the Lean editor server +# from docker-compose.yml (see lean/). It is the heavy one — the image's +# first build fetches Mathlib — so dev.sh only rides along with docker: when +# docker is not available it says so and starts the other two regardless. set -euo pipefail ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" PID_DIR="$ROOT/.pids" LOG_DIR="$ROOT/.logs" +COMPOSE="$ROOT/docker-compose.yml" SERVICES=("backend" "frontend") +LEAN_LOG="$LOG_DIR/lean.log" + +compose() { docker compose -f "$COMPOSE" "$@"; } + +# The Lean server needs docker up, not just installed — probing the daemon +# keeps a dead docker socket from failing backend + frontend. +docker_ready() { + command -v docker >/dev/null 2>&1 && docker info >/dev/null 2>&1 +} + +lean_running() { + docker_ready && [[ -n "$(compose ps --status running --services 2>/dev/null | grep -x lean)" ]] +} pid_of() { local pid_file="$PID_DIR/$1.pid" @@ -43,6 +63,25 @@ start_service() { echo "started $name (PID $pid) — log: $LOG_DIR/$name.log" } +# `up -d` also builds the image the first time it is asked for (heavy: +# Mathlib), so this rides in the background with its output to lean.log +# rather than holding `start` hostage to a cold build. +start_lean() { + if lean_running; then + echo "lean is already running (docker compose)" + return + fi + if ! docker_ready; then + echo "lean: docker is not available — skipping the Lean server (see lean/README.md)" >&2 + return + fi + mkdir -p "$LOG_DIR" + setsid bash -c 'cd "$1" && exec docker compose -f "$2" up -d lean' _ "$ROOT" "$COMPOSE" \ + > "$LEAN_LOG" 2>&1 & + echo "starting lean (docker compose) — log: $LEAN_LOG" + echo " (the first build fetches Mathlib and takes a while)" +} + stop_service() { local name="$1" local pid @@ -68,6 +107,17 @@ stop_service() { echo "stopped $name (PID $pid)" } +# `stop`, not `down` — the container is kept (like a stopped dev server), +# and `docker compose down` stays the maintainer's call. +stop_lean() { + if ! lean_running; then + echo "lean is not running" + return + fi + compose stop lean >/dev/null 2>&1 || true + echo "stopped lean (docker compose)" +} + status() { for name in "${SERVICES[@]}"; do if is_running "$name"; then @@ -76,9 +126,17 @@ status() { echo "$name: stopped" fi done + if lean_running; then + echo "lean: running (docker compose)" + elif docker_ready; then + echo "lean: stopped" + else + echo "lean: stopped (docker is not available)" + fi } FG_PIDS=() +LEAN_PID="" SHUTTING=0 # Stop all foreground services (and their process groups). A second call @@ -88,11 +146,17 @@ fg_stop_all() { if [[ $SHUTTING -eq 1 ]]; then sig=KILL; else SHUTTING=1 echo - echo "stopping frontend + backend..." + echo "stopping backend + frontend + lean..." fi for pid in "${FG_PIDS[@]:-}"; do kill -"$sig" -- "-$pid" 2>/dev/null || kill -"$sig" "$pid" 2>/dev/null || true done + if [[ -n "$LEAN_PID" ]]; then + kill -"$sig" -- "-$LEAN_PID" 2>/dev/null || kill -"$sig" "$LEAN_PID" 2>/dev/null || true + # belt and braces: if the compose client died before telling dockerd, + # the container is still up — `stop` is quick and idempotent. + docker_ready && compose stop lean >/dev/null 2>&1 || true + fi wait 2>/dev/null || true for name in "${SERVICES[@]}"; do rm -f "$PID_DIR/$name.pid"; done exit 0 @@ -116,11 +180,22 @@ foreground() { FG_PIDS+=("$pid") echo "$pid" > "$PID_DIR/$name.pid" done + # The Lean server rides along the same way — compose `up` streams its + # build/run output, tagged. But the pair stays in charge: lean's absence + # (no docker) or its failure (no image, daemon flake) never takes them + # down, so `wait -n` watches only the npm services. + if docker_ready; then + setsid bash -c 'cd "$1" && exec docker compose -f "$2" up lean' _ "$ROOT" "$COMPOSE" \ + > >(sed -u "s/^/[lean] /") 2>&1 & + LEAN_PID=$! + else + echo "[lean] docker is not available — running without the Lean server (see lean/README.md)" >&2 + fi trap 'fg_stop_all' INT TERM - echo "frontend + backend running — press Ctrl+C to stop both" - # Exit as soon as either service dies, so they always run/stop together. - wait -n - echo "a dev server exited — stopping the other one..." + echo "backend + frontend running (lean if docker allows) — press Ctrl+C to stop all" + # Exit as soon as either dev server dies, so they always run/stop together. + wait -n "${FG_PIDS[@]}" + echo "a dev server exited — stopping the others..." fg_stop_all } @@ -130,29 +205,46 @@ case "${1:-dev}" in ;; start) for name in "${SERVICES[@]}"; do start_service "$name"; done + start_lean echo echo "backend: http://localhost:5000" echo "frontend: http://localhost:3000" + echo "lean: http://localhost:8080 (docker compose) — the wiki frames it at /lean" ;; stop) for name in "${SERVICES[@]}"; do stop_service "$name"; done + stop_lean ;; restart) for name in "${SERVICES[@]}"; do stop_service "$name"; done + stop_lean for name in "${SERVICES[@]}"; do start_service "$name"; done + start_lean ;; status) status ;; logs) case "${2:-all}" in - all) tail -f "$LOG_DIR"/*.log ;; + # `all` mixes the file logs with the container's — lean lives in + # docker, not in a dev.log, once it is up. + all) + if docker_ready; then + compose logs -f lean & + LEAN_LOG_PID=$! + trap 'kill "$LEAN_LOG_PID" 2>/dev/null || true' INT TERM + fi + tail -f "$LOG_DIR"/*.log + ;; backend|frontend) tail -f "$LOG_DIR/$2.log" ;; - *) echo "usage: $0 logs [all|backend|frontend]"; exit 1 ;; + lean) + if docker_ready; then compose logs -f lean; else echo "docker is not available" >&2; exit 1; fi + ;; + *) echo "usage: $0 logs [all|backend|frontend|lean]"; exit 1 ;; esac ;; *) - echo "usage: $0 [dev|start|stop|restart|status|logs [all|backend|frontend]] (default: dev)" + echo "usage: $0 [dev|start|stop|restart|status|logs [all|backend|frontend|lean]] (default: dev)" exit 1 ;; esac diff --git a/docker-compose.yml b/docker-compose.yml index 2776ab6..ab9427c 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -14,6 +14,20 @@ services: frontend: image: git.aranroig.com/syndria98/mathew-frontend:latest + environment: + # Where the browser finds the Lean editor server below (the wiki's + # /lean frames it). An https:// site needs an https:// address here, + # or the browser refuses the frame — see lean/README.md. + NUXT_PUBLIC_LEAN_URL: ${NUXT_PUBLIC_LEAN_URL:-http://mathew.aranroig.com:8080} + restart: always + + # The Lean editor (lean4web) — its own server, since it runs a real Lean + # process per session and asks for a dedicated machine (see lean/). + lean: + build: ./lean + image: mathew-lean:latest + ports: + - "8080:8080" restart: always backend: diff --git a/frontend/app/assets/css/_book.scss b/frontend/app/assets/css/_book.scss index cfac660..c1e54b8 100644 --- a/frontend/app/assets/css/_book.scss +++ b/frontend/app/assets/css/_book.scss @@ -273,12 +273,12 @@ // The link map and the graphing calculator are pages too: the search popup // lays one of them on the book beside the articles (ToolPane.vue). It fills // the page edge to edge — no column of prose scrolls here, the surface keeps -// its own docks and toolbars — and it takes the whole share of the desk, a -// plane being no narrower read than a page of text. Each stage's own sheet -// answers for the rest (_graph.scss, _calculator.scss). +// its own docks and toolbars — and it is held to the very width an article +// page is (the .book-pane rules: --pane-max-w, and the whole desk when it is +// the only page open). Each stage's own sheet answers for the rest +// (_graph.scss, _calculator.scss). .book-pane.pane-tools { - max-width: none; overflow: hidden; } diff --git a/frontend/app/assets/css/_calculator.scss b/frontend/app/assets/css/_calculator.scss index d654093..f36451d 100644 --- a/frontend/app/assets/css/_calculator.scss +++ b/frontend/app/assets/css/_calculator.scss @@ -115,8 +115,9 @@ font: italic 0.95rem/1 'Computer Modern', Georgia, serif; } -// a relation or point carries no lone "y =", so it sheds the gutter and the -// input takes back the room it stood in +// only a field that reads as a function wears the "y =" gutter; everything +// else — a relation, point, slider, or unfinished text — is bare, and the +// input takes back the room the gutter stood in .calc-input-box.bare .calc-input { padding-left: 10px; } @@ -134,6 +135,77 @@ &.input-error { color: var(--danger); } } +// The typeset echo of the field's text (Desmos' way): while the reader +// types, the formula sets on its own line under the text; once the field +// rests, it takes the text's place beside the "y =" gutter, so the dock +// reads as mathematics. A click wakes the text again (the box is a label); +// the input only steps out of sight, never out of the tab order — and +// Tab waking it draws the text back. An expression that does not read +// carries no echo, so it stays plain text and red, as ever. +.calc-typeset { + display: none; + color: var(--text); + + .katex { font-size: 1rem; } +} + +.calc-input-box.typeset { + flex-wrap: wrap; + + .calc-typeset { display: block; } + + // typing: the echo takes a line of its own, under the field + &:focus-within .calc-typeset { + flex: 0 0 100%; + padding: 0 10px 8px; + } + + // at rest: the field folds away and the formula stands in its place + &:not(:focus-within) { + .calc-input { + flex: none; + width: 0; + min-width: 0; + padding: 0; + opacity: 0; + } + + .calc-typeset { + flex: 1; + min-width: 0; + padding: 8px 10px; + overflow-x: auto; + } + } +} + +// A row that declared a variable ("k", "k = 3"). Once the reader stops +// editing it, the field folds away to nothing — the name and value now live +// in the slider laid in its place (see .calc-vars.is-inline). The input stays +// mounted and focusable (never display:none), so the slider's name can be a +// label that wakes it back to edit the declaration; a focused field stands +// open as any other. This is how a made variable reads as just a slider, not +// a "k = 3" box above a slider. +.calc-input-box.var-decl:not(:focus-within) { + flex: 0 0 0; + min-width: 0; + overflow: hidden; + border-color: transparent; + background: transparent; + + .calc-input { + width: 0; + min-width: 0; + padding: 0; + } +} + +// while the declaration's text is awake, its inline slider steps aside — the +// field is the whole row again +.calc-input-box.var-decl:focus-within ~ .calc-vars.is-inline { + display: none; +} + .calc-remove:hover { color: var(--danger); background: color-mix(in srgb, var(--danger) 10%, transparent); @@ -148,6 +220,86 @@ .calc-add { margin-top: 12px; } +// free variables ("k", "a", "radius") — each slider hangs just under the +// row that claims it. The name sets like the maths it names; the drag does +// the rough work, the field the fine +.calc-vars { + display: flex; + flex-direction: column; + gap: 4px; + margin: 5px 0 2px; + padding: 0; + list-style: none; +} + +.calc-var { + display: flex; + align-items: center; + gap: 8px; +} + +.calc-var-name { + flex: none; + min-width: 1.5ch; + color: var(--text); + font: italic 0.98rem/1 'Computer Modern', Georgia, serif; +} + +// the name of a made variable is the door back to its declaration: it is a +// label for the folded field, so clicking it wakes "k = 3" to be edited +.calc-var-name.editable { + padding: 1px 2px; + border-radius: 4px; + cursor: text; + + &:hover { background: var(--surface-2); } +} + +// a made variable's slider laid in the row in place of its field: no hanging +// margin, the drag takes the room the field used to hold +.calc-vars.is-inline { + flex: 1; + min-width: 0; + margin: 0; + gap: 0; +} + +.calc-var-range { + flex: 1; + min-width: 0; + accent-color: var(--accent); +} + +.calc-var-number { + flex: none; + width: 58px; + min-width: 0; + padding: 3px 6px; + border: 1px solid var(--border); + border-radius: 7px; + background: var(--bg-elev); + color: var(--text); + font: 0.8rem/1.3 'Computer Modern', Georgia, serif; + font-variant-numeric: tabular-nums; + + // no spinners on the slider's little twin — the drag is the spinner + -moz-appearance: textfield; + appearance: textfield; + + &::-webkit-outer-spin-button, + &::-webkit-inner-spin-button { + -webkit-appearance: none; + appearance: none; + margin: 0; + } + + &:focus { + outline: none; + border-color: var(--accent); + box-shadow: var(--ring); + } +} + // the fold: the dock slides out to the left, under the app sidebar, and a // quiet card takes its place at the plane's top-left corner .calc-dock-enter-active, @@ -195,6 +347,131 @@ box-shadow: var(--shadow-sm); } +// the 3D scene hangs its toolbar from a wrapper so the configuration +// card can fold out under it: the wrapper takes the corner, the row +// keeps its look on the hinge +.plot-tools { + position: absolute; + top: 10px; + right: 12px; + z-index: 2; + + .plot-toolbar { position: static; } + + // the configuration button while its card is open, the graph menu's way + .panel-icon-btn.open { color: var(--text); background: var(--surface-2); } +} + +// the configuration card: the space the surfaces stand in — each edge +// editable, the height by default the surfaces' own, the mesh's fineness +.plot-config { + @include dropdown-panel($z: 20, $overflow: visible); + right: 0; + min-width: 250px; + padding: 10px 12px; +} + +.plot-config-row { + display: flex; + align-items: baseline; + justify-content: space-between; + gap: 18px; + padding: 3px 0; +} + +.plot-config-axis { + color: var(--muted); + font: italic 13px 'Computer Modern', Georgia, serif; +} + +.plot-config-label { + color: var(--muted); + font-size: 0.8rem; + font-weight: 600; +} + +.plot-config-value { + color: var(--text); + font: 0.82rem/1.3 'Computer Modern', Georgia, serif; + font-variant-numeric: tabular-nums; + white-space: nowrap; +} + +.plot-config-bounds { + display: flex; + align-items: center; + gap: 6px; +} + +.plot-config-dots { + color: var(--faint); +} + +.plot-config-input { + width: 68px; + min-width: 0; + padding: 4px 7px; + border: 1px solid var(--border); + border-radius: 7px; + background: var(--surface); + color: var(--text); + font: 0.82rem/1.2 'Computer Modern', Georgia, serif; + font-variant-numeric: tabular-nums; + + &:focus { + outline: none; + border-color: var(--accent); + box-shadow: var(--ring); + } +} + +// the switch that decides whose height z answers to: the surfaces' or +// the reader's own two bounds +.plot-config-toggle { + display: flex; + align-items: center; + justify-content: space-between; + gap: 12px; + width: 100%; + margin-top: 7px; + padding: 7px 0 5px; + border-top: 1px solid var(--border); + color: var(--muted); + font-size: 0.74rem; + line-height: 1.35; + text-align: left; + + &:hover { color: var(--text); } +} + +.plot-config-switch { + position: relative; + flex: none; + width: 32px; + height: 18px; + border-radius: 999px; + background: var(--border-strong); + transition: background-color 0.15s; + + .knob { + position: absolute; + top: 2px; + left: 2px; + width: 14px; + height: 14px; + border-radius: 50%; + background: var(--bg-elev); + box-shadow: var(--shadow-sm); + transition: transform 0.15s ease; + } + + &.on { + background: var(--accent); + + .knob { transform: translateX(14px); } + } +} + // where the cursor stands, bottom-right so the dock never covers it .plot-readout { position: absolute; @@ -246,6 +523,8 @@ .plot-toolbar { top: 8px; right: 8px; } + .plot-tools { top: 8px; right: 8px; } + // during the fold the dock lifts out of the flow, so the plane takes the // width back at once rather than after the slide .calc-dock-leave-active { position: absolute; left: 0; right: 0; } diff --git a/frontend/app/assets/css/_lean.scss b/frontend/app/assets/css/_lean.scss new file mode 100644 index 0000000..22f74fd --- /dev/null +++ b/frontend/app/assets/css/_lean.scss @@ -0,0 +1,271 @@ +@use 'mixins' as *; + +// ---------- Lean editor (/lean) ---------- + +// The wiki's own Lean workbench. On the /lean address it owns the space +// beside the sidebar the way the map and the plane do — fixed, edge to +// edge. In a book pane it becomes the pane's own box instead. +// (The page transition only fades, so no transform steals the +// fixed positioning.) +.lean-stage { + position: fixed; + inset: 0 0 0 var(--sidebar-w); + transition: left 0.22s ease; + z-index: 1; + background: var(--bg); +} + +.pane-stage .lean-stage { + position: absolute; + inset: 0; +} + +// editor left, infoview right — the workbench of every Lean editor, in +// the wiki's own materials. The fold closes the panel's track and the +// editor takes the whole width. +.lean-work { + position: absolute; + inset: 0; + display: grid; + grid-template-columns: minmax(0, 1fr) 340px; + transition: grid-template-columns 0.22s ease; +} + +.lean-work[data-panel='collapsed'] { + grid-template-columns: minmax(0, 1fr) 0; +} + +.lean-work-editor { + position: relative; + min-width: 0; + background: var(--surface); +} + +.lean-work-panel { + display: flex; + flex-direction: column; + min-width: 0; + min-height: 0; + border-left: 1px solid var(--border); + background: var(--bg-elev); + overflow: hidden; + visibility: visible; + transition: opacity 0.18s ease, visibility 0s; +} + +.lean-work[data-panel='collapsed'] .lean-work-panel { + opacity: 0; + visibility: hidden; + // out of sight and out of the reader's way — only after the track closes + transition: opacity 0.18s ease, visibility 0s 0.22s; +} + +// status row: whose Lean, doing what, and the door to the classic client +.lean-work-status { + display: flex; + align-items: center; + gap: 8px; + padding: 9px 12px; + border-bottom: 1px solid var(--border); + font-size: 0.74rem; + color: var(--muted); + + .lean-work-dot { + width: 7px; + height: 7px; + border-radius: 50%; + background: var(--faint); + flex-shrink: 0; + } + + &[data-phase='ready'] .lean-work-dot { background: var(--success); } + &[data-phase='lost'] .lean-work-dot { background: var(--danger); } + &[data-phase='connecting'] .lean-work-dot, + &[data-phase='initializing'] .lean-work-dot { background: var(--accent); } + + // elaborating: the amber pulse every Lean editor wears while working + &[data-busy='true'] .lean-work-dot { + background: #d97706; + animation: lean-pulse 1s ease-in-out infinite; + } + + [data-theme='dark'] &[data-busy='true'] .lean-work-dot { background: #f5a83c; } +} + +@keyframes lean-pulse { + 50% { opacity: 0.35; } +} + +.lean-work-phase { + min-width: 0; + overflow: hidden; + text-overflow: ellipsis; + white-space: nowrap; +} + +// the status row's two quiet doors: the classic client outside, and the fold +.lean-work-classic, +.lean-work-collapse { + display: grid; + place-items: center; + width: 24px; + height: 24px; + border-radius: 7px; + color: var(--faint); + transition: color 0.15s ease, background 0.15s ease; + + &:hover { + color: var(--text); + background: var(--surface-2); + } +} + +.lean-work-classic { + margin-left: auto; +} + +// the panes below: Goals and Messages, the wiki's own infoview +.lean-work-goals, +.lean-work-messages { + padding: 10px 12px 14px; + overflow-y: auto; + min-height: 0; + + h3 { + margin: 0 0 8px; + font-size: 0.66rem; + font-weight: 600; + text-transform: uppercase; + letter-spacing: 0.06em; + color: var(--faint); + } + + pre { + margin: 0 0 8px; + padding: 9px 11px; + border: 1px solid var(--border); + border-radius: 10px; + background: var(--surface); + color: var(--text); + font-family: ui-monospace, 'JetBrains Mono', 'Cascadia Code', 'Fira Code', Menlo, Consolas, monospace; + font-size: 0.78rem; + line-height: 1.55; + white-space: pre-wrap; + word-break: break-word; + } +} + +.lean-work-goals { flex: 1 1 55%; } +.lean-work-messages { + flex: 1 1 45%; + border-top: 1px solid var(--border); +} + +.lean-work-messages ul { + list-style: none; + margin: 0; + padding: 0; + + li { position: relative; } +} + +.lean-work-msg-line { + font-family: ui-monospace, 'JetBrains Mono', Menlo, Consolas, monospace; + font-size: 0.66rem; + color: var(--faint); +} + +.lean-work-none { + margin: 0; + font-size: 0.8rem; + color: var(--faint); +} + +// the fold's other half: while the panel lies collapsed, this quiet card +// waits at the editor's top-right corner to pull the infoview back +.lean-panel-open { + position: absolute; + top: 10px; + right: 12px; + z-index: 2; + display: flex; + align-items: center; + gap: 6px; + padding: 7px 12px; + border: 1px solid var(--border); + border-radius: 11px; + background: color-mix(in srgb, var(--bg-elev) 84%, transparent); + backdrop-filter: blur(10px); + box-shadow: var(--shadow-sm); + color: var(--muted); + font-size: 0.84rem; + font-weight: 650; + white-space: nowrap; + transition: color 0.15s, background-color 0.15s; + + &:hover { color: var(--text); background: var(--surface-2); } +} + +// until Lean answers — and when the server is not there at all — the +// wiki speaks for the editor +.lean-state { + position: absolute; + inset: 0; + z-index: 1; + display: grid; + place-items: center; + align-content: center; + gap: 14px; + padding: 24px; + background: var(--bg); + + .banner { width: min(520px, 100%); } +} + +.lean-spinner { + width: 22px; + height: 22px; + border-radius: 50%; + border: 2px solid color-mix(in srgb, var(--accent) 25%, transparent); + border-top-color: var(--accent); + animation: lean-spin 0.7s linear infinite; +} + +@keyframes lean-spin { + to { transform: rotate(1turn); } +} + +.lean-loading-text { + margin: 0; + font-size: 0.86rem; + color: var(--muted); +} + +// small screens: the panel lies under the editor instead of beside it — +// and collapses into the bottom edge the same way +@media (max-width: 900px) { + .lean-work { + grid-template-columns: none; + grid-template-rows: minmax(0, 1fr) minmax(0, 40%); + transition: grid-template-rows 0.22s ease; + } + + .lean-work[data-panel='collapsed'] { + grid-template-columns: none; + grid-template-rows: minmax(0, 1fr) minmax(0, 0%); + } + + .lean-work-panel { + border-left: 0; + border-top: 1px solid var(--border); + } +} + +@media (prefers-reduced-motion: reduce) { + .lean-stage { transition: none; } + .lean-work { transition: none; } + .lean-work-panel { transition: opacity 0.01s ease, visibility 0s; } + .lean-work[data-panel='collapsed'] .lean-work-panel { transition: opacity 0.01s ease, visibility 0s; } + .lean-spinner { animation-duration: 1.4s; } + .lean-work-status[data-busy='true'] .lean-work-dot { animation: none; } +} diff --git a/frontend/app/assets/css/main.scss b/frontend/app/assets/css/main.scss index 6dedbb8..0403177 100644 --- a/frontend/app/assets/css/main.scss +++ b/frontend/app/assets/css/main.scss @@ -27,4 +27,5 @@ @use 'book'; // the reader: an open book of article pages @use 'graph'; // the link map @use 'calculator'; // the graphing calculator: function rows + the plane +@use 'lean'; // the Lean editor: a frame over the lean4web server (lean/) @use 'transitions'; // route fades, scrollbars diff --git a/frontend/app/components/AppHeader.vue b/frontend/app/components/AppHeader.vue index e2247a3..98067ba 100644 --- a/frontend/app/components/AppHeader.vue +++ b/frontend/app/components/AppHeader.vue @@ -127,6 +127,21 @@ const initials = computed(() => (user.value?.username.charAt(0) ?? '?').toUpperC {{ t('sidebar.calculator') }} + + + {{ t('sidebar.calculator3d') }} + + + + {{ t('sidebar.lean') }} + +import { expressionToLatex } from '~/utils/plot-expression' +import type { SurfaceFunction } from '~/utils/plot-expression' +import type { SurfaceSeries } from './Scene3D.vue' + +/* The 3D calculator: the space owns the surface, the inputs dock to its + left edge — foldable, so the space can have every pixel. Each field + reads as z = f(x, y), and the surface standing over that ground is + drawn (Scene3D turns it under the hand). A name that is none of x, y, + the constants or the known functions — "k" — is a slider, as on the + plane: a lone "k" or a "k = 2" claims one, and every surface speaking + the name answers to its value. Everything is compiled as it is typed; + one that reads wrong goes red and simply stops being drawn. The + rows, the sliders' values and the dock's fold are the reader's own — + kept between visits and between instances, the way the plane calculator + keeps its own; the two calculators never share rows, only the shapes of + their docks. + The /calculator3d address draws this as the page; the book lays it on + one of its pages (ToolPane), an instance beside the open articles. */ + +interface PlotRow { + id: number + expr: string + color: string + visible: boolean +} + +/* a surface wears one of eight hues, each readable on paper and on slate */ +const PALETTE = [ + '#e5484d', '#0091ff', '#46a758', '#f76808', '#8e4ec6', '#12a594', '#e93d82', '#3e63dd', +] +const STORAGE_KEY = 'mathew-calculator3d-plots' +const VARS_KEY = 'mathew-calculator3d-vars' +const DOCK_KEY = 'mathew-calc3d-dock' +const MAX_ROWS = 12 + +let nextId = 1 +const rows = ref([ + { id: nextId++, expr: 'sin(sqrt(x^2 + y^2))', color: PALETTE[0]!, visible: true }, + { id: nextId++, expr: '(x^2 - y^2) / 4', color: PALETTE[1]!, visible: true }, +]) + +/* one compile pass per render: the rows read alongside what they became — + a surface to draw, a slider to wear, and a reason for the ones that read + wrong (an empty field is nothing asked for, not a mistake). The "z =" + gutter stands only while the field reads as a surface — a slider or + unfinished text wears nothing, and the input takes back the room. One + that reads right carries its LaTeX too: the field echoes it typeset. */ +interface PlotEntry { + row: PlotRow + kind: 'surface' | 'variable' | null + fn: SurfaceFunction | null + // the free variables this row speaks, and the slider its own text claims + vars: string[] + declared: { name: string; value: number | null } | null + error: 'unknown' | 'syntax' | null + tex: string | null +} + +/* the sliders' values, keyed by variable. The compile pass reads them — + which is what ties every drawn surface to every slider: move one, every + expression speaking it recompiles and the space follows. */ +const varValues = reactive>({}) + +const entries = computed(() => { + const scope = { ...varValues } + return rows.value.map((row) => { + const src = row.expr.trim() + if (!src) return { row, kind: null, fn: null, vars: [], declared: null, error: null, tex: null } + const result = compileSurfaceExpression(src, scope) + if (result.ok) + return { + row, + kind: result.kind, + fn: result.kind === 'surface' ? result.fn : null, + vars: result.vars, + declared: result.kind === 'variable' ? { name: result.name, value: result.value } : null, + error: null, + tex: expressionToLatex(src), + } + return { row, kind: null, fn: null, vars: [], declared: null, error: result.reason === 'empty' ? null : result.reason, tex: null } + }) +}) + +/* the sliders: one per variable, hung under the row that claims it — the + declaration row when one asks, else the first row speaking it — values + kept between visits, as the rows are */ +const { slidersByRow, setVar } = useVarSliders( + varValues, + () => entries.value.map((e) => ({ rowId: e.row.id, vars: e.vars, declared: e.declared })), + VARS_KEY, +) + +/* the id of a row's field, so a declaration's inline slider can point back at + it (a label waking its input) to edit "k = 3" again — namespaced per + calculator so an instance of each open in the book never shares an id */ +const INPUT_SCOPE = 'space' +const fieldId = (rowId: number) => `calc-input-${INPUT_SCOPE}-${rowId}` + +/* a row whose own text declared a variable ("k", "k = 3") and whose slider + was anchored here wears that slider in place of its field once the field + rests — the field folds away (see .calc-input-box.var-decl) and the slider + takes the row, so a made variable reads as just a slider, not a "k = 3" + box above a slider */ +function wearsInlineSlider(e: PlotEntry): boolean { + return e.kind === 'variable' && (slidersByRow.value.get(e.row.id)?.length ?? 0) > 0 +} + +const series = computed(() => { + const out: SurfaceSeries[] = [] + for (const e of entries.value) { + if (!e.fn || !e.row.visible) continue + out.push({ id: e.row.id, color: e.row.color, visible: true, fn: e.fn }) + } + return out +}) + +/* a new surface takes the first hue no other row is wearing */ +function nextColor(): string { + const used = new Set(rows.value.map((r) => r.color)) + return PALETTE.find((c) => !used.has(c)) ?? PALETTE[rows.value.length % PALETTE.length]! +} + +function addRow() { + if (rows.value.length >= MAX_ROWS) return + rows.value.push({ id: nextId++, expr: '', color: nextColor(), visible: true }) +} + +function removeRow(id: number) { + rows.value = rows.value.filter((r) => r.id !== id) +} + +function toggleVisible(id: number) { + const row = rows.value.find((r) => r.id === id) + if (row) row.visible = !row.visible +} + +function cycleColor(id: number) { + const row = rows.value.find((r) => r.id === id) + if (!row) return + const at = PALETTE.indexOf(row.color) + row.color = PALETTE[(at + 1) % PALETTE.length]! +} + +/* Enter finishes a line the way clicking away does — it lets go of the field, + so the text settles (a surface folds to its typeset face, a variable to its + slider). On the last line the list invites one more, so the fresh field + takes the caret and the line you confirmed folds away; on any other line, + or once the list is full, Enter simply releases the field. */ +async function onEnter(id: number, ev: KeyboardEvent) { + const el = ev.target as HTMLElement | null + if (id === rows.value[rows.value.length - 1]?.id) { + const before = rows.value.length + addRow() + if (rows.value.length !== before) { + const newId = rows.value[rows.value.length - 1]!.id + await nextTick() + document.getElementById(fieldId(newId))?.focus() + return + } + } + el?.blur() +} + +/* whether the dock stands open is the reader's own — the fold slides the + rows away and leaves the space alone; the choice is kept between visits */ +const dockOpen = ref(true) + +function toggleDock() { + dockOpen.value = !dockOpen.value + try { + localStorage.setItem(DOCK_KEY, dockOpen.value ? '1' : '0') + } catch { + /* private mode etc. — the fold just won't persist */ + } +} + +/* the rows keep themselves between visits */ +function saveRows() { + try { + localStorage.setItem( + STORAGE_KEY, + JSON.stringify(rows.value.map(({ expr, color, visible }) => ({ expr, color, visible }))) + ) + } catch { + /* private mode etc. — the rows just won't persist */ + } +} +watch(rows, saveRows, { deep: true }) + +onMounted(() => { + try { + dockOpen.value = localStorage.getItem(DOCK_KEY) !== '0' + } catch { + /* storage unreadable — the dock stays open */ + } + try { + const raw = localStorage.getItem(STORAGE_KEY) + if (!raw) return + const stored: unknown = JSON.parse(raw) + if (!Array.isArray(stored)) return + const restored: PlotRow[] = [] + for (const item of stored) { + if (typeof item !== 'object' || item === null) continue + const { expr, color, visible } = item as Partial> + restored.push({ + id: nextId++, + expr: typeof expr === 'string' ? expr : '', + color: typeof color === 'string' ? color : PALETTE[restored.length % PALETTE.length]!, + visible: visible !== false, + }) + } + if (restored.length) rows.value = restored.slice(0, MAX_ROWS) + } catch { + /* storage unreadable — the default surfaces stay */ + } +}) + +const { t } = useI18n() + + + diff --git a/frontend/app/components/CalculatorStage.vue b/frontend/app/components/CalculatorStage.vue index 048320f..2af0e86 100644 --- a/frontend/app/components/CalculatorStage.vue +++ b/frontend/app/components/CalculatorStage.vue @@ -1,4 +1,5 @@ + + diff --git a/frontend/app/components/Scene3D.vue b/frontend/app/components/Scene3D.vue new file mode 100644 index 0000000..6c87c6e --- /dev/null +++ b/frontend/app/components/Scene3D.vue @@ -0,0 +1,832 @@ + + + diff --git a/frontend/app/components/SearchModal.vue b/frontend/app/components/SearchModal.vue index 317e217..cdac7c0 100644 --- a/frontend/app/components/SearchModal.vue +++ b/frontend/app/components/SearchModal.vue @@ -5,9 +5,9 @@ import type { ToolPage } from '~/utils/routes' /* Centered search popup: the sidebar and home search bars (or Ctrl/⌘+K, or "/" anywhere but a text field) open it, then it live-searches articles against the API as you type. ↑/↓ select, ↵ opens, esc closes. - The wiki's own pages — the link map and the graphing calculator — answer - the search too, and ↵ on one lays that surface on the book beside the - open articles rather than turning the page away to it. */ + The wiki's own pages — the link map, the graphing calculator, the Lean + editor — answer the search too, and ↵ on one lays that surface on the + book beside the open articles rather than turning the page away to it. */ const api = `${useRuntimeConfig().public.apiBase}/api` const route = useRoute() const router = useRouter() @@ -29,6 +29,14 @@ const PAGE_TOOLS: { tool: ToolPage; terms: string[] }[] = [ tool: 'calculator', terms: ['calculator', 'calc', 'plot', 'plotter', 'graphing', 'plane'], }, + { + tool: 'calculator3d', + terms: ['3d', '3d calculator', 'surface', 'space', 'solid', 'scene'], + }, + { + tool: 'lean', + terms: ['lean', 'lean4', 'lean 4', 'proof', 'prover', 'theorem prover', 'mathlib'], + }, ] const q = ref('') @@ -270,6 +278,10 @@ function highlight(text: string): Part[] { + + + + diff --git a/frontend/app/components/ToolPane.vue b/frontend/app/components/ToolPane.vue index f274baf..05d0fd1 100644 --- a/frontend/app/components/ToolPane.vue +++ b/frontend/app/components/ToolPane.vue @@ -1,7 +1,8 @@ + +
+ +
diff --git a/frontend/app/components/VarSliders.vue b/frontend/app/components/VarSliders.vue new file mode 100644 index 0000000..07c77f6 --- /dev/null +++ b/frontend/app/components/VarSliders.vue @@ -0,0 +1,60 @@ + + + diff --git a/frontend/app/composables/useArticleTabs.ts b/frontend/app/composables/useArticleTabs.ts index 78e3bfd..f905a28 100644 --- a/frontend/app/composables/useArticleTabs.ts +++ b/frontend/app/composables/useArticleTabs.ts @@ -4,8 +4,9 @@ export interface ArticleTab { /** the article this page is of — its canonical slug, and the page's key */ identity: string /** set when the page is one of the wiki's own pages — the link map, the - * graphing calculator — laid on the book instead of an article: the page - * draws that live surface, at its own address, for as long as it is open */ + * graphing calculator, the Lean editor — laid on the book instead of an + * article: the page draws that live surface, at its own address, for as + * long as it is open */ tool?: ToolPage /** the language this page is turned to */ lang: string @@ -24,6 +25,8 @@ const MAX_TABS = 10 export const TOOL_LABEL_KEYS: Record = { graph: 'sidebar.graph', calculator: 'sidebar.calculator', + calculator3d: 'sidebar.calculator3d', + lean: 'sidebar.lean', } /** The key of the book page holding one of the wiki's own pages. No article @@ -123,9 +126,10 @@ export function useArticleTabs() { } /** - * Lay one of the wiki's own pages — the link map, the graphing calculator — - * on the book beside the articles. One surface is one page however many - * times it is asked for: asking again just finds the page already there. + * Lay one of the wiki's own pages — the link map, the graphing calculator, + * the Lean editor — on the book beside the articles. One surface is one + * page however many times it is asked for: asking again just finds the + * page already there. */ function openTool(page: ToolPage) { const identity = toolPageIdentity(page) diff --git a/frontend/app/composables/useLeanSession.ts b/frontend/app/composables/useLeanSession.ts new file mode 100644 index 0000000..318d370 --- /dev/null +++ b/frontend/app/composables/useLeanSession.ts @@ -0,0 +1,287 @@ +/* The wiki's Lean session (client-side). + * + * One websocket to the lean4web server (`/websocket/`), through + * which the wiki plays the part of a Lean editor's language client: open a + * document, send edits, ask for the goal at the cursor (the server's + * `$/lean/plainGoal`), and read the diagnostics — whose severity-3 entries + * are Lean's `#check`/`#eval` style messages, shown in the Messages pane. + * + * The session lives at module scope on purpose: the book may move the Lean + * page between its full-page and pane hosts (unmounting the editor), but a + * running Lean elaboration and its open document are expensive to restart — + * so they outlive the component, and the editor simply re-attaches. */ +import { RpcSocket } from '~/utils/lean/lsp' + +export type LeanPhase = 'idle' | 'connecting' | 'initializing' | 'ready' | 'lost' + +export interface LeanInfoMessage { line: number, text: string } + +/* the shape the Lean server publishes per diagnostic (a slice of LSP) */ +export interface LeanDiagnostic { + range: { start: { line: number, character: number }, end: { line: number, character: number } } + severity?: number + message: string + source?: string +} + +const DOCUMENT_NAME = 'Main.lean' +const FALLBACK_PROJECT = 'MathlibDemo' + +interface LeanSession { + phase: Ref + goals: Ref + messages: Ref + busy: Ref + version: Ref + error: Ref + text: Ref + /* the uri the lean server knows this buffer by — LSP requests must + * name the document the server opened, not the editor's local one */ + serverDocUri: Ref + start: () => Promise + retry: () => void + change: (text: string) => void + cursorAt: (line: number, character: number) => void + request: (method: string, params?: unknown) => Promise + onDiagnostics: (cb: (diags: LeanDiagnostic[]) => void) => () => void +} + +let singleton: LeanSession | null = null + +export function useLeanSession(): LeanSession { + const config = useRuntimeConfig() + const leanUrl = String(config.public.leanUrl || '') + + if (!singleton && import.meta.client && leanUrl) singleton = createSession(leanUrl) + + /* a dormant stand-in keeps the component honest on the server, where + * there is nothing to speak to */ + return singleton ?? { + phase: ref('idle') as Ref, + goals: ref([]) as Ref, + messages: ref([]) as Ref, + busy: ref(false) as Ref, + version: ref(null) as Ref, + error: ref(null) as Ref, + text: ref('') as Ref, + serverDocUri: ref('') as Ref, + start: async () => {}, + retry: () => {}, + change: () => {}, + cursorAt: () => {}, + request: async () => { throw new Error('no lean session') }, + onDiagnostics: () => () => {}, + } +} + +function createSession(leanUrl: string): LeanSession { + const phase = ref('idle') + const goals = ref([]) + const messages = ref([]) + const busy = ref(false) + const version = ref(null) + const error = ref(null) + const text = ref('') + const serverDocUri = ref('') + + let rpc: RpcSocket | null = null + let docUri = `${FALLBACK_PROJECT}/${DOCUMENT_NAME}` + let sentVersion = 0 + let lastSentText = '' + const cursor = { line: 0, character: 0 } + const diagListeners = new Set<(diags: LeanDiagnostic[]) => void>() + let lastDiags: LeanDiagnostic[] = [] + + let changeTimer: ReturnType | undefined + let goalTimer: ReturnType | undefined + + const wsBase = leanUrl.replace(/\/+$/, '').replace(/^http/, 'ws') + + async function pickProject(): Promise { + try { + // the server's REST endpoints carry no CORS headers — probing them from + // another origin only earns a blocked request, so stay quiet cross-origin + // and name the canonical project (the websocket is CORS-free) + if (new URL(leanUrl, window.location.href).origin !== window.location.origin) { + return FALLBACK_PROJECT + } + const res = await fetch(`${leanUrl.replace(/\/+$/, '')}/api/projects`) + const projects = (await res.json()) as Array<{ folder: string, config?: { default?: boolean, hidden?: boolean } }> + const visible = projects.filter(p => !p.config?.hidden) + return (visible.find(p => p.config?.default) ?? visible[0])?.folder || FALLBACK_PROJECT + } + catch { return FALLBACK_PROJECT } + } + + function handleNotification(method: string, params: unknown) { + const p = params as Record | undefined + if (method === '$/lean/fileProgress') { + busy.value = Array.isArray(p?.processing) && p.processing.length > 0 + return + } + if (method === 'textDocument/publishDiagnostics') { + const raw = Array.isArray(p?.diagnostics) ? p.diagnostics as LeanDiagnostic[] : [] + // the server marks some diagnostics silent (elaboration noise); the + // wiki shows errors/warnings in the editor, info in the Messages pane + const diags = raw.filter(d => !('isSilent' in d && (d as any).isSilent)) + lastDiags = diags + messages.value = diags + .filter(d => d.severity === 3) + .map(d => ({ line: d.range.start.line + 1, text: d.message })) + for (const cb of diagListeners) cb(diags) + } + } + + async function connect() { + phase.value = 'connecting' + error.value = null + const project = await pickProject() + docUri = `${project}/${DOCUMENT_NAME}` + // a fresh document identity means the buffer below re-sends as new + sentVersion = 0 + lastSentText = '' + + try { + rpc = new RpcSocket(`${wsBase}/websocket/${project}`, { + onNotification: handleNotification, + onClose: () => { + if (phase.value !== 'idle' && phase.value !== 'lost') { + phase.value = 'lost' + busy.value = false + } + }, + }) + await rpc.whenOpen + + phase.value = 'initializing' + const init = await rpc.request<{ + serverInfo?: { name?: string, version?: string } + }>('initialize', { + processId: null, + clientInfo: { name: 'mathew', version: '0.1.0' }, + rootUri: '', + capabilities: { + general: { positionEncodings: ['utf-16'] }, + workspace: { configuration: false, workspaceFolders: false, applyEdit: true }, + window: { + showMessage: {}, + showDocument: { support: true }, + workDoneProgress: true, + configuration: true, + }, + textDocument: { + synchronization: { didChange: true, willSave: false, didSave: false }, + publishDiagnostics: { relatedInformation: true, versionSupport: true }, + hover: { contentFormat: ['markdown', 'plaintext'] }, + definition: { linkSupport: true }, + documentHighlight: {}, + completion: { + completionItem: { + snippetSupport: true, + documentationFormat: ['markdown', 'plaintext'], + insertTextFormat: { valueSet: [1, 2] }, + additionalTextEditsSupport: true, + }, + contextSupport: true, + }, + }, + }, + initializationOptions: { hasWidgets: true }, + }) + version.value = init.serverInfo?.version ?? null + rpc.notify('initialized', {}) + rpc.notify('textDocument/didOpen', { + textDocument: { uri: docUri, languageId: 'lean4', version: 1, text: text.value }, + }) + sentVersion = 1 + lastSentText = text.value + phase.value = 'ready' + void refreshGoal() + } + catch (err) { + error.value = err instanceof Error ? err.message : String(err) + phase.value = 'lost' + } + } + + async function refreshGoal() { + if (!rpc || phase.value !== 'ready') return + try { + const res = await rpc.request<{ goals?: string[], rendered?: string } | null>( + '$/lean/plainGoal', + { textDocument: { uri: docUri }, position: cursor }, + ) + // the server answers `null` away from tactic goals; `rendered` is the + // goals as a markdown fence — the array is the honest plain text + goals.value = res?.goals ?? [] + } + catch { /* raced by a newer edit (ContentModified) — the next ask wins */ } + } + + function sendChange() { + if (!rpc || phase.value !== 'ready' || text.value === lastSentText) return + sentVersion += 1 + // LSP allows one change spanning the whole document — simple and exact + const endLine = Math.max(lastSentText.split('\n').length - 1, 0) + const endChar = lastSentText.slice(lastSentText.lastIndexOf('\n') + 1).length + rpc.notify('textDocument/didChange', { + textDocument: { uri: docUri, version: sentVersion }, + contentChanges: [{ + range: { start: { line: 0, character: 0 }, end: { line: endLine, character: endChar } }, + text: text.value, + }], + }) + lastSentText = text.value + void refreshGoal() + } + + return { + phase, + goals, + messages, + busy, + version, + error, + text, + + async start() { + if (phase.value !== 'idle') return + await connect() + }, + + retry() { + try { rpc?.close() } + catch { /* gone */ } + rpc = null + goals.value = [] + messages.value = [] + busy.value = false + void connect() + }, + + change(newText) { + text.value = newText + clearTimeout(changeTimer) + changeTimer = setTimeout(sendChange, 400) + }, + + cursorAt(line, character) { + cursor.line = line + cursor.character = character + clearTimeout(goalTimer) + goalTimer = setTimeout(() => void refreshGoal(), 200) + }, + + request(method: string, params?: unknown) { + if (!rpc || phase.value !== 'ready') return Promise.reject(new Error('lean is not ready')) + return rpc.request(method, params) + }, + + onDiagnostics(cb) { + diagListeners.add(cb) + // a freshly (re)attached editor wants the current marks at once + cb(lastDiags) + return () => diagListeners.delete(cb) + }, + } +} diff --git a/frontend/app/composables/useVarSliders.ts b/frontend/app/composables/useVarSliders.ts new file mode 100644 index 0000000..db1dc54 --- /dev/null +++ b/frontend/app/composables/useVarSliders.ts @@ -0,0 +1,119 @@ +/* The free-variable sliders both calculators wear: one value per variable + in a scope the compile pass reads, one slider per variable anchored under + the row that claims it — the row declaring it ("k", "k = 2") when one + asks, else the first row speaking it — and the values kept between visits + per calculator. A name the scope does not carry yet reads as 1, where + every slider starts. */ + +export interface VarSlider { + name: string + value: number + min: number + max: number +} + +/* one row's reading, as far as sliders care: the variables it speaks and + the declaration its text claims (a null start says "k", not "k = 2") */ +export interface RowVarDecls { + rowId: number + vars: string[] + declared: { name: string; value: number | null } | null +} + +/* how far a slider reaches either side of zero; a value set past an end — + by "k = 40" or by typing — pulls that end out so the thumb can reach it */ +const SLIDER_MIN = -10 +const SLIDER_MAX = 10 + +export function useVarSliders( + varValues: Record, + decls: () => RowVarDecls[], + storageKey: string, +) { + /* every variable spoken, with the value its "k = 2" row asks to start at + — or 1, where sliders start. One variable wears one slider however many + rows speak it. */ + const varStarts = computed(() => { + const starts = new Map() + for (const d of decls()) { + if (d.declared && !starts.has(d.declared.name)) starts.set(d.declared.name, d.declared.value ?? 1) + for (const name of d.vars) if (!starts.has(name)) starts.set(name, 1) + } + return starts + }) + + // a variable the rows only now started speaking takes its start value; + // one the reader already moved keeps the value they left it at. Filling + // from the first pass keeps what the server draws and what the reader + // finds after mounting the same + function fillDefaults() { + for (const [name, value] of varStarts.value) { + if (!(name in varValues)) varValues[name] = value + } + } + watch(varStarts, fillDefaults, { immediate: true }) + + /* one slider per variable, filed under the row it sits beneath: the row + claiming it ("k", "k = 2") wins, else the first row that speaks it */ + const slidersByRow = computed(() => { + const anchor = new Map() + for (const d of decls()) { + if (d.declared && !anchor.has(d.declared.name)) anchor.set(d.declared.name, d.rowId) + } + for (const d of decls()) { + for (const name of d.vars) { + if (!anchor.has(name)) anchor.set(name, d.rowId) + } + } + const byRow = new Map() + for (const d of decls()) { + for (const name of d.vars) { + if (anchor.get(name) !== d.rowId) continue + const value = varValues[name] ?? 1 + const list = byRow.get(d.rowId) ?? [] + list.push({ name, value, min: Math.min(SLIDER_MIN, value), max: Math.max(SLIDER_MAX, value) }) + byRow.set(d.rowId, list) + } + } + return byRow + }) + + function setVar(name: string, raw: number) { + if (Number.isFinite(raw)) varValues[name] = raw + } + + /* the values keep themselves — only the ones a row still speaks, so a + variable nobody asks for anymore is forgotten on the next save rather + than haunting the store */ + function save() { + try { + const kept: Record = {} + for (const [name, value] of Object.entries(varValues)) { + if (varStarts.value.has(name) && Number.isFinite(value)) kept[name] = value + } + localStorage.setItem(storageKey, JSON.stringify(kept)) + } catch { + /* private mode etc. — the slider values just won't persist */ + } + } + watch([varValues, varStarts], save) + + onMounted(() => { + try { + const raw = localStorage.getItem(storageKey) + if (raw) { + const stored: unknown = JSON.parse(raw) + if (typeof stored === 'object' && stored !== null) { + for (const [name, value] of Object.entries(stored)) { + if (typeof value === 'number' && Number.isFinite(value)) varValues[name] = value + } + } + } + } catch { + /* storage unreadable — the sliders start where their rows ask */ + } + fillDefaults() + }) + + return { slidersByRow, setVar } +} diff --git a/frontend/app/pages/calculator3d.vue b/frontend/app/pages/calculator3d.vue new file mode 100644 index 0000000..7b9843c --- /dev/null +++ b/frontend/app/pages/calculator3d.vue @@ -0,0 +1,24 @@ + + + diff --git a/frontend/app/pages/lean.vue b/frontend/app/pages/lean.vue new file mode 100644 index 0000000..5006f48 --- /dev/null +++ b/frontend/app/pages/lean.vue @@ -0,0 +1,25 @@ + + + diff --git a/frontend/app/utils/lean/abbreviations.ts b/frontend/app/utils/lean/abbreviations.ts new file mode 100644 index 0000000..5d4a3a9 --- /dev/null +++ b/frontend/app/utils/lean/abbreviations.ts @@ -0,0 +1,4 @@ +/* Lean's unicode input table (the `\le` → `≤` abbreviations), from + * vscode-lean4 (MIT, leanprover-community/vscode-lean4, `lean4-unicode-input`). + * Each value may carry `$CURSOR` where the caret lands after the replacement. */ +export const leanAbbreviations: Record = {"!": "¬", "!!": "‼", "!?": "⁉", "\"A": "Ä", "\"E": "Ë", "\"I": "Ï", "\"O": "Ö", "\"U": "Ü", "\"a": "ä", "\"e": "ë", "\"i": "ï", "\"o": "ö", "\"u": "ü", "\"y": "ÿ", "#": "♯", "&": "⅋", "'A": "Á", "'E": "É", "'I": "Í", "'O": "Ó", "'U": "Ú", "'Y": "Ý", "'a": "á", "'e": "é", "'i": "í", "'o": "ó", "'u": "ú", "'y": "ý", "((": "⸨", "(())": "⸨$CURSOR⸩", "()": "($CURSOR)", "()_": "($CURSOR)_", "(=": "≘", "([": "⟮", "([])'": "⟮$CURSOR⟯", "(b": "⟅", "))": "⸩", ")b": "⟆", "*": "⋆", "*=": "≛", "+ ": "⊹", "-": "⁻¹", "---": "─", "--.": "╌", "--=": "═", "-->": "⟶", "--_": "━", "-1": "⁻¹", "-2": "⁻²", "-3": "⁻³", "-:": "∹", "->": "→", "->n": "↛", "-]": "⁆", "-int": "⨍", "-o": "⊸", "-{A}": "Ā", "-{E}": "Ē", "-{I}": "Ī", "-{O}": "Ō", "-{U}": "Ū", "-{a}": "ā", "-{e}": "ē", "-{i}": "ī", "-{o}": "ō", "-{u}": "ū", "-|": "⊣", "-~": "≂", ".": "·", ".+": "∔", ".-": "∸", "...": "⋯", ".=": "≐", ".=.": "≑", "/": "⧸", "/L": "Ł", "/O": "Ø", "/o": "ø", "0": "₀", "1": "₁", "2": "₂", "3": "₃", "4": "₄", "5": "₅", "6": "₆", "7": "₇", "8": "₈", "9": "₉", ":": "∶", "::": "∷", "::-": "∺", ":=": "≔", ":>": "⋗", ":~": "∻", "<": "⟨", "<-": "←", "<--": "⟵", "<-->": "⟷", "<->": "↔", "<->n": "↮", "<-n": "↚", "<:": "⋖", "<<": "⟪", "<=": "≤", "<=>": "⇔", "<=>n": "⇎", "<=n": "≰", "<>": "⟨$CURSOR⟩", "<|": "⧏", "<~": "≲", "<~n": "⋦", "<~nn": "≴", "=:": "≕", "==": "≡", "===": "≣", "==>": "⟹", "==n": "≢", "=>": "⇒", "=>n": "⇏", "=n": "≠", "=o": "≗", ">": "⟩", ">=": "≥", ">=n": "≱", ">>": "⟫", ">n": "≯", ">~": "≳", ">~n": "⋧", ">~nn": "≵", "?": "¿", "?!": "‽", "?=": "≟", "??": "⁇", "A": "𝔸", "AA": "Å", "AE": "Æ", "Alpha": "Α", "And": "⋀", "Beta": "Β", "Box": "□", "Bumpeq": "≎", "C": "ℂ", "Cap": "⋒", "Chi": "Χ", "Com": "ℂ", "Complement": "∁", "Cup": "⋓", "D": "Δ", "DH": "Ð", "Dei": "Ϯ", "Delta": "Δ", "Diamond": "◇", "Digamma": "Ϝ", "Downarrow": "⇓", "Epsilon": "Ε", "Eta": "Η", "F": "𝔽", "Fei": "Ϥ", "Frowny": "☹", "G": "Γ", "GA": "Α", "GB": "Β", "GC": "Χ", "GD": "Δ", "GE": "Ε", "GF": "Φ", "GG": "Γ", "GI": "Ι", "GK": "Κ", "GL": "Λ", "GM": "Μ", "GN": "Ν", "GO": "Ω", "GP": "Ψ", "GR": "Ρ", "GS": "Σ", "GT": "Τ", "GTH": "Θ", "GU": "Υ", "GX": "Ξ", "GZ": "Ζ", "Ga": "α", "Gamma": "Γ", "Gangia": "Ϫ", "Gb": "β", "Gc": "χ", "Gd": "δ", "Ge": "ε", "Gf": "φ", "Gg": "γ", "Gi": "ι", "Gk": "κ", "Gl": "λ", "Gl-": "ƛ", "Glb": "⨅", "Gm": "μ", "Gn": "ν", "Go": "ω", "Gp": "ψ", "Gr": "ρ", "Gs": "σ", "Gt": "τ", "Gth": "θ", "Gu": "υ", "Gx": "ξ", "Gz": "ζ", "H": "ℍ", "Heta": "Ͱ", "Hori": "Ϩ", "I": "⋂", "I0": "⋂₀", "Im": "ℑ", "Inf": "⨅", "Int": "ℤ", "Inter": "⋂", "Iota": "Ι", "Join": "⨆", "K": "𝕂", "Kappa": "Κ", "Khei": "Ϧ", "Koppa": "Ϟ", "L": "Λ", "Lambda": "Λ", "Lamda": "Λ", "Leftarrow": "⇐", "Leftrightarrow": "⇔", "Letter": "✉", "Ll": "⋘", "Lleftarrow": "⇚", "Longleftarrow": "⇐", "Longleftrightarrow": "⇔", "Longrightarrow": "⇒", "Lsh": "↰", "Lub": "⨆", "MCA": "𝓐", "MCB": "𝓑", "MCC": "𝓒", "MCD": "𝓓", "MCE": "𝓔", "MCF": "𝓕", "MCG": "𝓖", "MCH": "𝓗", "MCI": "𝓘", "MCJ": "𝓙", "MCK": "𝓚", "MCL": "𝓛", "MCM": "𝓜", "MCN": "𝓝", "MCO": "𝓞", "MCP": "𝓟", "MCQ": "𝓠", "MCR": "𝓡", "MCS": "𝓢", "MCT": "𝓣", "MCU": "𝓤", "MCV": "𝓥", "MCW": "𝓦", "MCX": "𝓧", "MCY": "𝓨", "MCZ": "𝓩", "MCa": "𝓪", "MCb": "𝓫", "MCc": "𝓬", "MCd": "𝓭", "MCe": "𝓮", "MCf": "𝓯", "MCg": "𝓰", "MCh": "𝓱", "MCi": "𝓲", "MCj": "𝓳", "MCk": "𝓴", "MCl": "𝓵", "MCm": "𝓶", "MCn": "𝓷", "MCo": "𝓸", "MCp": "𝓹", "MCq": "𝓺", "MCr": "𝓻", "MCs": "𝓼", "MCt": "𝓽", "MCu": "𝓾", "MCv": "𝓿", "MCw": "𝔀", "MCx": "𝔁", "MCy": "𝔂", "MCz": "𝔃", "MIA": "𝑨", "MIB": "𝑩", "MIC": "𝑪", "MID": "𝑫", "MIE": "𝑬", "MIF": "𝑭", "MIG": "𝑮", "MIH": "𝑯", "MII": "𝑰", "MIJ": "𝑱", "MIK": "𝑲", "MIL": "𝑳", "MIM": "𝑴", "MIN": "𝑵", "MIO": "𝑶", "MIP": "𝑷", "MIQ": "𝑸", "MIR": "𝑹", "MIS": "𝑺", "MIT": "𝑻", "MIU": "𝑼", "MIV": "𝑽", "MIW": "𝑾", "MIX": "𝑿", "MIY": "𝒀", "MIZ": "𝒁", "MIa": "𝒂", "MIb": "𝒃", "MIc": "𝒄", "MId": "𝒅", "MIe": "𝒆", "MIf": "𝒇", "MIg": "𝒈", "MIh": "𝒉", "MIi": "𝒊", "MIj": "𝒋", "MIk": "𝒌", "MIl": "𝒍", "MIm": "𝒎", "MIn": "𝒏", "MIo": "𝒐", "MIp": "𝒑", "MIq": "𝒒", "MIr": "𝒓", "MIs": "𝒔", "MIt": "𝒕", "MIu": "𝒖", "MIv": "𝒗", "MIw": "𝒘", "MIx": "𝒙", "MIy": "𝒚", "MIz": "𝒛", "McA": "𝒜", "McB": "ℬ", "McC": "𝒞", "McD": "𝒟", "McE": "ℰ", "McF": "ℱ", "McG": "𝒢", "McH": "ℋ", "McI": "ℐ", "McJ": "𝒥", "McK": "𝒦", "McL": "ℒ", "McM": "ℳ", "McN": "𝒩", "McO": "𝒪", "McP": "𝒫", "McQ": "𝒬", "McR": "ℛ", "McS": "𝒮", "McT": "𝒯", "McU": "𝒰", "McV": "𝒱", "McW": "𝒲", "McX": "𝒳", "McY": "𝒴", "McZ": "𝒵", "Mca": "𝒶", "Mcb": "𝒷", "Mcc": "𝒸", "Mcd": "𝒹", "Mce": "ℯ", "Mcf": "𝒻", "Mcg": "ℊ", "Mch": "𝒽", "Mci": "𝒾", "Mcj": "𝒿", "Mck": "𝓀", "Mcl": "𝓁", "Mcm": "𝓂", "Mcn": "𝓃", "Mco": "ℴ", "Mcp": "𝓅", "Mcq": "𝓆", "Mcr": "𝓇", "Mcs": "𝓈", "Mct": "𝓉", "Mcu": "𝓊", "Mcv": "𝓋", "Mcw": "𝓌", "Mcx": "𝓍", "Mcy": "𝓎", "Mcz": "𝓏", "Meet": "⨅", "MfA": "𝔄", "MfB": "𝔅", "MfC": "ℭ", "MfD": "𝔇", "MfE": "𝔈", "MfF": "𝔉", "MfG": "𝔊", "MfH": "ℌ", "MfI": "ℑ", "MfJ": "𝔍", "MfK": "𝔎", "MfL": "𝔏", "MfM": "𝔐", "MfN": "𝔑", "MfO": "𝔒", "MfP": "𝔓", "MfQ": "𝔔", "MfR": "ℜ", "MfS": "𝔖", "MfT": "𝔗", "MfU": "𝔘", "MfV": "𝔙", "MfW": "𝔚", "MfX": "𝔛", "MfY": "𝔜", "MfZ": "ℨ", "Mfa": "𝔞", "Mfb": "𝔟", "Mfc": "𝔠", "Mfd": "𝔡", "Mfe": "𝔢", "Mff": "𝔣", "Mfg": "𝔤", "Mfh": "𝔥", "Mfi": "𝔦", "Mfj": "𝔧", "Mfk": "𝔨", "Mfl": "𝔩", "Mfm": "𝔪", "Mfn": "𝔫", "Mfo": "𝔬", "Mfp": "𝔭", "Mfq": "𝔮", "Mfr": "𝔯", "Mfs": "𝔰", "Mft": "𝔱", "Mfu": "𝔲", "Mfv": "𝔳", "Mfw": "𝔴", "Mfx": "𝔵", "Mfy": "𝔶", "Mfz": "𝔷", "MiA": "𝐴", "MiB": "𝐵", "MiC": "𝐶", "MiD": "𝐷", "MiE": "𝐸", "MiF": "𝐹", "MiG": "𝐺", "MiH": "𝐻", "MiI": "𝐼", "MiJ": "𝐽", "MiK": "𝐾", "MiL": "𝐿", "MiM": "𝑀", "MiN": "𝑁", "MiO": "𝑂", "MiP": "𝑃", "MiQ": "𝑄", "MiR": "𝑅", "MiS": "𝑆", "MiT": "𝑇", "MiU": "𝑈", "MiV": "𝑉", "MiW": "𝑊", "MiX": "𝑋", "MiY": "𝑌", "MiZ": "𝑍", "Mia": "𝑎", "Mib": "𝑏", "Mic": "𝑐", "Mid": "𝑑", "Mie": "𝑒", "Mif": "𝑓", "Mig": "𝑔", "Mii": "𝑖", "Mij": "𝑗", "Mik": "𝑘", "Mil": "𝑙", "Mim": "𝑚", "Min": "𝑛", "Mio": "𝑜", "Mip": "𝑝", "Miq": "𝑞", "Mir": "𝑟", "Mis": "𝑠", "Mit": "𝑡", "Miu": "𝑢", "Miv": "𝑣", "Miw": "𝑤", "Mix": "𝑥", "Miy": "𝑦", "Miz": "𝑧", "N": "ℕ", "Nat": "ℕ", "Nu": "Ν", "O": "Ø", "O*": "⍟", "O+": "⨁", "O.": "⨀", "OE": "Œ", "Omega": "Ω", "Omicron": "Ο", "Or": "⋁", "Ox": "⨂", "P": "Π", "P0": "Π₀", "P_0": "Π₀", "Phi": "Φ", "Pi": "Π", "Pi0": "Π₀", "Pi_0": "Π₀", "Psi": "Ψ", "Q": "ℚ", "R": "ℝ", "R>=0": "ℝ≥0", "Rat": "ℚ", "Re": "ℜ", "Real": "ℝ", "Rge0": "ℝ≥0", "Rho": "Ρ", "Rightarrow": "⇒", "Rrightarrow": "⇛", "Rsh": "↱", "S": "Σ", "Sampi": "Ϡ", "San": "Ϻ", "Shei": "Ϣ", "Shima": "Ϭ", "Sho": "Ϸ", "Sigma": "Σ", "Smiley": "☺", "Sqcap": "⨅", "Sqcup": "⨆", "Stigma": "Ϛ", "Subset": "⋐", "Sup": "⨆", "Supset": "⋑", "TH": "Þ", "Tau": "Τ", "Tb": "◀", "Theta": "Θ", "Tr": "◀", "Tw": "◁", "U": "⋃", "U+": "⨄", "U.": "⨃", "U0": "⋃₀", "Un": "⋃", "Union": "⋃", "Uparrow": "⇑", "Updownarrow": "⇕", "Upsilon": "Υ", "Vdash": "⊩", "Vert": "‖", "Vvdash": "⊪", "X": "⨯", "Xi": "Ξ", "Yot": "Ϳ", "Z": "ℤ", "Zeta": "Ζ", "Zsqrt": "ℤ√", "[-": "⁅", "[--]": "⁅$CURSOR⁆", "[[": "⟦", "[[]]": "⟦$CURSOR⟧", "[]": "[$CURSOR]", "[]_": "[$CURSOR]_", "\\": "\\", "])": "⟯", "]]": "⟧", "^(": "⁽", "^)": "⁾", "^+": "⁺", "^-": "⁻", "^-1": "⁻¹", "^0": "⁰", "^1": "¹", "^2": "²", "^3": "³", "^4": "⁴", "^5": "⁵", "^6": "⁶", "^7": "⁷", "^8": "⁸", "^9": "⁹", "^=": "⁼", "^A": "ᴬ", "^Ae": "ᴭ", "^B": "ᴮ", "^Bbarred": "ᴯ", "^D": "ᴰ", "^E": "ᴱ", "^Ereversed": "ᴲ", "^G": "ᴳ", "^H": "ᴴ", "^Hstroke": "ꟸ", "^I": "ᴵ", "^Ismall": "ᶦ", "^Istroke": "ᶧ", "^J": "ᴶ", "^K": "ᴷ", "^L": "ᴸ", "^Lsmall": "ᶫ", "^M": "ᴹ", "^N": "ᴺ", "^Nreversed": "ᴻ", "^Nsmall": "ᶰ", "^O": "ᴼ", "^Ou": "ᴽ", "^P": "ᴾ", "^R": "ᴿ", "^Rinverted": "ʶ", "^SM": "℠", "^T": "ᵀ", "^TEL": "℡", "^TM": "™", "^U": "ᵁ", "^Usmall": "ᶸ", "^V": "ⱽ", "^W": "ᵂ", "^a": "ᵃ", "^a_": "ª", "^ain": "ᵜ", "^alpha": "ᵅ", "^b": "ᵇ", "^beta": "ᵝ", "^bot": "ᗮ", "^c": "ᶜ", "^ccurl": "ᶝ", "^chi": "ᵡ", "^d": "ᵈ", "^e": "ᵉ", "^eng": "ᵑ", "^eopen": "ᵋ", "^ereversedopen": "ᶟ", "^esh": "ᶴ", "^eth": "ᶞ", "^ezh": "ᶾ", "^f": "ᶠ", "^g": "ᵍ", "^gamma": "ˠ", "^gscript": "ᶢ", "^h": "ʰ", "^heng": "ꭜ", "^hhook": "ʱ", "^hwithhook": "ʱ", "^i": "ⁱ", "^iota": "ᶥ", "^istroke": "ᶤ", "^j": "ʲ", "^jtail": "ᶨ", "^k": "ᵏ", "^l": "ˡ", "^lhook": "ᶪ", "^lretroflexhook": "ᶩ", "^ls": "ꭝ", "^ltilde": "ꭞ", "^m": "ᵐ", "^mhook": "ᶬ", "^n": "ⁿ", "^nlefthook": "ᶮ", "^nretroflexhook": "ᶯ", "^o": "ᵒ", "^o_": "º", "^obarred": "ᶱ", "^obottom": "ᵕ", "^oe": "ꟹ", "^oopen": "ᵓ", "^otop": "ᵔ", "^p": "ᵖ", "^perp": "ᗮ", "^phi": "ᶲ", "^r": "ʳ", "^s": "ˢ", "^schwa": "ᵊ", "^shook": "ᶳ", "^stop": "ˤ", "^t": "ᵗ", "^theta": "ᶿ", "^turneda": "ᵄ", "^turnedae": "ᵆ", "^turnedalpha": "ᶛ", "^turnede": "ᵌ", "^turnedh": "ᶣ", "^turnedi": "ᵎ", "^turnedm": "ᵚ", "^turnedmleg": "ᶭ", "^turnedr": "ʴ", "^turnedrhook": "ʵ", "^turnedrwithhook": "ʵ", "^turnedv": "ᶺ", "^twithpalatalhook": "ᶵ", "^u": "ᵘ", "^ubar": "ᶶ", "^uhook": "ꭟ", "^upsilon": "ᶷ", "^usideways": "ᵙ", "^v": "ᵛ", "^vargamma": "ᵞ", "^varphi": "ᵠ", "^vhook": "ᶹ", "^w": "ʷ", "^x": "ˣ", "^y": "ʸ", "^z": "ᶻ", "^zcurl": "ᶽ", "^zretroflexhook": "ᶼ", "^{A}": "Â", "^{E}": "Ê", "^{I}": "Î", "^{O}": "Ô", "^{U}": "Û", "^{a}": "â", "^{e}": "ê", "^{i}": "î", "^{o}": "ô", "^{u}": "û", "_(": "₍", "_)": "₎", "_+": "₊", "_-": "₋", "_--": "̲", "_0": "₀", "_1": "₁", "_2": "₂", "_3": "₃", "_4": "₄", "_5": "₅", "_6": "₆", "_7": "₇", "_8": "₈", "_9": "₉", "_=": "₌", "_a": "ₐ", "_e": "ₑ", "_h": "ₕ", "_i": "ᵢ", "_j": "ⱼ", "_k": "ₖ", "_l": "ₗ", "_m": "ₘ", "_n": "ₙ", "_o": "ₒ", "_p": "ₚ", "_r": "ᵣ", "_s": "ₛ", "_t": "ₜ", "_u": "ᵤ", "_v": "ᵥ", "_x": "ₓ", "`A": "À", "`E": "È", "`I": "Ì", "`O": "Ò", "`U": "Ù", "`a": "à", "`e": "è", "`i": "ì", "`o": "ò", "`u": "ù", "a": "α", "aa": "å", "addopposite": "ᵃᵒᵖ", "ae": "æ", "aeeqfun": "→ₘ", "afghani": "؋", "aleph": "ℵ", "aleph0": "ℵ₀", "alghom": "→ₐ", "all": "∀", "all^f": "∀ᶠ", "all^m": "∀ᵐ", "allf": "∀ᶠ", "allm": "∀ᵐ", "alpha": "α", "amalg": "∐", "an": "∧", "and": "∧", "and=": "≙", "angle": "∠", "angstrom": "Å", "aop": "ᵃᵒᵖ", "apl": "⌶", "approx": "≈", "approxeq": "≊", "ast": "∗", "asterisk": "⁎", "asymp": "≍", "austral": "₳", "average": "⨍", "b": "β", "b+": "⊞", "b-": "⊟", "b.": "⊡", "b0": "𝟘", "b1": "𝟙", "b2": "𝟚", "b3": "𝟛", "b4": "𝟜", "b5": "𝟝", "b6": "𝟞", "b7": "𝟟", "b8": "𝟠", "b9": "𝟡", "bInter": "⋂", "bUnion": "⋃", "backcong": "≌", "backepsilon": "∍", "backprime": "‵", "backsim": "∽", "backsimeq": "⋍", "barwedge": "⊼", "bb": "𝔹", "bbA": "𝔸", "bbB": "𝔹", "bbC": "ℂ", "bbD": "𝔻", "bbE": "𝔼", "bbF": "𝔽", "bbG": "𝔾", "bbH": "ℍ", "bbI": "𝕀", "bbJ": "𝕁", "bbK": "𝕂", "bbL": "𝕃", "bbM": "𝕄", "bbN": "ℕ", "bbO": "𝕆", "bbP": "ℙ", "bbQ": "ℚ", "bbR": "ℝ", "bbS": "𝕊", "bbT": "𝕋", "bbU": "𝕌", "bbV": "𝕍", "bbW": "𝕎", "bbX": "𝕏", "bbY": "𝕐", "bbZ": "ℤ", "bba": "𝕒", "bbb": "𝕓", "bbc": "𝕔", "bbd": "𝕕", "bbe": "𝕖", "bbf": "𝕗", "bbg": "𝕘", "bbh": "𝕙", "bbi": "𝕚", "bbj": "𝕛", "bbk": "𝕜", "bbl": "𝕝", "bbm": "𝕞", "bbn": "𝕟", "bbo": "𝕠", "bbp": "𝕡", "bbq": "𝕢", "bbr": "𝕣", "bbs": "𝕤", "bbt": "𝕥", "bbu": "𝕦", "bbv": "𝕧", "bbw": "𝕨", "bbx": "𝕩", "bby": "𝕪", "bbz": "𝕫", "bc": "ℂ", "be": "β", "because": "∵", "beta": "β", "beth": "ℶ", "between": "≬", "bfA": "𝐀", "bfB": "𝐁", "bfC": "𝐂", "bfD": "𝐃", "bfE": "𝐄", "bfF": "𝐅", "bfG": "𝐆", "bfH": "𝐇", "bfI": "𝐈", "bfJ": "𝐉", "bfK": "𝐊", "bfL": "𝐋", "bfM": "𝐌", "bfN": "𝐍", "bfO": "𝐎", "bfP": "𝐏", "bfQ": "𝐐", "bfR": "𝐑", "bfS": "𝐒", "bfT": "𝐓", "bfU": "𝐔", "bfV": "𝐕", "bfW": "𝐖", "bfX": "𝐗", "bfY": "𝐘", "bfZ": "𝐙", "bfa": "𝐚", "bfb": "𝐛", "bfc": "𝐜", "bfd": "𝐝", "bfe": "𝐞", "bff": "𝐟", "bfg": "𝐠", "bfh": "𝐡", "bfi": "𝐢", "bfj": "𝐣", "bfk": "𝐤", "bfl": "𝐥", "bfm": "𝐦", "bfn": "𝐧", "bfo": "𝐨", "bfp": "𝐩", "bfq": "𝐪", "bfr": "𝐫", "bfs": "𝐬", "bft": "𝐭", "bfu": "𝐮", "bfv": "𝐯", "bfw": "𝐰", "bfx": "𝐱", "bfy": "𝐲", "bfz": "𝐳", "bigcap": "⋂", "bigcirc": "◯", "bigcoprod": "∐", "bigcup": "⋃", "bigglb": "⨅", "biginf": "⨅", "bigjoin": "⨆", "biglub": "⨆", "bigmeet": "⨅", "bigsolidus": "⧸", "bigsqcap": "⨅", "bigsqcup": "⨆", "bigstar": "★", "bigsup": "⨆", "bigtriangledown": "▽", "bigtriangleup": "△", "bigvee": "⋁", "bigwedge": "⋀", "bihimp": "⇔", "biohazard": "☣", "blacklozenge": "✦", "blacksmiley": "☻", "blacksquare": "▪", "blacktriangle": "▴", "blacktriangledown": "▾", "blacktriangleleft": "◂", "blacktriangleright": "▸", "bn": "ℕ", "bot": "⊥", "boundedcontinuousfunction": "→ᵇ", "bowtie": "⋈", "boxmid": "◫", "boxminus": "⊟", "boxplus": "⊞", "boxtimes": "⊠", "bp": "ℙ", "bq": "ℚ", "br": "ℝ", "bracketl": "⁅", "bracketr": "⁆", "brokenbar": "¦", "bsum": "⅀", "bu": "•", "bub": "•", "bumpeq": "≏", "but": "‣", "buw": "◦", "bx": "⊠", "bz": "ℤ", "c": "χ", "cC": "Ç", "cap": "∩", "caution": "☡", "cc": "ç", "cdot": "·", "cdots": "⋯", "ce": "ȩ", "cedi": "₵", "ceil": "⌈$CURSOR⌉", "celsius": "℃", "cent": "¢", "centerdot": "·", "ch": "χ", "checkmark": "✓", "chi": "χ", "ci": "●", "ci.": "◎", "ci..": "◌", "ciO": "◯", "cib": "●", "circ": "∘", "circeq": "≗", "circlearrowleft": "↺", "circlearrowright": "↻", "circledR": "®", "circledS": "Ⓢ", "circledast": "⊛", "circledcirc": "⊚", "circleddash": "⊝", "ciw": "○", "cl": "⌞", "clL": "⌊", "clR": "⌋", "cll": "⌞", "clr": "⌟", "clubsuit": "♣", "coe": "↑", "colon": "₡", "coloneq": "≔", "com": "ℂ", "comp": "∘", "compl": "ᶜ", "complement": "ᶜ", "complementprefix": "∁", "con": "⬝", "cong": "≅", "construction": "🚧", "coprod": "⨿", "copyright": "©", "covby": "⋖", "covers": "⋖", "crossproduct": "⨯", "cruzeiro": "₢", "cu": "⌜", "cuL": "⌈", "cuR": "⌉", "cul": "⌜", "cup": "∪", "cur": "⌝", "curlyeqprec": "⋞", "curlyeqsucc": "⋟", "curlypreceq": "≼", "curlyvee": "⋎", "curlywedge": "⋏", "currency": "¤", "curvearrowleft": "↶", "curvearrowright": "↷", "d": "↓", "d-": "↓", "d-2": "⇊", "d-u-": "⇵", "d-|": "↧", "d=": "⇓", "d==": "⟱", "dag": "†", "dagger": "†", "daleth": "ℸ", "dashv": "⊣", "dd-": "↡", "ddag": "‡", "ddagger": "‡", "ddots": "⋱", "de": "δ", "def=": "≝", "defs": "≙", "degree": "°", "dei": "ϯ", "delta": "δ", "dfinsupp": "→ₚ", "dh": "ð", "di": "◆", "di.": "◈", "diameter": "⌀", "diamond": "⋄", "diamondsuit": "♢", "dib": "◆", "die": "⚀", "digamma": "ϝ", "directsum": "⨁", "div": "÷", "divideontimes": "⋇", "division": "÷", "diw": "◇", "dl": "↙", "dl-": "↙", "dl=": "⇙", "dong": "₫", "dot": "·", "doteq": "≐", "doteqdot": "≑", "dotplus": "∔", "dotsquare": "⊡", "downarrow": "↓", "downdownarrows": "⇊", "downleftharpoon": "⇃", "downrightharpoon": "⇂", "dr": "↘", "dr-": "↘", "dr=": "⇘", "drachma": "₯", "dvd": "∣", "dz": "↯", "e": "ε", "ell": "ℓ", "em": "—", "empty": "∅", "emptyset": "∅", "en": "–", "enat": "ℕ∞", "ennreal": "ℝ≥0∞", "entails": "⊢", "ep": "ε", "eps": "ε", "epsilon": "ε", "eqcirc": "≖", "eqcolon": "≕", "eqn": "≠", "eqslantgtr": "⋝", "eqslantless": "⋜", "equiv": "≃", "et": "η", "eta": "η", "euro": "€", "ex": "∃", "exf": "∃ᶠ", "exists": "∃", "exn": "∄", "f<": "‹", "f<<": "«", "f<<>>": "«$CURSOR»", "f<>": "‹$CURSOR›", "f>": "›", "f>>": "»", "facsimile": "℻", "fallingdotseq": "≒", "fei": "ϥ", "female": "♀", "finprod": "∏ᶠ", "finsum": "∑ᶠ", "finsupp": "→₀", "flat": "♭", "floor": "⌊$CURSOR⌋", "flq": "‹", "flqq": "«", "forall": "∀", "frac": "¼", "frac1": "⅟", "frac12": "½", "frac13": "⅓", "frac14": "¼", "frac15": "⅕", "frac16": "⅙", "frac18": "⅛", "frac23": "⅔", "frac25": "⅖", "frac34": "¾", "frac35": "⅗", "frac38": "⅜", "frac45": "⅘", "frac56": "⅚", "frac58": "⅝", "frac78": "⅞", "frown": "⌢", "frq": "›", "frqq": "»", "fun": "λ", "functor": "⥤", "fuzzy": "‖", "g": "γ", "ga": "γ", "gamma": "γ", "gangia": "ϫ", "ge": "≥", "gen": "≱", "geq": "≥", "geqn": "≱", "geqq": "≧", "geqslant": "≥", "gets": "←", "gg": "≫", "ggg": "⋙", "gimel": "ℷ", "glb": "⊓", "glq": "‚", "glqq": "„", "gnapprox": "⋧", "gneq": "≩", "gneqq": "≩", "gnsim": "⋧", "goal": "⊢", "grq": "‘", "grqq": "“", "gtrapprox": "≳", "gtrdot": "⋗", "gtreqless": "⋛", "gtreqqless": "⋛", "gtrless": "≷", "gtrsim": "≳", "guarani": "₲", "gvertneqq": "≩", "hbar": "ℏ", "hcomp": "◫", "heartsuit": "♥", "heq": "≍", "heta": "ͱ", "heyting": "⇨", "himp": "⇨", "hnot": "￢", "hom": "⟶", "homotopy": "∼", "hookleftarrow": "↩", "hookrightarrow": "↪", "hori": "ϩ", "hryvnia": "₴", "i": "∩", "iff": "↔", "imath": "ı", "imp": "→", "in": "∈", "increment": "∆", "inf": "⊓", "infi": "⨅", "infty": "∞", "inn": "∉", "int": "ℤ", "integral": "∫", "integral-": "⨍", "inter": "∩", "intercal": "⊺", "intersection": "∩", "inv": "⁻¹", "io": "ι", "iota": "ι", "iso": "≅", "join": "⊔", "kI": "Į", "ka": "κ", "kappa": "κ", "kelvin": "K", "khei": "ϧ", "ki": "į", "kip": "₭", "koppa": "ϟ", "l": "←", "l-": "←", "l--": "⟵", "l-2": "⇇", "l->": "↢", "l-n": "↚", "l-r-": "⇆", "l-|": "↤", "l1": "→₁", "l1simplefunc": "→₁ₛ", "l=": "⇐", "l==": "⇚", "l=n": "⇍", "la": "λ", "lam": "λ", "lambda": "λ", "lamda": "λ", "langle": "⟨", "lari": "₾", "lbag": "⟅", "lceil": "⌈", "ldata": "《", "ldots": "…", "ldq": "“", "le": "≤", "leadsto": "↝", "leftarrow": "←", "leftarrowtail": "↢", "leftharpoondown": "↽", "leftharpoonup": "↼", "leftleftarrows": "⇇", "leftrightarrow": "↔", "leftrightarrows": "⇆", "leftrightharpoons": "⇋", "leftrightsquigarrow": "↭", "leftthreetimes": "⋋", "len": "≰", "leq": "≤", "leqn": "≰", "leqq": "≦", "leqslant": "≤", "lessapprox": "≲", "lessdot": "⋖", "lesseqgtr": "⋚", "lesseqqgtr": "⋚", "lessgtr": "≶", "lesssim": "≲", "lf": "⧏", "lfloor": "⌊", "lhd": "◁", "liel": "⁅", "lier": "⁆", "linearmap": "→ₗ", "lira": "₤", "ll": "≪", "ll-": "↞", "llbracket": "〚", "llcorner": "⌞", "lnapprox": "⋦", "lneq": "≨", "lneqq": "≨", "lnot": "¬", "lnsim": "⋦", "longleftarrow": "⟵", "longleftrightarrow": "⟷", "longrightarrow": "⟶", "looparrowleft": "↫", "looparrowright": "↬", "lozenge": "✧", "lq": "‘", "lr": "↔", "lr-": "↔", "lr--": "⟷", "lr-n": "↮", "lr=": "⇔", "lr=n": "⇎", "lrcorner": "⌟", "lr~": "↭", "lsimplex": "⦋", "ltimes": "⋉", "lub": "⊔", "lvertneqq": "≨", "l~": "↜", "m": "μ", "m=": "≞", "ma": "↦", "male": "♂", "maltese": "✠", "manat": "₼", "mapsto": "↦", "mathscr{I}": "ℐ", "measuredangle": "∡", "meet": "⊓", "mem": "∈", "member": "∈", "mho": "℧", "micro": "µ", "mid": "∣", "mill": "₥", "minus": "−", "miny": "⧿", "models": "⊧", "mop": "ᵐᵒᵖ", "mp": "∓", "mu": "μ", "mulopposite": "ᵐᵒᵖ", "multimap": "⊸", "multiplication": "×", "n": "\\n", "nLeftarrow": "⇍", "nLeftrightarrow": "⇎", "nRightarrow": "⇏", "nVDash": "⊯", "nVdash": "⊮", "nabla": "∇", "naira": "₦", "napprox": "≉", "nat": "ℕ", "nat_trans": "⟹", "nattrans": "⟹", "natural": "♮", "nbhds": "𝓝", "nceil": "⌈$CURSOR⌉₊", "ncong": "≇", "ne": "≠", "nearrow": "↗", "neg": "¬", "neq": "≠", "nequiv": "≢", "nexists": "∄", "nfloor": "⌊$CURSOR⌋₊", "ngeq": "≱", "ngeqq": "≱", "ngeqslant": "≱", "ngtr": "≯", "nhds": "𝓝", "ni": "∋", "nin": "∉", "nleftarrow": "↚", "nleftrightarrow": "↮", "nleq": "≰", "nleqq": "≰", "nleqslant": "≰", "nless": "≮", "nmid": "∤", "nni": "∌", "nnnorm": "‖$CURSOR‖₊", "nnreal": "ℝ≥0", "nomisma": "𐆎", "norm": "‖$CURSOR‖", "not": "¬", "note": "♩", "notin": "∉", "notlt": "≮", "nparallel": "∦", "nprec": "⊀", "npreceq": "⋠", "nrightarrow": "↛", "nshortmid": "∤", "nsim": "≁", "nsimeq": "≄", "nsubset": "⊄", "nsubseteq": "⊈", "nsubseteqq": "⊈", "nsucc": "⊁", "nsucceq": "⋡", "nsupset": "⊅", "nsupseteq": "⊉", "nsupseteqq": "⊉", "ntriangleleft": "⋪", "ntrianglelefteq": "⋬", "ntriangleright": "⋫", "ntrianglerighteq": "⋭", "nu": "ν", "numero": "№", "nvDash": "⊭", "nvdash": "⊬", "nwarrow": "↖", "o": "∘", "o*": "∘*", "o+": "⊕", "o-": "⊝", "o--": "⊖", "o.": "⊙", "o/": "⊘", "o=": "⊜", "octagonal": "🛑", "od": "ᵒᵈ", "odot": "⊙", "oe": "œ", "ohm": "Ω", "oiint": "∯", "oint": "∮", "om": "ω", "omega": "ω", "omicron": "ο", "ominus": "⊖", "oo": "⊚", "op": "ᵒᵖ", "oplus": "⊕", "opposite": "ᵒᵖ", "or": "∨", "or=": "≚", "orderdual": "ᵒᵈ", "ordfeminine": "ª", "ordmasculine": "º", "oslash": "⊘", "otimes": "⊗", "ounce": "℥", "ox": "⊗", "p": "Π", "pa": "▰", "pab": "▰", "paragraph": "¶", "parallel": "∥", "partial": "∂", "partnership": "㉐", "paw": "▱", "pd": "∂", "per": "⅌", "permil": "‰", "perp": "⟂", "peseta": "₧", "peso": "₱", "ph": "φ", "phi": "φ", "pi": "π", "pilcrow": "¶", "pitchfork": "⋔", "pitensorproduct": "⨂", "pm": "±", "pound": "£", "pounds": "£", "powerset": "𝒫", "pr": "↣", "prec": "≺", "precapprox": "≾", "preceq": "≼", "precnapprox": "⋨", "precnsim": "⋨", "precsim": "≾", "preim": "⁻¹'", "preimage": "⁻¹'", "prime": "′", "prod": "∏", "prohibited": "🛇", "propto": "∝", "ps": "ψ", "psi": "ψ", "qed": "∎", "quad": " ", "quot": "⧸", "r": "→", "r!": "¡", "r-": "→", "r--": "⟶", "r-2": "⇉", "r-3": "⇶", "r->": "↣", "r-l-": "⇄", "r-n": "↛", "r-o": "⊸", "r-|": "↦", "r0": "→₀", "r1": "→₁", "r1s": "→₁ₛ", "r=": "⇒", "r==": "⇛", "r=n": "⇏", "r^b": "→ᵇ", "r_0": "→₀", "r_1": "→₁", "r_1s": "→₁ₛ", "r_a": "→ₐ", "r_l": "→ₗ", "r_m": "→ₘ", "r_p": "→ₚ", "r_s": "→ₛ", "r_sl": "→ₛₗ", "ra": "→ₐ", "radioactive": "☢", "rangle": "⟩", "rat": "ℚ", "rb": "→ᵇ", "rbag": "⟆", "rceil": "⌉", "rdata": "》", "rdq": "”", "re": "▬", "real": "ℝ", "reb": "▬", "registered": "®", "rew": "▭", "rfloor": "⌋", "rh": "ρ", "rhd": "▷", "rho": "ρ", "rightangle": "∟", "rightarrow": "→", "rightarrowtail": "↣", "rightharpoondown": "⇁", "rightharpoonup": "⇀", "rightleftarrows": "⇄", "rightleftharpoons": "⇌", "rightrightarrows": "⇉", "rightthreetimes": "⋌", "risingdotseq": "≓", "rl": "→ₗ", "rm": "→ₘ", "root": "√", "rp": "→ₚ", "rq": "’", "rr-": "↠", "rrbracket": "〛", "rs": "→ₛ", "rsimplex": "⦌", "rsl": "→ₛₗ", "rtimes": "⋊", "ruble": "₽", "rupee": "₨", "rw": "▸", "r~": "↝", "sInter": "⋂₀", "sUnion": "⋃₀", "s[]": "⦋$CURSOR⦌", "sampi": "ϡ", "san": "ϻ", "sb0": "𝟬", "sb1": "𝟭", "sb2": "𝟮", "sb3": "𝟯", "sb4": "𝟰", "sb5": "𝟱", "sb6": "𝟲", "sb7": "𝟳", "sb8": "𝟴", "sb9": "𝟵", "sbs": "﹨", "scissor": "✂", "searrow": "↘", "section": "§", "semilinearmap": "→ₛₗ", "setminus": "\\", "sharp": "♯", "shei": "ϣ", "shima": "ϭ", "sho": "ϸ", "shortmid": "∣", "si": "σ", "sigma": "σ", "sigmaobj": "∐", "sim": "∼", "simeq": "≃", "simplefunc": "→ₛ", "simplex": "⦋$CURSOR⦌", "smallamalg": "∐", "smallsetminus": "∖", "smallsmile": "⌣", "smile": "⌣", "smul": "•", "spadesuit": "♠", "span": "∙", "specializes": "⤳", "spesmilo": "₷", "sphericalangle": "∢", "sq": "◾", "sq.": "▣", "sqb": "■", "sqcap": "⊓", "sqcup": "⊔", "sqo": "▢", "sqrt": "√", "sqsubset": "⊏", "sqsubseteq": "⊑", "sqsupset": "⊐", "sqsupseteq": "⊒", "square": "□", "squb": "⊑", "squbn": "⋢", "squigarrowright": "⇝", "squp": "⊒", "squpn": "⋣", "sqw": "□", "ss": "⊆", "ssqub": "⊏", "ssqup": "⊐", "ssub": "⊂", "ssubn": "⊄", "ssubset": "⊂", "ssup": "⊃", "ssupn": "⊅", "ssupset": "⊃", "st": "⋆", "st12": "✹", "st4": "✦", "st6": "✶", "st8": "✴", "star": "⋆", "stigma": "ϛ", "straightphi": "φ", "sub": "⊆", "subn": "⊈", "subset": "⊆", "subseteq": "⊆", "subseteqq": "⊆", "subsetneq": "⊊", "subsetneqq": "⊊", "succ": "≻", "succapprox": "≿", "succcurlyeq": "≽", "succeq": "≽", "succnapprox": "⋩", "succnsim": "⋩", "succsim": "≿", "sum": "∑", "sup": "⊔", "supn": "⊉", "supr": "⨆", "supset": "⊇", "supseteq": "⊇", "supseteqq": "⊇", "supsetneq": "⊋", "supsetneqq": "⊋", "surd": "√", "surd3": "∛", "surd4": "∜", "swarrow": "↙", "sy": "⁻¹", "symmdiff": "∆", "t": "▸", "t=": "≜", "ta": "τ", "tau": "τ", "tb": "◂", "telephone": "℡", "tenge": "₸", "tensorpower": "⨂", "tensorproduct": "⊗", "textbaht": "฿", "textcircledP": "℗", "textcolonmonetary": "₡", "textdied": "✝", "textdiscount": "⁒", "textestimated": "℮", "textfractionsolidus": "⁄", "textinterrobang": "‽", "textlira": "₤", "textlquill": "⁅", "textmu": "µ", "textmusicalnote": "♪", "textnaira": "₦", "textnumero": "№", "textopenbullet": "◦", "textpertenthousand": "‱", "textpeso": "₱", "textrecipe": "℞", "textreferencemark": "※", "textrquill": "⁆", "textwon": "₩", "th": "θ", "therefore": "∴", "theta": "θ", "thickapprox": "≈", "thicksim": "∼", "tie": "⁀", "times": "×", "tint": "∯", "tiny": "⧾", "to": "→", "to0": "→₀", "to1": "→₁", "to1s": "→₁ₛ", "to^b": "→ᵇ", "to_0": "→₀", "to_1": "→₁", "to_1s": "→₁ₛ", "to_a": "→ₐ", "to_l": "→ₗ", "to_m": "→ₘ", "to_p": "→ₚ", "to_s": "→ₛ", "to_sl": "→ₛₗ", "toa": "→ₐ", "tob": "→ᵇ", "tol": "→ₗ", "tom": "→ₘ", "top": "⊤", "tos": "→ₛ", "tosl": "→ₛₗ", "tr": "⬝", "trans": "▹", "transport": "▹", "triangle": "▵", "triangledown": "▿", "triangleleft": "◃", "trianglelefteq": "⊴", "triangleq": "≜", "triangleright": "▹", "trianglerighteq": "⊵", "tugrik": "₮", "tw": "◃", "twoheadleftarrow": "↞", "twoheadrightarrow": "↠", "u": "↑", "u+": "⊎", "u-": "↑", "u-2": "⇈", "u-d-": "⇅", "u-|": "↥", "u.": "⊍", "u=": "⇑", "u==": "⟰", "ud": "↕", "ud-": "↕", "ud-|": "↨", "ud=": "⇕", "ul": "↖", "ul-": "↖", "ul=": "⇖", "ulcorner": "⌜", "un": "∪", "uncertainty": "⯑", "undertie": "‿", "union": "∪", "uparrow": "↑", "updownarrow": "↕", "upleftharpoon": "↿", "uplus": "⊎", "uprightharpoon": "↾", "upsilon": "υ", "upuparrows": "⇈", "ur": "↗", "ur-": "↗", "ur=": "⇗", "urcorner": "⌝", "uu-": "↟", "v": "∨", "vC": "Č", "vD": "Ď", "vDash": "⊨", "vE": "Ě", "varbeta": "ϐ", "varkai": "ϗ", "varkappa": "ϰ", "varnothing": "∅", "varphi": "ϕ", "varpi": "ϖ", "varprime": "′", "varpropto": "∝", "varrho": "ϱ", "varsigma": "ς", "vartheta": "ϑ", "vartriangleleft": "⊲", "vartriangleright": "⊳", "vc": "č", "vd": "ď", "vdash": "⊢", "vdots": "⋮", "ve": "ě", "vectorproduct": "⨯", "vee": "∨", "veebar": "⊻", "vsi": "ς", "warning": "⚠", "wcovby": "⩿", "wcovers": "⩿", "wedge": "∧", "won": "₩", "wp": "℘", "wr": "≀", "x": "×", "xf": "×ᶠ", "xi": "ξ", "xs": "×ˢ", "yen": "¥", "ze": "ζ", "zeta": "ζ", "zsqrtd": "ℤ√", "{{": "⦃", "{{}}": "⦃$CURSOR⦄", "{}": "{$CURSOR}", "{}_": "{$CURSOR}_", "|": "∣", "|-": "⊢", "|->": "↦", "|-n": "⊬", "|=": "⊨", "|=>": "⇰", "|=n": "⊭", "|n": "∤", "||": "‖", "||-": "⊩", "||-n": "⊮", "||=": "⊫", "||=n": "⊯", "|||-": "⊪", "||||": "‖$CURSOR‖", "}}": "⦄", "~": "∼", "~-": "≃", "~-n": "≄", "~=": "≅", "~=n": "≇", "~>": "⤳", "~A": "Ã", "~N": "Ñ", "~O": "Õ", "~a": "ã", "~n": "≁", "~o": "õ", "~{n}": "ñ", "~~": "≈", "~~-": "≊", "~~n": "≉", "~~~": "≋"} diff --git a/frontend/app/utils/lean/lean-language.ts b/frontend/app/utils/lean/lean-language.ts new file mode 100644 index 0000000..9df4b7a --- /dev/null +++ b/frontend/app/utils/lean/lean-language.ts @@ -0,0 +1,252 @@ +/* The Lean 4 language for Monaco — registered once, client-side. + * + * A Monarch tokenizer (keywords, tactics, commands, the nested `/- -/` + * comments Lean uses for docstrings) plus themes built from the wiki's live + * palette, so the editor matches the page around it and follows the wiki's + * theme *and* accent switches live: the accent — caret, selection, active + * line number, keywords — is sampled from the `--accent` custom properties + * that `[data-accent]` swaps. (Lean's own server also offers semantic + * highlighting; keyword colours are the honest first pass — see the note in + * lean/README.) */ +import * as monaco from 'monaco-editor' + +export const LEAN_LANGUAGE = 'lean4' +export const LEAN_THEMES = { light: 'mathew-light', dark: 'mathew-dark' } as const + +/* words that introduce declarations, terms, and structuring */ +const keywords = [ + 'abstract', 'axiom', 'by', 'cases', 'catch', 'class', 'command', 'deriving', 'do', + 'else', 'end', 'example', 'expansion', 'explicit', 'export', 'def', 'theorem', + 'lemma', 'corollary', 'proposition', 'instance', 'structure', 'inductive', 'abbrev', + 'mutual', 'namespace', 'section', 'open', 'protected', 'private', 'partial', + 'noncomputable', 'set_option', 'unset_option', 'option', 'attribute', 'variable', + 'variables', 'include', 'hiding', 'renaming', 'as', 'where', 'from', 'show', + 'have', 'suffices', 'let', 'in', 'if', 'then', 'match', 'with', 'without', 'fun', + 'forall', 'at', 'using', 'via', 'override', 'obsolete', 'inherit', 'field', + 'generalizing', 'replacing', 'renaming', 'specializing', 'unshuffling', 'case', + 'dive', 'guard', 'modifies', 'macro', 'macro_rules', 'syntax', 'elab', 'elab_rules', + 'notation', 'infix', 'infixl', 'infixr', 'prefix', 'postfix', 'binders', + 'declare_syntax_cat', 'syntax_cat', 'extend', 'scoped', 'unused', 'auto_unfold', + 'extern', 'implemented_by', 'native_decide', 'lift', 'coe', 'coe_struct', + 'classical', 'decidable', 'universe', 'universes', 'exit', +] + +/* tactics — the words after `by` and inside tactic blocks */ +const tactics = [ + 'intro', 'intros', 'exact', 'apply', 'refine', 'have', 'obtain', 'use', 'exists', + 'constructor', 'left', 'right', 'simp', 'simp_all', 'simp_rw', 'rw', 'rewrite', + 'show', 'conv', 'calc', 'ring', 'ring_nf', 'field_simp', 'norm_num', 'omega', + 'linarith', 'nlinarith', 'positivity', 'decide', 'trivial', 'rfl', 'refl', 'symm', + 'trans', 'ext', 'funext', 'congr', 'congr!', 'cases', 'induction', 'rcases', + 'obtain', 'subst', 'contradiction', 'exfalso', 'push_neg', 'contrapose', + 'constructor', 'aesop', 'tauto', 'bv_decide', 'gcongr', 'change', 'generalize', + 'revert', 'clear', 'rename_i', 'next', 'any_goals', 'all_goals', 'focus', 'dotl', + 'by_contra', 'by_contra!', 'apply_fun', 'congr_arg', 'congrFun', 'congrArg', + 'simpa', 'simpa using', 'norm_cast', 'exact?', 'apply?', 'sorry', 'native_decide', + 'unfold', 'dsimp', 'unfold_projs', 'whisker', 'thm_to_tactic', 'tauto', 'mt', + 'absurd', 'injection', 'no_index', 'guard_goals', 'expect_failure', 'stop', 'skip', + 'trace', 'log', 'sleep', 'wait', 'recover', 'error', +] + +const commands = ['#check', '#eval', '#reduce', '#synth', '#print', '#exit', '#where', '#hole', '#why', '#loogle', '#guard'] + +let registered = false + +export function registerLeanLanguage() { + if (registered) return + registered = true + + monaco.languages.register({ id: LEAN_LANGUAGE }) + + monaco.languages.setLanguageConfiguration(LEAN_LANGUAGE, { + comments: { lineComment: '--', blockComment: ['/-', '-/'] }, + brackets: [ + ['{', '}'], ['[', ']'], ['(', ')'], + ['⟨', '⟩'], ['⟦', '⟧'], ['‹', '›'], ['⦃', '⦄'], ['⁅', '⁆'], ['⌈', '⌉'], ['⌊', '⌋'], + ], + autoClosingPairs: [ + { open: '{', close: '}' }, { open: '[', close: ']' }, { open: '(', close: ')' }, + { open: '"', close: '"' }, { open: '/-', close: '-/' }, + { open: '⟨', close: '⟩' }, { open: '⟦', close: '⟧' }, { open: '‹', close: '›' }, + ], + surroundingPairs: [ + { open: '{', close: '}' }, { open: '[', close: ']' }, { open: '(', close: ')' }, + { open: '"', close: '"' }, { open: '⟨', close: '⟩' }, { open: '⟦', close: '⟧' }, + { open: '‹', close: '›' }, + ], + indentationRules: { + increaseIndentPattern: /^\s*(\bby\b|\bdo\b|\bthen\b|\bcalc\b|\{[^}]*$|\[[^\]]*$|\([^)]*$)/, + decreaseIndentPattern: /^\s*(\bend\b|\}|\\|\)|\/-})/, + }, + }) + + monaco.languages.setMonarchTokensProvider(LEAN_LANGUAGE, { + keywords, + tactics, + commands, + tokenizer: { + root: [ + [/--.*$/, 'comment'], + [/\/-/, { token: 'comment', next: '@blockcomment' }], + [/"/, { token: 'string', next: '@string' }], + [/[0-9]+\.[0-9]+([eE][-+]?[0-9]+)?/, 'number.float'], + [/[0-9]+([eE][-+]?[0-9]+)?[nNzQqR]?/, 'number'], + [ + // one identifier run (ascii word, or a unicode run — Lean names + // carry α, →, ≤, ⁻¹), then decided against the word lists + /[a-zA-Z_#][a-zA-Z0-9_?!'∆∇]*|[^\x00-\x7F][a-zA-Z0-9_?!'∆∇]*/, + { + cases: { + '@commands': 'keyword.command', + '@tactics': 'keyword.tactic', + '@keywords': 'keyword', + '@default': 'identifier', + }, + }, + ], + [/^\s*@\[[^\]]*\]/, 'annotation'], + [/[→←↔∧∨¬∀∃≠≤≥<>!=+\-*/^|&~:;.,@#][=]?/, 'operator'], + ], + blockcomment: [ + [/\/-/, { token: 'comment', next: '@blockcomment' }], + [/-\//, { token: 'comment', next: '@pop' }], + [/[^\-\/]+/, 'comment'], + [/[\/-]/, 'comment'], + ], + string: [ + [/[^\\"]+/, 'string'], + [/\\./, 'string.escape'], + [/"/, { token: 'string', next: '@pop' }], + ], + }, + }) +} + +/* ---------- the wiki's palette, read live, as editor themes ---------- */ + +/* Monaco themes are plain hex, not CSS variables, so the accent is sampled + * off the document each time a theme is built — the same read the canvas + * surfaces make. The fallbacks are violet, the wiki's default accent. */ +function wikiAccent(dark: boolean) { + const css = getComputedStyle(document.documentElement) + const at = (name: string, fallback: string) => css.getPropertyValue(name).trim() || fallback + return { + accent: at('--accent', dark ? '#7c8cff' : '#4f5fe8'), + strong: at('--accent-strong', dark ? '#99a5ff' : '#3d4dd6'), + second: at('--accent-2', dark ? '#38d3ee' : '#0ea5c9'), + } +} + +/* `#rrggbbaa` — Monaco's translucent form, standing in for the wiki's + * `color-mix`. Shorthand hex is widened; anything else passes through. */ +function alpha(hex: string, a: string) { + if (/^#[0-9a-f]{3}$/i.test(hex)) return `#${hex.slice(1).split('').map(c => c + c).join('')}${a}` + return /^#[0-9a-f]{6}$/i.test(hex) ? `${hex}${a}` : hex +} + +/* token rules take hex without the leading `#` */ +function ink(hex: string) { + return hex.replace(/^#/, '') +} + +/* Themes are named by their palette (mathew-dark-fb7185…): a new accent + * yields a fresh theme rather than one Monaco may have cached under an old + * palette, and a reader cycling back reuses a definition already made. */ +const definedThemes = new Set() + +/* the theme matching the wiki right now — [data-theme] picks the surfaces, + * [data-accent] the caret, selection, active line number and keywords */ +export function currentLeanTheme(): string { + const dark = document.documentElement.getAttribute('data-theme') === 'dark' + const a = wikiAccent(dark) + const name = `${dark ? LEAN_THEMES.dark : LEAN_THEMES.light}-${ink(a.accent)}-${ink(a.strong)}-${ink(a.second)}`.toLowerCase() + if (definedThemes.has(name)) return name + definedThemes.add(name) + + monaco.editor.defineTheme(name, dark + ? { + base: 'vs-dark', + inherit: true, + rules: [ + { token: 'keyword', foreground: ink(a.strong) }, + { token: 'keyword.tactic', foreground: '38d3ee' }, + { token: 'keyword.command', foreground: ink(a.strong), fontStyle: 'bold' }, + { token: 'string', foreground: '3fce8b' }, + { token: 'number', foreground: 'f5a83c' }, + { token: 'comment', foreground: '6b7488', fontStyle: 'italic' }, + { token: 'annotation', foreground: '99a1b5' }, + { token: 'operator', foreground: '99a1b5' }, + { token: 'type.identifier', foreground: '38d3ee' }, + ], + colors: { + 'editor.background': '#141826', + 'editor.foreground': '#e7eaf3', + 'editor.lineHighlightBackground': '#1a2030', + 'editorLineNumber.foreground': '#6b7488', + 'editorLineNumber.activeForeground': a.accent, + 'editorCursor.foreground': a.accent, + 'editor.selectionBackground': alpha(a.accent, '40'), + 'editor.selectionHighlightBackground': alpha(a.accent, '1f'), + 'editorIndentGuide.background1': '#232a3c', + 'editorIndentGuide.activeBackground1': '#313a52', + 'editorWhitespace.foreground': '#313a52', + 'editorWidget.background': '#10131c', + 'editorWidget.border': '#232a3c', + 'editorSuggestWidget.selectedBackground': '#1a2030', + 'editorHoverWidget.background': '#10131c', + 'editorHoverWidget.border': '#232a3c', + 'scrollbarSlider.background': '#e7eaf329', + 'scrollbarSlider.hoverBackground': '#e7eaf347', + 'scrollbarSlider.activeBackground': '#e7eaf366', + 'editorError.foreground': '#f47085', + 'editorWarning.foreground': '#f5a83c', + 'editorInfo.foreground': a.second, + }, + } + : { + base: 'vs', + inherit: true, + rules: [ + { token: 'keyword', foreground: ink(a.strong) }, + { token: 'keyword.tactic', foreground: '0891b2' }, + { token: 'keyword.command', foreground: ink(a.strong), fontStyle: 'bold' }, + { token: 'string', foreground: '189a5c' }, + { token: 'number', foreground: 'd97706' }, + { token: 'comment', foreground: '8a93a8', fontStyle: 'italic' }, + { token: 'annotation', foreground: '5b6478' }, + { token: 'operator', foreground: '5b6478' }, + { token: 'type.identifier', foreground: '0891b2' }, + ], + colors: { + 'editor.background': '#ffffff', + 'editor.foreground': '#1b2130', + 'editor.lineHighlightBackground': '#eef1f7', + 'editorLineNumber.foreground': '#8a93a8', + 'editorLineNumber.activeForeground': a.accent, + 'editorCursor.foreground': a.accent, + 'editor.selectionBackground': alpha(a.accent, '33'), + 'editor.selectionHighlightBackground': alpha(a.accent, '1a'), + 'editorIndentGuide.background1': '#e2e6ef', + 'editorIndentGuide.activeBackground1': '#cfd5e3', + 'editorWhitespace.foreground': '#cfd5e3', + 'editorWidget.background': '#ffffff', + 'editorWidget.border': '#e2e6ef', + 'editorSuggestWidget.selectedBackground': '#eef1f7', + 'editorHoverWidget.background': '#ffffff', + 'editorHoverWidget.border': '#e2e6ef', + 'scrollbarSlider.background': '#1b213024', + 'scrollbarSlider.hoverBackground': '#1b21304d', + 'scrollbarSlider.activeBackground': '#1b213066', + 'editorError.foreground': '#d1344b', + 'editorWarning.foreground': '#d97706', + 'editorInfo.foreground': a.second, + }, + }) + + return name +} + +/* move the editor to the palette the wiki is wearing right now */ +export function applyLeanTheme() { + monaco.editor.setTheme(currentLeanTheme()) +} diff --git a/frontend/app/utils/lean/lsp.ts b/frontend/app/utils/lean/lsp.ts new file mode 100644 index 0000000..08301ce --- /dev/null +++ b/frontend/app/utils/lean/lsp.ts @@ -0,0 +1,116 @@ +/* A very small JSON-RPC 2.0 client over WebSocket — the dialect the lean4web + * server forwards between the browser and a real Lean language server + * (`lake serve`): one JSON message per frame, in either direction. + * + * The wiki is a deliberate minimal client: it opens one document, tracks the + * cursor, and asks for goals. The Lean server nonetheless sends a few + * *requests* its way — registering file watchers, asking to refresh caches, + * probing for configuration. There is nothing to register or refresh here, + * so those are acknowledged with `null` (a `workspace/configuration` probe + * with `null` per item) rather than left hanging. */ + +export interface RpcError { + code: number + message: string + data?: unknown +} + +interface RpcMessage { + jsonrpc: '2.0' + id?: number | string + method?: string + params?: unknown + result?: unknown + error?: RpcError +} + +export class RpcSocket { + private ws: WebSocket + private nextId = 1 + private pending = new Map void, reject: (e: Error) => void }>() + private closed = false + + readonly whenOpen: Promise + + constructor( + url: string, + private handlers: { + onNotification?: (method: string, params: unknown) => void + onClose?: (info: { clean: boolean }) => void + } = {}, + ) { + this.ws = new WebSocket(url) + this.whenOpen = new Promise((resolve, reject) => { + this.ws.addEventListener('open', () => resolve(), { once: true }) + this.ws.addEventListener('error', () => reject(new Error('websocket failed to open')), { once: true }) + }) + + this.ws.addEventListener('message', (ev: MessageEvent) => { + let msg: RpcMessage + try { + msg = JSON.parse(String(ev.data)) + } + catch { return } + if (!msg || typeof msg !== 'object' || msg.jsonrpc !== '2.0') return + + if (msg.id !== undefined && msg.method) { this.answerServer(msg); return } + if (msg.id !== undefined) { + const waiter = this.pending.get(Number(msg.id)) + if (!waiter) return + this.pending.delete(Number(msg.id)) + if (msg.error) waiter.reject(new Error(`${msg.method ?? 'request'}: ${msg.error.message}`)) + else waiter.resolve(msg.result) + return + } + if (msg.method) this.handlers.onNotification?.(msg.method, msg.params) + }) + + this.ws.addEventListener('close', (ev: CloseEvent) => { + this.closed = true + const err = new Error('lean server closed the connection') + for (const waiter of this.pending.values()) waiter.reject(err) + this.pending.clear() + this.handlers.onClose?.({ clean: ev.wasClean }) + }) + } + + get open() { + return this.ws.readyState === WebSocket.OPEN + } + + async request(method: string, params?: unknown): Promise { + if (this.closed || this.ws.readyState !== WebSocket.OPEN) throw new Error('not connected to the lean server') + const id = this.nextId++ + const wire: RpcMessage = { jsonrpc: '2.0', id, method } + if (params !== undefined) wire.params = params + this.ws.send(JSON.stringify(wire)) + return new Promise((resolve, reject) => { + this.pending.set(id, { resolve: resolve as (v: unknown) => void, reject }) + }) + } + + notify(method: string, params?: unknown) { + if (this.closed || this.ws.readyState !== WebSocket.OPEN) return + const wire: RpcMessage = { jsonrpc: '2.0', method } + if (params !== undefined) wire.params = params + this.ws.send(JSON.stringify(wire)) + } + + close() { + this.closed = true + try { this.ws.close() } + catch { /* already gone */ } + } + + /* capability registrations, cache refreshes, configuration probes: the + * honest answer from a single-document client is "nothing to do" */ + private answerServer(msg: RpcMessage) { + let result: unknown = null + if (msg.method === 'workspace/configuration') { + const items = (msg.params as { items?: unknown[] } | undefined)?.items + result = Array.isArray(items) ? items.map(() => null) : null + } + if (this.closed || this.ws.readyState !== WebSocket.OPEN) return + this.ws.send(JSON.stringify({ jsonrpc: '2.0', id: msg.id, result })) + } +} diff --git a/frontend/app/utils/lean/monaco-worker.ts b/frontend/app/utils/lean/monaco-worker.ts new file mode 100644 index 0000000..59c9399 --- /dev/null +++ b/frontend/app/utils/lean/monaco-worker.ts @@ -0,0 +1,8 @@ +/* Monaco's editor worker, wrapped so the `?worker` import stays static + * (what this toolchain resolves) while the component still pulls it in + * lazily, only in the browser. Monaco 0.57's exports map makes paths like + * `monaco-editor/esm/vs/...` invalid — the package-root form below is the + * real specifier (`./editor/*` → `./esm/vs/editor/*`). */ +import EditorWorker from 'monaco-editor/editor/editor.worker.js?worker' + +export { EditorWorker } diff --git a/frontend/app/utils/plot-expression.ts b/frontend/app/utils/plot-expression.ts index a7d43d1..e66c69f 100644 --- a/frontend/app/utils/plot-expression.ts +++ b/frontend/app/utils/plot-expression.ts @@ -10,6 +10,14 @@ everything it accepts is a real function of x or a real relation in the plane, and everything else is refused with a reason. + A name that is not x, y, one of the constants, or a called function is a + free variable — "k", "a", "radius" — and asks for a slider: the compiled + answer names the variables it speaks, and evaluation reads their values + from the scope it is handed. So an expression with a variable means the + family of curves those values trace. "k" alone, or "k = 2" ahead of a + plain number, is the declaration itself: it claims the slider and plots + nothing of its own. + Precedence is the usual one: + - bind loosest; then * / % (left, implicit multiplication included — "2x" is 2·x); then unary minus, so -x^2 negates the square; then ^, right-associative, its exponent may carry a sign so @@ -20,24 +28,39 @@ export type PlotFunction = (x: number) => number /* a relation of the plane: the curve is its zero set */ export type PlaneFunction = (x: number, y: number) => number +/* a surface of space: the height z above the point (x, y) */ +export type SurfaceFunction = (x: number, y: number) => number + +/* the values a free name answers with — one slider per variable. A name the + scope does not carry yet reads as 1, where a fresh slider starts */ +export type VarScope = Record + /* why a text was refused: nothing to read, a name the calculator does not speak, or a shape the grammar rejects */ export type PlotErrorReason = 'empty' | 'unknown' | 'syntax' export type CompiledPlot = - | { ok: true; kind: 'function'; fn: PlotFunction } - | { ok: true; kind: 'relation'; fn: PlaneFunction } - // "(x, y)" or "P = (x, y)": a single dot at fixed coordinates, optionally named - | { ok: true; kind: 'point'; x: number; y: number; label: string | null } + // each kind carries the free variables it speaks, in order of appearance + | { ok: true; kind: 'function'; vars: string[]; fn: PlotFunction } + | { ok: true; kind: 'relation'; vars: string[]; fn: PlaneFunction } + // "(x, y)" or "P = (x, y)": a single dot at fixed coordinates, optionally + // named. Coordinates may ride the sliders, so the dot moves with them + | { ok: true; kind: 'point'; vars: string[]; x: number; y: number; label: string | null } + // "k" or "k = 2": claims a slider. A null value says the text asked for + // one without saying where it starts. Plots nothing of its own + | { ok: true; kind: 'variable'; vars: string[]; name: string; value: number | null } | { ok: false; reason: PlotErrorReason } type Op = '+' | '-' | '*' | '/' | '%' | '^' | '=' | '(' | ')' | ',' -type Token = { t: Op } | { t: 'num'; value: number } | { t: 'id'; name: string } +/* a number carries the text it was read from: the typesetter prints that, + so a half-typed decimal keeps the digits exactly as they stand */ +type Token = { t: Op } | { t: 'num'; value: number; raw: string } | { t: 'id'; name: string } type Node = - | { kind: 'num'; value: number } - | { kind: 'var'; name: 'x' | 'y' } + | { kind: 'num'; value: number; raw?: string } + // x and y are the plane's coordinates; every other name is a slider + | { kind: 'var'; name: string } | { kind: 'const'; value: number } | { kind: 'neg'; arg: Node } | { kind: 'bin'; op: '+' | '-' | '*' | '/' | '%' | '^'; a: Node; b: Node } @@ -132,9 +155,10 @@ function tokenize(src: string): Token[] { i++ } else break } - const value = Number.parseFloat(s.slice(start, i)) + const text = s.slice(start, i) + const value = Number.parseFloat(text) if (!Number.isFinite(value)) throw new PlotParseError('syntax') - toks.push({ t: 'num', value }) + toks.push({ t: 'num', value, raw: text }) continue } if (/[a-z_]/i.test(c)) { @@ -171,6 +195,9 @@ function tokenize(src: string): Token[] { interface Parser { toks: Token[] pos: number + /* when set, a name that is not x, y, a constant or a called function + becomes a variable recorded here; when absent, it is refused */ + free: Set | null } const peek = (p: Parser): Token | null => p.toks[p.pos] ?? null @@ -238,7 +265,7 @@ function parseAtom(p: Parser): Node { if (!tk) throw new PlotParseError('syntax') if (tk.t === 'num') { p.pos++ - return { kind: 'num', value: tk.value } + return { kind: 'num', value: tk.value, raw: tk.raw } } if (tk.t === '(') { p.pos++ @@ -268,28 +295,39 @@ function parseAtom(p: Parser): Node { if (!arityOk(tk.name, args.length)) throw new PlotParseError('syntax') return { kind: 'call', name: tk.name, args } } + // no coordinate, no constant, no name the calculator calls — then it is + // a variable: a slider the reader sets, shared wherever its name is spoken + if (p.free) { + p.free.add(tk.name) + return { kind: 'var', name: tk.name } + } throw new PlotParseError('unknown') } throw new PlotParseError('syntax') } -function evaluate(node: Node, x: number, y: number): number { +function evaluate(node: Node, x: number, y: number, scope: VarScope): number { switch (node.kind) { case 'num': return node.value - case 'var': - return node.name === 'x' ? x : y + case 'var': { + if (node.name === 'x') return x + if (node.name === 'y') return y + // a slider's set value; until it carries one, where every slider starts + const v = scope[node.name] + return typeof v === 'number' && Number.isFinite(v) ? v : 1 + } case 'const': return node.value case 'neg': - return -evaluate(node.arg, x, y) + return -evaluate(node.arg, x, y, scope) case 'call': { const fn = FUNCTIONS[node.name]! - return fn(...node.args.map((a) => evaluate(a, x, y))) + return fn(...node.args.map((a) => evaluate(a, x, y, scope))) } case 'bin': { - const a = evaluate(node.a, x, y) - const b = evaluate(node.b, x, y) + const a = evaluate(node.a, x, y, scope) + const b = evaluate(node.b, x, y, scope) switch (node.op) { case '+': return a + b @@ -326,9 +364,26 @@ function mentionsY(node: Node): boolean { } } -/* a point's coordinates hold no variable — a lone x or y has no single value - to place a dot at, so only constant expressions (numbers, pi, sqrt(2)…) - make a coordinate */ +/* whether x or y stands anywhere in a tree. A point's coordinate may ride + the sliders — each has one value to place the dot at — but a plane + variable has no single value, so the dot would have nowhere to go */ +function mentionsPlane(node: Node): boolean { + switch (node.kind) { + case 'var': + return node.name === 'x' || node.name === 'y' + case 'neg': + return mentionsPlane(node.arg) + case 'bin': + return mentionsPlane(node.a) || mentionsPlane(node.b) + case 'call': + return node.args.some(mentionsPlane) + default: + return false + } +} + +/* a declaration's value is a plain number — numbers, pi, sqrt(2)… welcome, + sliders and x and y not */ function isConstant(node: Node): boolean { switch (node.kind) { case 'var': @@ -377,62 +432,317 @@ function pointPair(toks: Token[]): [Token[], Token[]] | null { } /* one run of tokens, the whole of it — a leftover is a shape the grammar - does not know */ -function parseAll(toks: Token[]): Node { - const p: Parser = { toks, pos: 0 } + does not know. Free variables are collected into `free` when given */ +function parseAll(toks: Token[], free: Set | null = null): Node { + const p: Parser = { toks, pos: 0, free } const ast = parseExpr(p) if (p.pos !== toks.length) throw new PlotParseError('syntax') return ast } -/* read one expression, equation, or point; a refusal says whether a name was - not known or the shape was wrong — an empty text is the caller's to treat as - "nothing asked for", not as an error. A "(x, y)" — or "P = (x, y)" with a - name out front — is a point at fixed coordinates. With an "=" otherwise the - text is the relation left − right = 0 (a lone "y =" ahead of an expression - in x is still the fast function); without it, an expression in x is y = f(x) - and one carrying y is the relation that expression equals zero. */ -export function compilePlotExpression(src: string): CompiledPlot { +/* a name the reader may claim for a slider: not one of the plane's two + coordinates, not one of the constants, not a function the calculator calls */ +function declName(name: string): string | null { + if (name === 'x' || name === 'y') return null + if (Object.hasOwn(CONSTANTS, name) || Object.hasOwn(FUNCTIONS, name)) return null + return name +} + +/* read a slider's claim from a token run — "k" alone, or "k = 2" with a + claimable name ahead of a plain number — or null when the text claims + none. The value reads strictly: a "P = (2, 3)" or "k = x" is a point and + a relation, not declarations, and says so by not parsing as a number. */ +function declarationOf(toks: Token[]): { name: string; value: number | null } | null { + if (toks.length === 0 || toks[0]!.t !== 'id') return null + const name = declName(toks[0]!.name) + if (!name) return null + if (toks.length === 1) return { name, value: null } + if (toks.length > 2 && toks[1]!.t === '=' && !toks.slice(2).some((tk) => tk.t === '=')) { + try { + const rhs = parseAll(toks.slice(2)) // strict: a declaration's value is a plain number + if (isConstant(rhs)) return { name, value: evaluate(rhs, 0, 0, {}) } + } catch { + /* not a plain number — not a declaration, whatever it reads as instead */ + } + } + return null +} + +/* read one expression, equation, point or slider declaration; a refusal says + whether a name was not known or the shape was wrong — an empty text is the + caller's to treat as "nothing asked for", not as an error. A "(x, y)" — or + "P = (x, y)" with a name out front — is a point at fixed coordinates. With + an "=" otherwise the text is the relation left − right = 0 (a lone "y =" + ahead of an expression in x is still the fast function); without it, an + expression in x is y = f(x) and one carrying y is the relation that + expression equals zero. A name none of those readings speaks — "k" alone, + or "k = 2" ahead of a plain number — declares a slider: it plots nothing + and its value answers everywhere the name is spoken. Functions, relations + and points list the variables they speak in `vars` and read their values + from `scope` at their every evaluation — so one dragged slider moves the + whole family of curves at once. */ +export function compilePlotExpression(src: string, scope: VarScope = {}): CompiledPlot { if (src.length > 400) return { ok: false, reason: 'syntax' } try { const toks = tokenize(stripAssignment(src)) if (toks.length === 0) return { ok: false, reason: 'empty' } const at = toks.findIndex((tk) => tk.t === '=') + const free = new Set() + + // A slider claiming its own row: "k", or "k = 2" ahead of a plain number + const decl = declarationOf(toks) + if (decl) return { ok: true, kind: 'variable', vars: [decl.name], name: decl.name, value: decl.value } // A point: "(x, y)" on its own, or "P = (x, y)" with a lone name ahead of - // the "=". Coordinates must be constant — a variable has no single value - // to place a dot at — and finite once read. + // the "=". Coordinates may ride the sliders — and must be finite once read. const named = at === 1 && toks[0]!.t === 'id' const pair = pointPair(named ? toks.slice(2) : toks) if (pair) { - const cx = parseAll(pair[0]) - const cy = parseAll(pair[1]) - if (!isConstant(cx) || !isConstant(cy)) return { ok: false, reason: 'syntax' } - const x = evaluate(cx, 0, 0) - const y = evaluate(cy, 0, 0) + const cx = parseAll(pair[0], free) + const cy = parseAll(pair[1], free) + if (mentionsPlane(cx) || mentionsPlane(cy)) return { ok: false, reason: 'syntax' } + const x = evaluate(cx, 0, 0, scope) + const y = evaluate(cy, 0, 0, scope) if (!Number.isFinite(x) || !Number.isFinite(y)) return { ok: false, reason: 'syntax' } const label = named ? src.slice(0, src.indexOf('=')).trim() : null - return { ok: true, kind: 'point', x, y, label: label || null } + return { ok: true, kind: 'point', vars: [...free], x, y, label: label || null } } if (at === -1) { - const ast = parseAll(toks) + const ast = parseAll(toks, free) return mentionsY(ast) - ? { ok: true, kind: 'relation', fn: (x, y) => evaluate(ast, x, y) } - : { ok: true, kind: 'function', fn: (x) => evaluate(ast, x, 0) } + ? { ok: true, kind: 'relation', vars: [...free], fn: (x, y) => evaluate(ast, x, y, scope) } + : { ok: true, kind: 'function', vars: [...free], fn: (x) => evaluate(ast, x, 0, scope) } } const left = toks.slice(0, at) const right = toks.slice(at + 1) if (left.length === 0 || right.length === 0 || right.some((tk) => tk.t === '=')) throw new PlotParseError('syntax') - const rhs = parseAll(right) + const rhs = parseAll(right, free) // "y = " is the explicit curve it always was: x alone decides it if (left.length === 1 && left[0]!.t === 'id' && left[0]!.name === 'y' && !mentionsY(rhs)) - return { ok: true, kind: 'function', fn: (x) => evaluate(rhs, x, 0) } - const lhs = parseAll(left) - return { ok: true, kind: 'relation', fn: (x, y) => evaluate(lhs, x, y) - evaluate(rhs, x, y) } + return { ok: true, kind: 'function', vars: [...free], fn: (x) => evaluate(rhs, x, 0, scope) } + const lhs = parseAll(left, free) + return { + ok: true, + kind: 'relation', + vars: [...free], + fn: (x, y) => evaluate(lhs, x, y, scope) - evaluate(rhs, x, y, scope), + } } catch (err) { if (err instanceof PlotParseError) return { ok: false, reason: err.reason } return { ok: false, reason: 'syntax' } } } + +/* the inside of the 3D field's "z = …" — a lone "z =" ahead of an expression + in x and y; the reader may also write "f(x, y) =" or type the height with + no left side at all, which reads the same */ +function stripSurfaceAssignment(src: string): string { + return src + .replace(/^\s*f\s*\(\s*x\s*,\s*y\s*\)\s*=/i, '') + .replace(/^\s*z\s*=/i, '') +} + +export type CompiledSurface = + // each carries the free variables it speaks, in order of appearance + | { ok: true; kind: 'surface'; vars: string[]; fn: SurfaceFunction } + // "k" or "k = 2": claims a slider, as in the plane's fields. A null value + // says the text asked for one without saying where it starts. Draws nothing + | { ok: true; kind: 'variable'; vars: string[]; name: string; value: number | null } + | { ok: false; reason: PlotErrorReason } + +/* compile the height of a surface above (x, y): the same algebra as the + plane, only read as z = f(x, y). A "z =" ahead of the expression is the + height's own name and sheds; what is left must speak x and y (constants + are welcome — a level surface is still a surface). Names x and y are not + are slider variables read from scope at each evaluation, and "k" or + "k = 2" is the plane's slider declaration — space and plane wear the very + same variables. A stray "=" is still a leftover: space answers a height + alone, and refuses whatever cannot read as one. */ +export function compileSurfaceExpression(src: string, scope: VarScope = {}): CompiledSurface { + if (src.length > 400) return { ok: false, reason: 'syntax' } + try { + const body = stripSurfaceAssignment(src) + const toks = tokenize(body) + if (toks.length === 0) return { ok: false, reason: 'empty' } + // a slider claiming its own row: "k", or "k = 2" ahead of a plain number + const decl = declarationOf(toks) + if (decl) return { ok: true, kind: 'variable', vars: [decl.name], name: decl.name, value: decl.value } + const free = new Set() + const ast = parseAll(toks, free) + return { ok: true, kind: 'surface', vars: [...free], fn: (x, y) => evaluate(ast, x, y, scope) } + } catch (err) { + if (err instanceof PlotParseError) return { ok: false, reason: err.reason } + return { ok: false, reason: 'syntax' } + } +} + +/* ---------- printing the same maths back typeset ---------- */ + +/* the calculator's fields echo their text as set mathematics while it is + typed (Desmos' way). Printing the parser's own tree keeps the two + readings honest: what is displayed is exactly what would be plotted — + so a text that does not compile simply has no type-setting, and an + unfinished draft stays plain text until it reads right. Fractions are + fractions, radicals are radicals, exponents rise; parentheses appear + only where precedence would otherwise lie. */ + +const LATEX_FUNCTIONS: Record = { + sin: '\\sin', + cos: '\\cos', + tan: '\\tan', + asin: '\\arcsin', + acos: '\\arccos', + atan: '\\arctan', + sinh: '\\sinh', + cosh: '\\cosh', + tanh: '\\tanh', + ln: '\\ln', + log: '\\log', + log2: '\\log_{2}', + log10: '\\log_{10}', + min: '\\min', + max: '\\max', +} + +/* a folded constant answers as its symbol when its value is exactly one */ +function constSymbol(v: number): string | null { + if (v === Math.PI) return '\\pi' + if (v === Math.PI * 2) return '\\tau' + if (v === Math.E) return 'e' + if (v === (1 + Math.sqrt(5)) / 2) return '\\varphi' + return null +} + +/* how tightly a printed node binds: one that binds looser than the context + it stands in gains parentheses */ +function nodePrec(n: Node): number { + if (n.kind === 'bin') { + if (n.op === '+' || n.op === '-') return 10 + if (n.op === '^') return 40 + if (n.op === '/') return 90 // a \\frac carries its own grouping + return 20 // * and % + } + if (n.kind === 'neg') return 30 + return 100 +} + +function printNode(n: Node, ctx: number): string { + const s = printBare(n) + return nodePrec(n) < ctx ? `\\left(${s}\\right)` : s +} + +/* two factors standing side by side are multiplied silently — unless the + right one is a number (numbers must not run together), or a bare number + is followed by a fraction (which would read as a mixed number) */ +function needsDot(a: Node, b: Node): boolean { + if (b.kind === 'num') return true + return a.kind === 'num' && b.kind === 'bin' && b.op === '/' +} + +function printBare(n: Node): string { + switch (n.kind) { + case 'num': + return n.raw ?? String(n.value) + case 'var': + return n.name + case 'const': + return constSymbol(n.value) ?? String(n.value) + case 'neg': + return `-${printNode(n.arg, 30)}` + case 'call': + return printCall(n.name, n.args) + case 'bin': { + switch (n.op) { + case '+': + return `${printNode(n.a, 10)} + ${printNode(n.b, 11)}` + case '-': + return `${printNode(n.a, 10)} - ${printNode(n.b, 11)}` + case '*': { + const a = printNode(n.a, 20) + // a looser factor beside a silent product would change its sense — + // even a leading minus reads as subtraction there. The gap between + // factors is a space: free in math mode, and it keeps a \\pi from + // running into the next atom as one control word + const b = printNode(n.b, 31) + return needsDot(n.a, n.b) ? `${a} \\cdot ${b}` : `${a} ${b}` + } + case '/': + return `\\frac{${printNode(n.a, 0)}}{${printNode(n.b, 0)}}` + case '%': + return `${printNode(n.a, 20)} \\bmod ${printNode(n.b, 21)}` + case '^': + // braces group the exponent outright, so it never needs parentheses; + // an exp(...) base is already a superscribed e — it takes parens + // rather than carry a second superscript + return `${n.a.kind === 'call' && n.a.name === 'exp' ? `\\left(${printBare(n.a)}\\right)` : printNode(n.a, 41)}^{${printNode(n.b, 0)}}` + } + } + } +} + +function printCall(name: string, args: Node[]): string { + const one = args[0] ?? { kind: 'num', value: 0 } + switch (name) { + case 'sqrt': + return `\\sqrt{${printNode(one, 0)}}` + case 'cbrt': + return `\\sqrt[3]{${printNode(one, 0)}}` + case 'abs': + return `\\left|${printNode(one, 0)}\\right|` + case 'floor': + return `\\left\\lfloor ${printNode(one, 0)} \\right\\rfloor` + case 'ceil': + return `\\left\\lceil ${printNode(one, 0)} \\right\\rceil` + case 'exp': + return `e^{${printNode(one, 0)}}` + case 'mod': + return `${printNode(args[0] ?? one, 20)} \\bmod ${printNode(args[1] ?? one, 21)}` + default: { + const label = LATEX_FUNCTIONS[name] ?? name + return `${label}\\left(${args.map((a) => printNode(a, 0)).join(',\\, ')}\\right)` + } + } +} + +/* the whole text of a field as one typeset line: the same readings the + compiler runs — an "f(x) =" or "z =" ahead of the maths is shed, a lone + "y =" the field's gutter already wears is shed too (the gutter prints + it), a "(x, y)" — optionally named — is a point, a claimable name alone + or ahead of a plain number claims a slider, and any other "=" is the + equation it states. Free variables print as themselves, italic like the + rest. Null when the text does not read: the caller keeps the plain text, + and its red, until it does. */ +export function expressionToLatex(src: string): string | null { + if (!src.trim() || src.length > 400) return null + try { + const toks = tokenize(stripSurfaceAssignment(stripAssignment(src))) + if (toks.length === 0) return null + const at = toks.findIndex((tk) => tk.t === '=') + const free = new Set() + + const named = at === 1 && toks[0]!.t === 'id' + const pair = pointPair(named ? toks.slice(2) : toks) + if (pair) { + const coords = `\\left(${printNode(parseAll(pair[0], free), 0)},\\, ${printNode(parseAll(pair[1], free), 0)}\\right)` + if (!named) return coords + const label = src.slice(0, src.indexOf('=')).trim() + const name = /^[a-z][a-z0-9_]*$/i.test(label) ? label : `\\text{${label.replace(/[\\{}]/g, '')}}` + return `${name} = ${coords}` + } + + if (at === -1) return printNode(parseAll(toks, free), 0) + const left = toks.slice(0, at) + const right = toks.slice(at + 1) + if (left.length === 0 || right.length === 0 || right.some((tk) => tk.t === '=')) return null + // "y = " is the function the field's gutter already wears: the + // type-set line answers with its right side alone + if (left.length === 1 && left[0]!.t === 'id' && left[0]!.name === 'y' && !right.some((tk) => tk.t === 'id' && tk.name === 'y')) + return printNode(parseAll(right, free), 0) + // "=" binds loosest of all — neither side ever needs parentheses + return `${printNode(parseAll(left, free), 0)} = ${printNode(parseAll(right, free), 0)}` + } catch { + return null + } +} diff --git a/frontend/app/utils/routes.ts b/frontend/app/utils/routes.ts index 29d041c..aa0c240 100644 --- a/frontend/app/utils/routes.ts +++ b/frontend/app/utils/routes.ts @@ -67,17 +67,19 @@ export function isReadingSurface(path: string): boolean { /* ---------- the wiki's own pages ---------- - The link map and the graphing calculator are pages the shelf holds no - copies of — but the book can read them too. Each has one plain address of - its own, and useArticleTabs can lay it on the row beside the open articles: - the page then draws the live surface instead of an article, for as long as - its page stays open. */ + The link map, the calculators and the Lean editor are pages the shelf + holds no copies of — but the book can read them too. Each has one plain + address of its own, and useArticleTabs can lay it on the row beside the + open articles: the page then draws the live surface instead of an + article, for as long as its page stays open. */ -export type ToolPage = 'graph' | 'calculator' +export type ToolPage = 'graph' | 'calculator' | 'calculator3d' | 'lean' const TOOL_PAGE_PATHS: Record = { graph: '/graph', calculator: '/calculator', + calculator3d: '/calculator3d', + lean: '/lean', } /** The address a tool page lives at. */ diff --git a/frontend/i18n/locales/ca.json b/frontend/i18n/locales/ca.json index a95ee17..4545a8c 100644 --- a/frontend/i18n/locales/ca.json +++ b/frontend/i18n/locales/ca.json @@ -33,6 +33,10 @@ "graph": "Graf", "calculator": "Calculadora", "calculatorHint": "Calculadora — representa funcions i equacions", + "calculator3d": "Calculadora 3D", + "calculator3dHint": "Calculadora 3D — representa superfícies a l'espai", + "lean": "Lean", + "leanHint": "Lean — escriu i comprova proves al navegador", "admin": "Admin", "adminHint": "Administració — els comptes d'aquesta wiki", "requests": "Sol·licituds", @@ -170,16 +174,55 @@ "show": "Mostra al pla", "hide": "Amaga del pla", "remove": "Treu la funció", - "add": "Afegeix funció", + "add": "Afegeix expressió", "errorUnknown": "No conec aquest nom — la calculadora entén x, y, pi, e i les funcions habituals.", "errorSyntax": "Això no es llegeix com una funció de x ni com una equació en x i y.", "resetView": "Reinicia la vista", "zoomIn": "Apropa", "zoomOut": "Allunya", "cursor": "x = {x} y = {y}", + "variablesPanel": "Variables", + "variableValue": "Valor de {name}", + "editVariable": "Edita {name}", "collapse": "Amaga les funcions", "expand": "Mostra les funcions" }, + "calc3d": { + "metaTitle": "Calculadora gràfica 3D", + "metaDescription": "Representa superfícies z = f(x, y) a l'espai — l'escena gira arrossegant i s'apropa amb la roda. sin, cos, ln, sqrt i companyia.", + "panelHeading": "Superfícies", + "functionsPanel": "Superfícies a representar", + "expressionAria": "Funció de x i y", + "errorSyntax": "Això no es llegeix com una funció de x i y.", + "show": "Mostra a l'espai", + "hide": "Amaga de l'espai", + "config": "Configuració de l'espai", + "configSubdivisions": "Subdivisions", + "configZNote": "z segueix l'alçada de les superfícies", + "configMin": "Límit inferior de {axis}", + "configMax": "Límit superior de {axis}" + }, + "lean": { + "metaTitle": "Editor de Lean", + "metaDescription": "Escriu Lean 4 al navegador — l'editor comprova les proves amb Mathlib en el seu propi servidor Lean dedicat.", + "editorAria": "Editor de Lean 4", + "loading": "Obrint l'editor de Lean…", + "openExternal": "Obre l'editor en una pestanya nova", + "noServer": "Aquest wiki no té cap servidor de Lean connectat — indica a NUXT_PUBLIC_LEAN_URL on n'hi ha un (mira lean/).", + "unreachable": "El servidor de Lean no respon a {url} — pot ser que encara s'estigui iniciant (la primera arrencada construeix les memòries cau de Mathlib). Comprova que està en marxa (des de l'arrel del repo: ./dev.sh) i torna-ho a provar.", + "retry": "Torna-ho a provar", + "connecting": "Connectant amb el servidor de Lean…", + "initializing": "Despertant el Lean i carregant Mathlib — la primera vegada tarda una mica.", + "elaborating": "Comprovant…", + "ready": "Lean {version} — a punt", + "goals": "Objectius", + "messages": "Missatges", + "noGoals": "Cap objectiu al cursor.", + "infoview": "Vista d'informació", + "collapse": "Amaga la vista d'informació", + "expand": "Mostra la vista d'informació", + "seedDoc": "import Mathlib\n\n-- Posa el cursor darrere del `sorry`: l'objectiu apareix a la dreta.\n-- Ctrl+Space compleix; escriu `\\le` per a ≤.\n\nexample : 2 + 2 = 4 := by\n sorry\n" + }, "reader": { "notFoundTitle": "Aquest article no existeix (encara)", "notFoundText": "No hi ha res a {path}. Tu mateix pots escriure'n la primera versió — només cal Markdown.", diff --git a/frontend/i18n/locales/de.json b/frontend/i18n/locales/de.json index 06b1dee..16e7079 100644 --- a/frontend/i18n/locales/de.json +++ b/frontend/i18n/locales/de.json @@ -33,6 +33,10 @@ "graph": "Graph", "calculator": "Rechner", "calculatorHint": "Rechner — Funktionen und Gleichungen plotten", + "calculator3d": "3D-Rechner", + "calculator3dHint": "3D-Rechner — Flächen im Raum plotten", + "lean": "Lean", + "leanHint": "Lean — Beweise im Browser schreiben und prüfen", "admin": "Admin", "adminHint": "Verwaltung — die Konten in dieser Wiki", "requests": "Anfragen", @@ -170,16 +174,55 @@ "show": "Auf der Ebene anzeigen", "hide": "Auf der Ebene ausblenden", "remove": "Funktion entfernen", - "add": "Funktion hinzufügen", + "add": "Ausdruck hinzufügen", "errorUnknown": "Den Namen kenne ich nicht — der Rechner spricht x, y, pi, e und die üblichen Funktionen.", "errorSyntax": "Das liest sich nicht als Funktion von x oder als Gleichung in x und y.", "resetView": "Ansicht zurücksetzen", "zoomIn": "Vergrößern", "zoomOut": "Verkleinern", "cursor": "x = {x} y = {y}", + "variablesPanel": "Variablen", + "variableValue": "Wert von {name}", + "editVariable": "{name} bearbeiten", "collapse": "Funktionen ausblenden", "expand": "Funktionen einblenden" }, + "calc3d": { + "metaTitle": "3D-Grafikrechner", + "metaDescription": "Flächen z = f(x, y) im Raum zeichnen — die Szene dreht sich per Zug, die Rollen zoomt. sin, cos, ln, sqrt und Co.", + "panelHeading": "Flächen", + "functionsPanel": "Zu zeichnende Flächen", + "expressionAria": "Funktion von x und y", + "errorSyntax": "Das liest sich nicht als Funktion von x und y.", + "show": "Im Raum anzeigen", + "hide": "Im Raum ausblenden", + "config": "Raumkonfiguration", + "configSubdivisions": "Unterteilungen", + "configZNote": "z folgt der Höhe der Flächen", + "configMin": "Untere {axis}-Grenze", + "configMax": "Obere {axis}-Grenze" + }, + "lean": { + "metaTitle": "Lean-Editor", + "metaDescription": "Lean 4 im Browser — der Editor prüft Beweise gegen Mathlib auf einem eigenen dedizierten Lean-Server.", + "editorAria": "Lean-4-Editor", + "loading": "Der Lean-Editor wird geöffnet…", + "openExternal": "Editor in neuem Tab öffnen", + "noServer": "Dieses Wiki hat keinen Lean-Server angeschlossen — setze NUXT_PUBLIC_LEAN_URL auf die Adresse eines Servers (siehe lean/).", + "unreachable": "Der Lean-Server antwortet nicht auf {url} — vielleicht startet er noch (der erste Start baut die Mathlib-Caches). Prüfe, ob er läuft (vom Repo-Stamm: ./dev.sh), und versuche es erneut.", + "retry": "Erneut versuchen", + "connecting": "Verbindung mit dem Lean-Server wird aufgebaut…", + "initializing": "Lean wird geweckt und Mathlib geladen — beim ersten Mal dauert das einen Moment.", + "elaborating": "Prüfung…", + "ready": "Lean {version} — bereit", + "goals": "Ziele", + "messages": "Nachrichten", + "noGoals": "Kein Ziel am Cursor.", + "infoview": "Infoansicht", + "collapse": "Infoansicht ausblenden", + "expand": "Infoansicht einblenden", + "seedDoc": "import Mathlib\n\n-- Setze den Cursor hinter das `sorry` — das Ziel erscheint rechts.\n-- Strg+Leertaste ergänzt; `\\le` ergibt ≤.\n\nexample : 2 + 2 = 4 := by\n sorry\n" + }, "reader": { "notFoundTitle": "Dieser Artikel existiert (noch) nicht", "notFoundText": "Unter {path} ist nichts. Du kannst die erste Version selbst schreiben — es braucht nur Markdown.", diff --git a/frontend/i18n/locales/en.json b/frontend/i18n/locales/en.json index cd8e876..d4fe839 100644 --- a/frontend/i18n/locales/en.json +++ b/frontend/i18n/locales/en.json @@ -33,6 +33,10 @@ "graph": "Graph", "calculator": "Calculator", "calculatorHint": "Calculator — plot functions and equations", + "calculator3d": "3D Calculator", + "calculator3dHint": "3D Calculator — plot surfaces in space", + "lean": "Lean", + "leanHint": "Lean — write and check proofs in the browser", "admin": "Admin", "adminHint": "Admin — the accounts on this wiki", "requests": "Requests", @@ -170,16 +174,55 @@ "show": "Show on the plane", "hide": "Hide from the plane", "remove": "Remove function", - "add": "Add function", + "add": "Add expression", "errorUnknown": "I don't know that name — the calculator speaks x, y, pi, e and the usual functions.", "errorSyntax": "This does not read as a function of x or an equation in x and y.", "resetView": "Reset the view", "zoomIn": "Zoom in", "zoomOut": "Zoom out", "cursor": "x = {x} y = {y}", + "variablesPanel": "Variables", + "variableValue": "Value of {name}", + "editVariable": "Edit {name}", "collapse": "Hide functions", "expand": "Show functions" }, + "calc3d": { + "metaTitle": "3D graphing calculator", + "metaDescription": "Plot surfaces z = f(x, y) in space — the scene turns with a drag and zooms with the wheel. sin, cos, ln, sqrt and friends.", + "panelHeading": "Surfaces", + "functionsPanel": "Surfaces to plot", + "expressionAria": "Function of x and y", + "errorSyntax": "This does not read as a function of x and y.", + "show": "Show in the space", + "hide": "Hide from the space", + "config": "Space configuration", + "configSubdivisions": "Subdivisions", + "configZNote": "z follows the surfaces' height", + "configMin": "{axis} lower bound", + "configMax": "{axis} upper bound" + }, + "lean": { + "metaTitle": "Lean editor", + "metaDescription": "Write Lean 4 in the browser — the editor checks proofs against Mathlib on its own dedicated Lean server.", + "editorAria": "Lean 4 editor", + "loading": "Opening the Lean editor…", + "openExternal": "Open the editor in a new tab", + "noServer": "This wiki has no Lean server wired up — set NUXT_PUBLIC_LEAN_URL to where one lives (see lean/).", + "unreachable": "The Lean server is not answering at {url} — it may still be starting (the first boot builds the Mathlib caches). Check it is running (from the repo root: ./dev.sh), then try again.", + "retry": "Try again", + "connecting": "Connecting to the Lean server…", + "initializing": "Waking Lean and loading Mathlib — the first run takes a moment.", + "elaborating": "Checking…", + "ready": "Lean {version} — ready", + "goals": "Goals", + "messages": "Messages", + "noGoals": "No goal at the cursor.", + "infoview": "Infoview", + "collapse": "Hide infoview", + "expand": "Show infoview", + "seedDoc": "import Mathlib\n\n-- Place the cursor after the `sorry` — the goal appears on the right.\n-- Ctrl+Space completes; typing `\\le` gives ≤.\n\nexample : 2 + 2 = 4 := by\n sorry\n" + }, "reader": { "notFoundTitle": "This article does not exist (yet)", "notFoundText": "Nothing lives at {path}. You can write the first version yourself — it only takes Markdown.", diff --git a/frontend/i18n/locales/es.json b/frontend/i18n/locales/es.json index cb14631..d3b8903 100644 --- a/frontend/i18n/locales/es.json +++ b/frontend/i18n/locales/es.json @@ -33,6 +33,10 @@ "graph": "Grafo", "calculator": "Calculadora", "calculatorHint": "Calculadora — representa funciones y ecuaciones", + "calculator3d": "Calculadora 3D", + "calculator3dHint": "Calculadora 3D — representa superficies en el espacio", + "lean": "Lean", + "leanHint": "Lean — escribe y comprueba pruebas en el navegador", "admin": "Admin", "adminHint": "Administración — las cuentas de esta wiki", "requests": "Solicitudes", @@ -170,16 +174,55 @@ "show": "Mostrar en el plano", "hide": "Ocultar del plano", "remove": "Quitar función", - "add": "Añadir función", + "add": "Añadir expresión", "errorUnknown": "No conozco ese nombre — la calculadora habla x, y, pi, e y las funciones de siempre.", "errorSyntax": "Esto no se lee como una función de x ni como una ecuación en x e y.", "resetView": "Reiniciar la vista", "zoomIn": "Acercar", "zoomOut": "Alejar", "cursor": "x = {x} y = {y}", + "variablesPanel": "Variables", + "variableValue": "Valor de {name}", + "editVariable": "Editar {name}", "collapse": "Ocultar las funciones", "expand": "Mostrar las funciones" }, + "calc3d": { + "metaTitle": "Calculadora gráfica 3D", + "metaDescription": "Representa superficies z = f(x, y) en el espacio — la escena gira arrastrando y se acerca con la rueda. sin, cos, ln, sqrt y compañía.", + "panelHeading": "Superficies", + "functionsPanel": "Superficies a representar", + "expressionAria": "Función de x e y", + "errorSyntax": "Esto no se lee como una función de x e y.", + "show": "Mostrar en el espacio", + "hide": "Ocultar del espacio", + "config": "Configuración del espacio", + "configSubdivisions": "Subdivisiones", + "configZNote": "z sigue la altura de las superficies", + "configMin": "Límite inferior de {axis}", + "configMax": "Límite superior de {axis}" + }, + "lean": { + "metaTitle": "Editor de Lean", + "metaDescription": "Escribe Lean 4 en el navegador — el editor comprueba las pruebas con Mathlib en su propio servidor Lean dedicado.", + "editorAria": "Editor de Lean 4", + "loading": "Abriendo el editor de Lean…", + "openExternal": "Abrir el editor en una pestaña nueva", + "noServer": "Este wiki no tiene ningún servidor de Lean conectado — indica en NUXT_PUBLIC_LEAN_URL dónde vive uno (mira lean/).", + "unreachable": "El servidor de Lean no responde en {url} — puede que todavía se esté iniciando (el primer arranque construye las cachés de Mathlib). Comprueba que está en marcha (desde la raíz del repo: ./dev.sh) y vuelve a intentarlo.", + "retry": "Volver a intentarlo", + "connecting": "Conectando con el servidor de Lean…", + "initializing": "Despertando Lean y cargando Mathlib — la primera vez tarda un poco.", + "elaborating": "Comprobando…", + "ready": "Lean {version} — listo", + "goals": "Objetivos", + "messages": "Mensajes", + "noGoals": "Ningún objetivo en el cursor.", + "infoview": "Vista de información", + "collapse": "Ocultar la vista de información", + "expand": "Mostrar la vista de información", + "seedDoc": "import Mathlib\n\n-- Coloca el cursor tras el `sorry`: el objetivo aparece a la derecha.\n-- Ctrl+Space completa; escribe `\\le` para ≤.\n\nexample : 2 + 2 = 4 := by\n sorry\n" + }, "reader": { "notFoundTitle": "Este artículo no existe (todavía)", "notFoundText": "No hay nada en {path}. Puedes escribir tú la primera versión — solo hace falta Markdown.", diff --git a/frontend/i18n/locales/fr.json b/frontend/i18n/locales/fr.json index 0e77920..dbe9041 100644 --- a/frontend/i18n/locales/fr.json +++ b/frontend/i18n/locales/fr.json @@ -33,6 +33,10 @@ "graph": "Graphe", "calculator": "Calculatrice", "calculatorHint": "Calculatrice — trace des fonctions et des équations", + "calculator3d": "Calculatrice 3D", + "calculator3dHint": "Calculatrice 3D — trace des surfaces dans l'espace", + "lean": "Lean", + "leanHint": "Lean — écrire et vérifier des preuves dans le navigateur", "admin": "Admin", "adminHint": "Administration — les comptes de ce wiki", "requests": "Demandes", @@ -170,16 +174,55 @@ "show": "Afficher sur le plan", "hide": "Masquer du plan", "remove": "Supprimer la fonction", - "add": "Ajouter une fonction", + "add": "Ajouter une expression", "errorUnknown": "Je ne connais pas ce nom — la calculatrice parle x, y, pi, e et les fonctions habituelles.", "errorSyntax": "Cela ne se lit pas comme une fonction de x ni comme une équation en x et y.", "resetView": "Réinitialiser la vue", "zoomIn": "Zoomer", "zoomOut": "Dézoomer", "cursor": "x = {x} y = {y}", + "variablesPanel": "Variables", + "variableValue": "Valeur de {name}", + "editVariable": "Modifier {name}", "collapse": "Masquer les fonctions", "expand": "Afficher les fonctions" }, + "calc3d": { + "metaTitle": "Calculatrice graphique 3D", + "metaDescription": "Tracez des surfaces z = f(x, y) dans l'espace — la scène tourne à la souris et se zoome à la molette. sin, cos, ln, sqrt et compagnie.", + "panelHeading": "Surfaces", + "functionsPanel": "Surfaces à tracer", + "expressionAria": "Fonction de x et y", + "errorSyntax": "Cela ne se lit pas comme une fonction de x et y.", + "show": "Afficher dans l'espace", + "hide": "Masquer de l'espace", + "config": "Configuration de l'espace", + "configSubdivisions": "Subdivisions", + "configZNote": "z suit la hauteur des surfaces", + "configMin": "Borne inférieure de {axis}", + "configMax": "Borne supérieure de {axis}" + }, + "lean": { + "metaTitle": "Éditeur Lean", + "metaDescription": "Écrire du Lean 4 dans le navigateur — l'éditeur vérifie les preuves avec Mathlib sur son propre serveur Lean dédié.", + "editorAria": "Éditeur Lean 4", + "loading": "Ouverture de l'éditeur Lean…", + "openExternal": "Ouvrir l'éditeur dans un nouvel onglet", + "noServer": "Ce wiki n'a pas de serveur Lean connecté — indiquez dans NUXT_PUBLIC_LEAN_URL où se trouve le serveur (voir lean/).", + "unreachable": "Le serveur Lean ne répond pas sur {url} — il est peut-être encore en train de démarrer (le premier démarrage construit les caches de Mathlib). Vérifiez qu'il tourne (depuis la racine du dépôt : ./dev.sh), puis réessayez.", + "retry": "Réessayer", + "connecting": "Connexion au serveur Lean…", + "initializing": "Réveil de Lean et chargement de Mathlib — la première fois prend un moment.", + "elaborating": "Vérification…", + "ready": "Lean {version} — prêt", + "goals": "Objectifs", + "messages": "Messages", + "noGoals": "Aucun objectif sous le curseur.", + "infoview": "Vue d'information", + "collapse": "Masquer la vue d'information", + "expand": "Afficher la vue d'information", + "seedDoc": "import Mathlib\n\n-- Placez le curseur après le `sorry` — l'objectif apparaît à droite.\n-- Ctrl+Space complète ; tapez `\\le` pour ≤.\n\nexample : 2 + 2 = 4 := by\n sorry\n" + }, "reader": { "notFoundTitle": "Cet article n'existe pas (encore)", "notFoundText": "Rien ne vit à {path}. Vous pouvez en écrire vous-même la première version — il ne faut que du Markdown.", diff --git a/frontend/nuxt.config.ts b/frontend/nuxt.config.ts index 7e8d6dd..1646146 100644 --- a/frontend/nuxt.config.ts +++ b/frontend/nuxt.config.ts @@ -43,6 +43,10 @@ export default defineNuxtConfig({ // browser calls /api on its own origin and nginx routes it to the // backend; dev keeps the absolute localhost address. apiBase: process.env.NUXT_PUBLIC_API_BASE ?? 'http://localhost:5000', + // Where the Lean editor server (lean4web — see lean/) lives: /lean + // frames this address. It is the browser's own way in, not the + // server's — the iframe talks to its own origin from there on. + leanUrl: process.env.NUXT_PUBLIC_LEAN_URL ?? 'http://localhost:8080', }, }, diff --git a/frontend/package-lock.json b/frontend/package-lock.json index 5da40df..30e721e 100644 --- a/frontend/package-lock.json +++ b/frontend/package-lock.json @@ -13,6 +13,7 @@ "katex": "^0.18.9", "markdown-it": "^15.0.2", "markdown-it-texmath": "^1.0.0", + "monaco-editor": "^0.57.0", "nuxt": "^4.5.2", "vue": "^3.5.43", "vue-router": "^5.3.1" @@ -9003,6 +9004,18 @@ "url": "https://github.com/fb55/entities?sponsor=1" } }, + "node_modules/marked": { + "version": "14.0.0", + "resolved": "https://registry.npmjs.org/marked/-/marked-14.0.0.tgz", + "integrity": "sha512-uIj4+faQ+MgHgwUW1l2PsPglZLOLOT1uErt06dAPtx2kjteLAkbsd/0FiYg/MGS+i7ZKLb7w2WClxHkzOOuryQ==", + "license": "MIT", + "bin": { + "marked": "bin/marked.js" + }, + "engines": { + "node": ">= 18" + } + }, "node_modules/mdn-data": { "version": "2.27.1", "resolved": "https://registry.npmjs.org/mdn-data/-/mdn-data-2.27.1.tgz", @@ -9178,6 +9191,25 @@ "integrity": "sha512-aF7yRQr/Q0O2/4pIXm6PZ5G+jAd7QS4Yu8m+WEeEHGnbo+7mE36CbLSDQiXYV8bVL3NfmdeqPJct0tUlnjVSnA==", "license": "MIT" }, + "node_modules/monaco-editor": { + "version": "0.57.0", + "resolved": "https://registry.npmjs.org/monaco-editor/-/monaco-editor-0.57.0.tgz", + "integrity": "sha512-5BkI9KGoqrNvBGUe15/QlZq3OooZ8WLg1AxTpaqHRCP3HNpzPPZKE2EDz8M7c+VRmCeUw1Brp4cx/PWm3kI/5A==", + "license": "MIT", + "dependencies": { + "dompurify": "3.4.15", + "marked": "14.0.0" + } + }, + "node_modules/monaco-editor/node_modules/dompurify": { + "version": "3.4.15", + "resolved": "https://registry.npmjs.org/dompurify/-/dompurify-3.4.15.tgz", + "integrity": "sha512-EUBjM+B+lkDE41iE82DDSCfkoPGfXx8IxFxPMjNzm/Uk4xDet77rTN9wqlxlVg71kK7XGuUMv6wUxJUwwv+Xyw==", + "license": "(MPL-2.0 OR Apache-2.0)", + "optionalDependencies": { + "@types/trusted-types": "^2.0.7" + } + }, "node_modules/mrmime": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/mrmime/-/mrmime-2.0.1.tgz", diff --git a/frontend/package.json b/frontend/package.json index 9e32d8c..86c5b3d 100644 --- a/frontend/package.json +++ b/frontend/package.json @@ -16,6 +16,7 @@ "katex": "^0.18.9", "markdown-it": "^15.0.2", "markdown-it-texmath": "^1.0.0", + "monaco-editor": "^0.57.0", "nuxt": "^4.5.2", "vue": "^3.5.43", "vue-router": "^5.3.1" diff --git a/frontend/types/vite-worker.d.ts b/frontend/types/vite-worker.d.ts new file mode 100644 index 0000000..84d6d65 --- /dev/null +++ b/frontend/types/vite-worker.d.ts @@ -0,0 +1,5 @@ +/* Vite's `?worker` import suffix (used by the Lean editor's web worker) */ +declare module '*?worker' { + const workerConstructor: new () => Worker + export default workerConstructor +} diff --git a/lean/Dockerfile b/lean/Dockerfile new file mode 100644 index 0000000..d9f84aa --- /dev/null +++ b/lean/Dockerfile @@ -0,0 +1,70 @@ +# Mathew — the Lean editor server +# +# Builds lean4web (https://github.com/leanprover-community/lean4web) from its +# upstream source and runs its production server: one port serves the editor +# client and the Lean sessions, which is what the wiki frames at /lean. +# +# Lean4web runs a real Lean process per session, so upstream asks for a +# dedicated server — this image carries the editor and Mathlib, the machine +# carries the load. +# +# docker build -t mathew-lean ./lean +# docker run -p 8080:8080 mathew-lean # → http://localhost:8080 +# +# The build is heavy by nature (Mathlib is fetched and its precompiled +# cache unpacked); expect a long build and an image of several GB. + +FROM node:24-bookworm + +# lake fetches dependencies over git/curl, drives clang to link, and elan +# (Lean's toolchain manager) installs the toolchains each project pins +RUN apt-get update && apt-get install -y --no-install-recommends \ + bash curl git ca-certificates unzip rsync \ + build-essential clang pkg-config libssl-dev \ + && rm -rf /var/lib/apt/lists/* + +# elan, with no default toolchain — every project pins its own in its +# lean-toolchain file, and elan installs that one when asked +RUN curl -sSfL https://elan.lean-lang.org/elan-init.sh | bash -s -- -y --default-toolchain none +ENV PATH="/root/.elan/bin:${PATH}" + +# The lean4web source. Pass a tag or branch to pin a build: +# docker build --build-arg LEAN4WEB_REF=v0.2.2 ./lean +ARG LEAN4WEB_REF=main +RUN git clone --depth 1 --branch "${LEAN4WEB_REF}" \ + https://github.com/leanprover-community/lean4web.git /opt/lean4web + +WORKDIR /opt/lean4web +RUN npm install + +# Build the Lean projects under Projects/ (MathlibDemo pulls Mathlib and +# unpacks its precompiled cache — the slow part of the image) and then the +# editor client, which the server serves alongside its websocket +RUN npm run build:projects + +# Mathew's theme layer: the wiki's font, stylesheet, and theme handshake +# join the client's public/ so they ship in the built bundle, and a sed +# wires them into index.html (and renames the tab). The wiki opens the +# frame as ?theme=light|dark and the editor opens matching the page +# around it — lean/theme/mathew.css explains how the skin attaches. +COPY theme/mathew.css theme/theme-init.js ./client/public/ +COPY theme/fonts/. ./client/public/fonts/ +RUN sed -i \ + -e 's##\n \n #' \ + -e 's#Lean Web#Lean · Mathew#' \ + client/index.html + +RUN npm run build:client + +# Bubblewrap cannot sandbox inside a container (no nested user namespaces by +# default) — Docker itself is the isolation here, so the server runs Lean +# directly. PORT 8080 is lean4web's production default: editor + websocket. +ENV NODE_ENV=production \ + NO_BWRAP=true \ + PORT=8080 +EXPOSE 8080 + +HEALTHCHECK --interval=30s --timeout=5s --start-period=90s --retries=3 \ + CMD curl -sf http://localhost:8080/health || exit 1 + +CMD ["npm", "run", "prod"] diff --git a/lean/README.md b/lean/README.md new file mode 100644 index 0000000..d6cbc38 --- /dev/null +++ b/lean/README.md @@ -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 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 + `/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 +`` 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=`). 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. diff --git a/lean/theme/fonts/SIL Open Font License.txt b/lean/theme/fonts/SIL Open Font License.txt new file mode 100644 index 0000000..8ed8440 --- /dev/null +++ b/lean/theme/fonts/SIL Open Font License.txt @@ -0,0 +1,55 @@ +Copyright (C) Authors of original metafont fonts: +Donald Ervin Knuth (cm, concrete fonts) +1995, 1996, 1997 J"org Knappen, 1990, 1992 Norbert Schwarz (ec fonts) +1992-2006 A.Khodulev, O.Lapko, A.Berdnikov, V.Volovich (lh fonts) +1997-2005 Claudio Beccari (cb greek fonts) +2002 FUKUI Rei (tipa fonts) +2003-2005 Han The Thanh (Vietnamese fonts) +1996-2005 Walter Schmidt (cmbright fonts) + +Copyright (C) 2003-2009, Andrey V. Panov (panov@canopus.iacp.dvo.ru), +with Reserved Font Family Name "Computer Modern Unicode fonts". + + + +This Font Software is licensed under the SIL Open Font License, Version 1.1. +This license is copied below, and is also available with a FAQ at: http://scripts.sil.org/OFL + +----------------------------------------------------------- +SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007 +----------------------------------------------------------- + +PREAMBLE +The goals of the Open Font License (OFL) are to stimulate worldwide development of collaborative font projects, to support the font creation efforts of academic and linguistic communities, and to provide a free and open framework in which fonts may be shared and improved in partnership with others. + +The OFL allows the licensed fonts to be used, studied, modified and redistributed freely as long as they are not sold by themselves. The fonts, including any derivative works, can be bundled, embedded, redistributed and/or sold with any software provided that any reserved names are not used by derivative works. The fonts and derivatives, however, cannot be released under any other type of license. The requirement for fonts to remain under this license does not apply to any document created using the fonts or their derivatives. + +DEFINITIONS +"Font Software" refers to the set of files released by the Copyright Holder(s) under this license and clearly marked as such. This may include source files, build scripts and documentation. + +"Reserved Font Name" refers to any names specified as such after the copyright statement(s). + +"Original Version" refers to the collection of Font Software components as distributed by the Copyright Holder(s). + +"Modified Version" refers to any derivative made by adding to, deleting, or substituting -- in part or in whole -- any of the components of the Original Version, by changing formats or by porting the Font Software to a new environment. + +"Author" refers to any designer, engineer, programmer, technical writer or other person who contributed to the Font Software. + +PERMISSION & CONDITIONS +Permission is hereby granted, free of charge, to any person obtaining a copy of the Font Software, to use, study, copy, merge, embed, modify, redistribute, and sell modified and unmodified copies of the Font Software, subject to the following conditions: + +1) Neither the Font Software nor any of its individual components, in Original or Modified Versions, may be sold by itself. + +2) Original or Modified Versions of the Font Software may be bundled, redistributed and/or sold with any software, provided that each copy contains the above copyright notice and this license. These can be included either as stand-alone text files, human-readable headers or in the appropriate machine-readable metadata fields within text or binary files as long as those fields can be easily viewed by the user. + +3) No Modified Version of the Font Software may use the Reserved Font Name(s) unless explicit written permission is granted by the corresponding Copyright Holder. This restriction only applies to the primary font name as presented to the users. + +4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font Software shall not be used to promote, endorse or advertise any Modified Version, except to acknowledge the contribution(s) of the Copyright Holder(s) and the Author(s) or with their explicit written permission. + +5) The Font Software, modified or unmodified, in part or in whole, must be distributed entirely under this license, and must not be distributed under any other license. The requirement for fonts to remain under this license does not apply to any document created using the Font Software. + +TERMINATION +This license becomes null and void if any of the above conditions are not met. + +DISCLAIMER +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE FONT SOFTWARE. \ No newline at end of file diff --git a/lean/theme/fonts/cmunbi.ttf b/lean/theme/fonts/cmunbi.ttf new file mode 100644 index 0000000..20505cf Binary files /dev/null and b/lean/theme/fonts/cmunbi.ttf differ diff --git a/lean/theme/fonts/cmunbx.ttf b/lean/theme/fonts/cmunbx.ttf new file mode 100644 index 0000000..9a42c0e Binary files /dev/null and b/lean/theme/fonts/cmunbx.ttf differ diff --git a/lean/theme/fonts/cmunrm.ttf b/lean/theme/fonts/cmunrm.ttf new file mode 100644 index 0000000..5e182b3 Binary files /dev/null and b/lean/theme/fonts/cmunrm.ttf differ diff --git a/lean/theme/fonts/cmunti.ttf b/lean/theme/fonts/cmunti.ttf new file mode 100644 index 0000000..ec5f1f6 Binary files /dev/null and b/lean/theme/fonts/cmunti.ttf differ diff --git a/lean/theme/mathew.css b/lean/theme/mathew.css new file mode 100644 index 0000000..7a2fdea --- /dev/null +++ b/lean/theme/mathew.css @@ -0,0 +1,215 @@ +/* ================================================================== + Mathew — the wiki's skin for lean4web. + + Lean4web paints its whole interface — the top bar, menus, modals and + the Monaco editor itself — with the CSS custom properties its VS Code + theme defines (`--vscode-*`), and its app root carries the + `monaco-editor` class so those variables reach every corner of the + page. This layer therefore does not fight the editor's styling: it + redefines that same vocabulary with the wiki's tokens — Computer + Modern for the chrome, the wiki's paper-and-slate surfaces, its + violet for focus, selection and links. + + The wiki opens the frame as ?theme=light|dark and the companion + theme-init.js records that on before the + first paint; with no parameter (a direct visit) the browser's + preference decides, exactly as lean4web's own default does. The + editor thus opens matching the page around it; the wiki's own theme + switch takes effect on the frame's next mount, not mid-edit — a live + swap would tear down a running Lean session. + + The rules that target elements directly (rather than through the + --vscode variables) carry an `html[data-mathew-theme]` prefix: the + client bundles its own stylesheets through JavaScript, which can land + after this link, so specificity, not source order, is what holds. + ================================================================== */ + +/* ---------- the wiki's typeface ---------- */ +/* Computer Modern, the wiki's reading face. CMU ships only two weights, + so intermediate weights map onto real faces the way the wiki's own + stylesheet does. */ +@font-face { + font-family: 'Computer Modern'; + src: url('/fonts/cmunrm.ttf') format('truetype'); + font-weight: 100 550; + font-style: normal; + font-display: swap; +} +@font-face { + font-family: 'Computer Modern'; + src: url('/fonts/cmunti.ttf') format('truetype'); + font-weight: 100 550; + font-style: italic; + font-display: swap; +} +@font-face { + font-family: 'Computer Modern'; + src: url('/fonts/cmunbx.ttf') format('truetype'); + font-weight: 551 900; + font-style: normal; + font-display: swap; +} +@font-face { + font-family: 'Computer Modern'; + src: url('/fonts/cmunbi.ttf') format('truetype'); + font-weight: 551 900; + font-style: italic; + font-display: swap; +} + +/* ---------- the wiki's palette, as the editor knows it ---------- */ +html[data-mathew-theme='light'], html:not([data-mathew-theme]) { + color-scheme: light; + --mw-bg: #f7f8fb; + --mw-bg-elev: #ffffff; + --mw-surface: #ffffff; + --mw-surface-2: #eef1f7; + --mw-input-bg: #ffffff; + --mw-border: #e2e6ef; + --mw-text: #1b2130; + --mw-muted: #5b6478; + --mw-accent: #4f5fe8; + --mw-accent-strong: #3d4dd6; + --mw-on-accent: #ffffff; + --mw-danger: #d1344b; + --mw-warning: #d97706; + --mw-shadow: 0 4px 12px rgb(16 24 40 / 8%), 0 16px 40px -12px rgb(16 24 40 / 18%); +} + +html[data-mathew-theme='dark'] { + color-scheme: dark; + --mw-bg: #0a0c12; + --mw-bg-elev: #10131c; + --mw-surface: #141826; + --mw-surface-2: #1a2030; + --mw-input-bg: #0c0f16; + --mw-border: #232a3c; + --mw-text: #e7eaf3; + --mw-muted: #99a1b5; + --mw-accent: #7c8cff; + --mw-accent-strong: #99a5ff; + --mw-on-accent: #0a0c12; + --mw-danger: #f47085; + --mw-warning: #f5a83c; + --mw-shadow: 0 4px 16px rgb(0 0 0 / 40%), 0 24px 48px -16px rgb(0 0 0 / 55%); +} + +/* ---------- the same vocabulary, in Mathew's colours ---------- + The app root (`.app.monaco-editor`) is where the editor's theme + service publishes --vscode-*; redefining the same names on it, with + an attribute selector for company, outranks the generated rules and + the whole interface — editor included — follows the wiki instead. */ +html[data-mathew-theme] body, +html[data-mathew-theme] .monaco-editor { + /* the editor paper */ + --vscode-editor-background: var(--mw-surface); + --vscode-editor-foreground: var(--mw-text); + --vscode-editor-selectionBackground: color-mix(in srgb, var(--mw-accent) 26%, transparent); + --vscode-editorCursor-foreground: var(--mw-accent); + --vscode-editorLineNumber-activeForeground: var(--mw-accent); + --vscode-editorGutter-background: var(--mw-surface); + + /* chrome: the top bar, menus, popups, hover */ + --vscode-menu-background: var(--mw-bg-elev); + --vscode-menu-foreground: var(--mw-text); + --vscode-menu-separatorBackground: var(--mw-border); + --vscode-menu-selectionBackground: var(--mw-surface-2); + --vscode-menu-selectionForeground: var(--mw-text); + --vscode-panel-border: var(--mw-border); + --vscode-widget-shadow: var(--mw-shadow); + + /* hovers and suggestions the editor paints */ + --vscode-editorWidget-border: var(--mw-border); + --vscode-editorHoverWidget-background: var(--mw-bg-elev); + --vscode-editorHoverWidget-foreground: var(--mw-text); + --vscode-editorHoverWidget-border: var(--mw-border); + + /* form controls, buttons, links */ + --vscode-input-background: var(--mw-input-bg); + --vscode-input-foreground: var(--mw-text); + --vscode-inputOption-activeForeground: var(--mw-accent); + --vscode-button-background: var(--mw-accent); + --vscode-button-hoverBackground: var(--mw-accent-strong); + --vscode-button-foreground: var(--mw-on-accent); + --vscode-button-border: transparent; + --vscode-textLink-foreground: var(--mw-accent-strong); + --vscode-focusBorder: var(--mw-accent); + + /* lists (the file and project pickers) */ + --vscode-list-hoverBackground: var(--mw-surface-2); + --vscode-list-dropBackground: color-mix(in srgb, var(--mw-accent) 12%, transparent); + + /* the editor draws its own scrollbars — same subtle wash as the wiki's */ + --vscode-scrollbarSlider-background: color-mix(in srgb, var(--mw-text) 18%, transparent); + --vscode-scrollbarSlider-hoverBackground: color-mix(in srgb, var(--mw-text) 30%, transparent); + --vscode-scrollbarSlider-activeBackground: color-mix(in srgb, var(--mw-text) 40%, transparent); + + /* messages and marks, in the wiki's reds and ambers */ + --vscode-notifications-background: var(--mw-bg-elev); + --vscode-notificationsErrorIcon-foreground: var(--mw-danger); + --vscode-editorError-foreground: var(--mw-danger); + --vscode-editorWarning-foreground: var(--mw-warning); + --vscode-editorWarning-background: color-mix(in srgb, var(--mw-warning) 14%, transparent); + --vscode-editorOverviewRuler-warningForeground: var(--mw-warning); + + /* inline code, as the wiki sets it */ + --vscode-textPreformat-background: var(--mw-surface-2); + --vscode-textPreformat-foreground: var(--mw-text); +} + +/* ---------- the chrome, wearing the wiki ---------- */ +/* The body: index.css paints it #2b2b2b / white by media query; the + wiki's own ground wins that tie by specificity. */ +html[data-mathew-theme] body { + margin: 0; + font-family: 'Computer Modern', 'CMU Serif', Georgia, 'Times New Roman', serif; + background: var(--mw-bg); + color: var(--mw-text); +} + +/* Form controls answer to the system font unless told; the editor keeps + its monospace (the wiki sets its own code the same way). */ +html[data-mathew-theme] button, +html[data-mathew-theme] input, +html[data-mathew-theme] select, +html[data-mathew-theme] textarea { + font-family: inherit; +} + +/* The top bar: the wiki's hairline, and its menu row rounded to a chip */ +html[data-mathew-theme] nav { + border-bottom: 1px solid var(--mw-border); +} +html[data-mathew-theme] nav .nav-link, +html[data-mathew-theme] nav select { + border-radius: 8px; +} + +/* Syntax errors and warnings read in the wiki's danger red / amber */ +html[data-mathew-theme] .loading-ring:after { + border-color: var(--mw-accent) transparent var(--mw-accent) transparent; +} + +/* Selection, like the wiki's — accent wash, not system blue */ +html[data-mathew-theme] ::selection { + background: color-mix(in srgb, var(--mw-accent) 30%, transparent); +} + +/* Scrollbars, the wiki's subtle shape (mirrors its _base.scss) */ +html[data-mathew-theme] ::-webkit-scrollbar { + width: 11px; + height: 10px; +} +html[data-mathew-theme] ::-webkit-scrollbar-thumb { + background: color-mix(in srgb, var(--mw-text) 18%, transparent); + border-radius: 8px; + border: 3px solid transparent; + background-clip: content-box; +} +html[data-mathew-theme] ::-webkit-scrollbar-thumb:hover { + background: color-mix(in srgb, var(--mw-text) 30%, transparent); + background-clip: content-box; +} +html[data-mathew-theme] ::-webkit-scrollbar-track { + background: transparent; +} diff --git a/lean/theme/theme-init.js b/lean/theme/theme-init.js new file mode 100644 index 0000000..2e01958 --- /dev/null +++ b/lean/theme/theme-init.js @@ -0,0 +1,24 @@ +/* Mathew's theme handshake with the wiki (see mathew.css, its stylesheet). + * + * The wiki opens this frame as ?theme=light|dark — the editor cannot see + * the page around it (another origin), but it can at least open wearing + * the same mood. Without the parameter — a direct visit — the browser's + * preference decides, the same rule lean4web follows for its own default. + * + * Runs synchronously in , before the first paint, so the page never + * flashes the wrong palette; is the hook the + * stylesheet's overrides hang on. */ +(function () { + var param = null + try { + param = new URLSearchParams(window.location.search).get('theme') + } catch (e) { + /* an engine without URLSearchParams gets the fallback below */ + } + var theme = param === 'light' || param === 'dark' + ? param + : window.matchMedia && window.matchMedia('(prefers-color-scheme: dark)').matches + ? 'dark' + : 'light' + document.documentElement.setAttribute('data-mathew-theme', theme) +})()