From 097160a6cd086305bdf5a3d8a248274e7e9abe88 Mon Sep 17 00:00:00 2001 From: Aran Roig Date: Mon, 19 Oct 2026 22:28:12 +0200 Subject: [PATCH] jdsjkdjk --- .gitea/workflows/deploy.yml | 10 ++++++---- AGENTS.md | 11 +++++++++-- README.md | 7 ++++--- docker-compose.yml | 14 +++++++++----- lean/README.md | 24 ++++++++++++++++-------- lean/entrypoint.sh | 20 +++++++++++++++++--- nginx.conf | 31 +++++++++++++++++++++++++++++++ 7 files changed, 92 insertions(+), 25 deletions(-) diff --git a/.gitea/workflows/deploy.yml b/.gitea/workflows/deploy.yml index 62c3577..be674c3 100644 --- a/.gitea/workflows/deploy.yml +++ b/.gitea/workflows/deploy.yml @@ -48,8 +48,7 @@ jobs: echo "lean=$lean" >> "$GITHUB_OUTPUT" echo "app=$app lean=$lean" - # The wiki app itself. Its deploy (`compose pull && up -d`) also pulls - # whatever mathew-lean:latest the registry holds — the lean job keeps it current. + # The wiki app itself — its deploy step never touches the lean service. deploy: runs-on: docker needs: changes @@ -91,13 +90,16 @@ jobs: scp docker-compose.yml deploy@${{ secrets.DEPLOY_HOST }}:/var/www/app/ scp nginx.conf deploy@${{ secrets.DEPLOY_HOST }}:/var/www/app/nginx.conf + # Scoped to the services this job owns: never pulls/builds lean from + # here (that would need the lean tag or lean/ sources on the host). + # deploy-lean.yml owns the lean service's pull and up. - name: Deploy run: | ssh deploy@${{ secrets.DEPLOY_HOST }} << 'EOF' echo "${{ secrets.REGISTRY_PASSWORD }}" | docker login git.aranroig.com -u "${{ secrets.REGISTRY_USER }}" --password-stdin cd /var/www/app/ - docker compose pull - docker compose up -d --remove-orphans + docker compose pull nginx frontend backend + docker compose up -d frontend backend nginx EOF # The Lean editor (lean4web): multi-stage, heavy by nature (it fetches diff --git a/AGENTS.md b/AGENTS.md index f601196..b3311fc 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -43,7 +43,11 @@ Frontend API URL comes from `NUXT_PUBLIC_API_BASE` (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 +address too, or the browser blocks it (and the `wss://` derived from it) as mixed content (see `lean/README.md`). Production +passes `https://mathew.aranroig.com/api/lean`: nginx strips the `/api/lean` prefix and +proxies the rest to `lean:8080`, so the editor's websocket rides the site's own origin +instead of a public port 8080 (the compose service binds that port to the host's +loopback, for dev only). 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 @@ -447,7 +451,10 @@ copy + an `APP_LANGUAGES` entry + the code in the backend's `SUPPORTED_LOCALES`. 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). + Lean server refuses an https wiki outright). Production uses + `https://mathew.aranroig.com/api/lean`, which `nginx.conf` proxies to `lean:8080`; the + bundled classic lean4web client still assumes it is served from a root, so behind + `/api/lean` the status bar's link opens a page whose assets 404. 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. diff --git a/README.md b/README.md index c487406..96cc1bd 100644 --- a/README.md +++ b/README.md @@ -206,10 +206,11 @@ 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 +Lean language protocol to it directly. Production serves it through nginx at +`https://mathew.aranroig.com/api/lean` (`NUXT_PUBLIC_LEAN_URL`); the container's own +8080 is bound to the host loopback for development, not published. 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). +accordingly. ## Notes for contributors diff --git a/docker-compose.yml b/docker-compose.yml index f842218..1192ef5 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -15,10 +15,11 @@ 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} + # Where the browser finds the Lean editor server: the site's own https + # origin, proxied to the lean service by nginx (/api/lean). An https:// + # site needs an https:// address here — the websocket's wss:// is derived + # from it, and an http:// server would be refused as mixed content. + NUXT_PUBLIC_LEAN_URL: ${NUXT_PUBLIC_LEAN_URL:-https://mathew.aranroig.com/api/lean} restart: always # The Lean editor (lean4web) — its own server, since it runs a real Lean @@ -33,8 +34,11 @@ services: # args: # BAKE_MATHLIB: "false" image: git.aranroig.com/syndria98/mathew-lean:latest + # Reachable only from this host (dev's frontend) and nginx; the public way + # in is https://mathew.aranroig.com/api/lean. Publishing the port would + # hand anyone on the internet a Lean shell — see lean/README.md. ports: - - "8080:8080" + - "127.0.0.1:8080:8080" restart: always # Only with BAKE_MATHLIB: "false" above: # volumes: diff --git a/lean/README.md b/lean/README.md index 583eb1a..bc3948a 100644 --- a/lean/README.md +++ b/lean/README.md @@ -61,13 +61,16 @@ The `BAKE_MATHLIB=false` image still ships the pinned elan toolchain, but not the project's `.lake`: the entrypoint notices a fresh volume and fills it once at first start — `lake update` fetches the sources pinned in `lake-manifest.json`, Mathlib's post-update hook downloads the matching -precompiled cache, `lake build` writes the project's own module. Expect ~10 -minutes and a few hundred MB of download; restarts after that are instant, -and **image rebuilds never touch Mathlib again** (the volume stays). The -trade: the cache must survive on the host, first start needs network, and it -redoes once if you recreate with a clean volume — hence the default staying -`BAKE_MATHLIB=true`. The commented blocks in `docker-compose.yml` wire this -up for the production stack. +precompiled cache, `lake build` writes the project's own module. The manifest +`lake update` resolved gets saved into the volume and re-applied at every +start, so the packages in the volume and the manifest in the image never tell +different stories (an unsynced pair would try to re-fetch Mathlib from GitHub +at each session). Expect ~10 minutes and a few hundred MB of download; +restarts after that are instant, and **image rebuilds never touch Mathlib +again** (the volume stays). The trade: the cache must survive on the host, +first start needs network, and it redoes once if you recreate with a clean +volume — hence the default staying `BAKE_MATHLIB=true`. The commented blocks +in `docker-compose.yml` wire this up for the production stack. ## The protocol the wiki's client speaks @@ -138,7 +141,12 @@ 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. +`NUXT_PUBLIC_LEAN_URL` at the `https://` address. The production stack does +the latter: nginx serves it at `https://mathew.aranroig.com/api/lean` and +proxies to `lean:8080`; the compose service publishes 8080 on loopback only +(dev's frontend), so the public way in is that one address. Note that the +bundled classic client expects to sit at the server root — under `/api/lean` +its assets resolve against the wiki and 404; the wiki's own editor is fine. ## Updating diff --git a/lean/entrypoint.sh b/lean/entrypoint.sh index e4c2f1f..192b6a8 100644 --- a/lean/entrypoint.sh +++ b/lean/entrypoint.sh @@ -8,19 +8,33 @@ # "Keeping Mathlib out of the image"), the project's .lake is meant to be a # volume: a fresh one gets filled once, at first start, so Mathlib's ~7GB of # compiled cache never travels through the registry. +# +# The manifest pairing matters: `lake update` advances the packages in .lake +# AND rewrites lake-manifest.json — but the manifest sits in the (ephemeral) +# image while the packages sit in the (permanent) volume. Without help, a new +# container would find manifest ≠ volume and try to re-sync Mathlib from +# GitHub at every session. So the first start saves the manifest it resolved +# into the volume, and every later start puts that saved copy over the +# image's — manifest and packages always tell the same story. set -eu PROJECT=/opt/lean4web/Projects/MathlibDemo +MANIFEST="$PROJECT/lake-manifest.json" +SAVED_MANIFEST="$PROJECT/.lake/mathew-lake-manifest.json" + +if [ -f "$SAVED_MANIFEST" ]; then + cp "$SAVED_MANIFEST" "$MANIFEST" +fi if [ ! -f "$PROJECT/.lake/build/lib/lean/MathlibDemo.olean" ]; then echo "[mathew-lean] $PROJECT/.lake holds no built Mathlib — fetching it once (expect ~10 minutes)" - cd "$PROJECT" # lake update pulls the sources pinned in lake-manifest.json, and Mathlib's # post-update hook fetches the matching precompiled cache; lake build then # only writes the project's own module. The image's pinned toolchain # (elan) stays as it is — no lean-toolchain re-curl, no surprise downloads. - lake update -R - lake build + # (subshell: its cd must not leak into the server's working directory) + ( cd "$PROJECT" && lake update -R && lake build ) + cp "$MANIFEST" "$SAVED_MANIFEST" echo "[mathew-lean] Mathlib ready" fi diff --git a/nginx.conf b/nginx.conf index 969813c..cbfc94c 100644 --- a/nginx.conf +++ b/nginx.conf @@ -10,6 +10,37 @@ http { listen 80; server_name _; + # The Lean editor server, at the site's own https origin instead of a + # bare :8080 (NUXT_PUBLIC_LEAN_URL points here). Longest-prefix wins, + # so this beats /api below. lean4web serves from its root, so the + # /api/lean prefix is stripped before proxying: the wiki's client asks + # for /api/lean/websocket/ and /api/lean/api/projects. + location = /api/lean { + # relative Location: the outer TLS proxy's scheme/host stay the + # browser's (an absolute redirect would say http://) + absolute_redirect off; + return 301 /api/lean/; + } + + location /api/lean/ { + set $lean_upstream lean:8080; + # `break` ends the rewrite phase, so the variable above is set first + rewrite ^/api/lean/(.*)$ /$1 break; + proxy_pass http://$lean_upstream; + + proxy_http_version 1.1; + proxy_set_header Host $host; + proxy_set_header X-Real-IP $remote_addr; + proxy_set_header X-Forwarded-For $proxy_add_x_forwarded_for; + proxy_set_header X-Forwarded-Proto $scheme; + proxy_set_header Upgrade $http_upgrade; + proxy_set_header Connection "upgrade"; + # A Lean session can sit idle while the reader thinks; the 60s + # default would drop its websocket. + proxy_read_timeout 1h; + proxy_send_timeout 1h; + } + # Api Requests ("/api" without a trailing slash must land here too, # or it falls through to the frontend and loops through its SSR proxy) location /api {