From 672d45fb921219085696d5f03122bfdd2bd08986 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Aug 2026 22:41:50 +0200 Subject: [PATCH 1/6] update ci --- .github/workflows/ci.yml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3846fefe..becdb0bc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -24,6 +24,7 @@ jobs: os: - ubuntu-latest - macos-latest + - windows-latest browser: - chrome include: @@ -35,10 +36,10 @@ jobs: uses: browser-actions/setup-firefox@v1 - name: Checkout repository - uses: actions/checkout@v6 + uses: actions/checkout@v7 - name: Setup Node.js - uses: actions/setup-node@v6 + uses: actions/setup-node@7 with: node-version: ${{ env.NODE_VERSION }} @@ -81,7 +82,7 @@ jobs: - name: Upload screenshots on failure if: failure() && steps.cypress_no_video.conclusion == 'failure' - uses: actions/upload-artifact@v6 + uses: actions/upload-artifact@7 with: name: cypress-screenshots-${{ matrix.os }}-${{ matrix.browser }} path: cypress/screenshots @@ -97,7 +98,7 @@ jobs: - name: Upload videos if: failure() && steps.cypress_no_video.conclusion == 'failure' - uses: actions/upload-artifact@v6 + uses: actions/upload-artifact@v7 with: name: cypress-videos-${{ matrix.os }}-${{ matrix.browser }} path: cypress/videos @@ -119,7 +120,7 @@ jobs: - name: Upload screenshots on failure if: runner.os == 'Linux' && failure() && steps.cypress_production_no_video.conclusion == 'failure' - uses: actions/upload-artifact@v6 + uses: actions/upload-artifact@v7 with: name: cypress-screenshots-production-${{ matrix.os }}-${{ matrix.browser }} path: cypress/screenshots @@ -134,7 +135,7 @@ jobs: - name: Upload screenshots on failure if: matrix.os == 'ubuntu-latest' &&matrix.browser == 'chromium' && failure() && steps.cypress_production_windows_no_video.conclusion == 'failure' - uses: actions/upload-artifact@v6 + uses: actions/upload-artifact@7 with: name: cypress-screenshots-production-windows-${{ matrix.os }}-${{ matrix.browser }} path: cypress/screenshots @@ -143,9 +144,9 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout repository - uses: actions/checkout@v6 + uses: actions/checkout@v7 - name: Setup Node.js - uses: actions/setup-node@v6 + uses: actions/setup-node@v7 with: node-version: ${{ env.NODE_VERSION }} - name: Install dependencies From a1f3b39ac3381bdc1941ff1061898522fc2ce015 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Aug 2026 22:45:03 +0200 Subject: [PATCH 2/6] fix --- .github/workflows/ci.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index becdb0bc..af853bc5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -39,7 +39,7 @@ jobs: uses: actions/checkout@v7 - name: Setup Node.js - uses: actions/setup-node@7 + uses: actions/setup-node@v7 with: node-version: ${{ env.NODE_VERSION }} @@ -82,7 +82,7 @@ jobs: - name: Upload screenshots on failure if: failure() && steps.cypress_no_video.conclusion == 'failure' - uses: actions/upload-artifact@7 + uses: actions/upload-artifact@v7 with: name: cypress-screenshots-${{ matrix.os }}-${{ matrix.browser }} path: cypress/screenshots @@ -135,7 +135,7 @@ jobs: - name: Upload screenshots on failure if: matrix.os == 'ubuntu-latest' &&matrix.browser == 'chromium' && failure() && steps.cypress_production_windows_no_video.conclusion == 'failure' - uses: actions/upload-artifact@7 + uses: actions/upload-artifact@v7 with: name: cypress-screenshots-production-windows-${{ matrix.os }}-${{ matrix.browser }} path: cypress/screenshots From 3a12dcfdbfdd7d888d4d2a3b2d2b175cd833f3c9 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Aug 2026 22:51:01 +0200 Subject: [PATCH 3/6] switch for windows --- .github/workflows/ci.yml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index af853bc5..4347c587 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -55,18 +55,30 @@ jobs: lint: false - name: Build sample projects + if: runner.os != 'Windows' run: npm run build:projects - name: Ensure sample project 'MathlibDemo' is built + if: runner.os != 'Windows' run: | cd Projects/MathlibDemo lake build --no-build - name: Ensure sample project 'Stable' is built + if: runner.os != 'Windows' run: | cd Projects/Stable lake build --no-build + - name: Manually building projects on Windows + if: runner.os == 'Windows' + run: | + cd Projects/MathlibDemo + lake exe cache get + lake build + cd ../Stable + lake build + - name: Install dependencies run: npm ci From afeb817524f1debcb675bbee222ccc383952d333 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Aug 2026 22:54:08 +0200 Subject: [PATCH 4/6] wording --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4347c587..43cb47fb 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -70,7 +70,7 @@ jobs: cd Projects/Stable lake build --no-build - - name: Manually building projects on Windows + - name: Build sample projects (Windows) if: runner.os == 'Windows' run: | cd Projects/MathlibDemo From 1689b8d0c75464fd4388f74c5dc65f433b360f12 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Aug 2026 23:02:31 +0200 Subject: [PATCH 5/6] update doc --- doc/Installation.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/doc/Installation.md b/doc/Installation.md index 2e4c7e91..2bb3ba06 100644 --- a/doc/Installation.md +++ b/doc/Installation.md @@ -49,15 +49,21 @@ On a running system, you might already have these installed, if not: ### Installation - Clone this repo: + ``` git clone --recurse-submodules https://github.com/leanprover-community/lean4web.git ``` + note that `--recurse-submodules` is needed to load the predefined projects in `Projects/`. (on an existing clone, you can call `git submodule init` and `git submodule update`) + - Navigate into the cloned repository + ``` cd lean4web ``` + - Install dependencies + ``` npm install ``` @@ -65,31 +71,45 @@ On a running system, you might already have these installed, if not: ### Development mode - Start the project in development mode + ``` npm start ``` + - Go to http://localhost:3000 ### Production mode - Compile the project + ``` npm run build ``` + + On Windows, the subcommand `npm run build:projects` might not work as it is implemented with Bash-Scripts. You can call `npm run build:client` instead and have your own logic to build all Lean projects (e.g. call `lake build` inside each project). + - Start the server + ``` npm run prod ``` + - To disable the bubblewrap containers, start the server with + ``` NO_BWRAP=true npm run prod ``` + - Start the client seperately, for example with + ``` npm run start:client ``` + and open http://localhost:3000 + - To set the locations of SSL certificates, use the following environment variables: + ``` SSL_CRT_FILE=/path/to/crt_file.cer SSL_KEY_FILE=/path/to/private_ssl_key.pem npm run prod ``` From b4f6232e65965ae188756a64c6d74a10ed3e4da6 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Aug 2026 23:12:58 +0200 Subject: [PATCH 6/6] cross-env --- client/package.json | 7 ++++--- package-lock.json | 31 +++++++++++++++++++++++++------ server/package.json | 5 +++-- 3 files changed, 32 insertions(+), 11 deletions(-) diff --git a/client/package.json b/client/package.json index 3a0d4055..3fe8742d 100644 --- a/client/package.json +++ b/client/package.json @@ -3,9 +3,9 @@ "private": true, "type": "module", "scripts": { - "analyse": "NODE_OPTIONS=--max-old-space-size=8192 npx vite-bundle-analyzer", - "dev": "NODE_ENV=development vite --host", - "build": "NODE_ENV=production vite build" + "analyse": "cross-env NODE_OPTIONS=--max-old-space-size=8192 npx vite-bundle-analyzer", + "dev": "cross-env NODE_ENV=development vite --host", + "build": "cross-env NODE_ENV=production vite build" }, "dependencies": { "@emotion/react": "^11.14.0", @@ -16,6 +16,7 @@ "@tailwindcss/vite": "^4.1.18", "@tanstack/query-core": "^5.90.14", "@uiw/react-codemirror": "^4.25.3", + "cross-env": "^10.1.0", "file-saver": "^2.0.5", "focus-trap-react": "^12.0.3", "jotai": "^2.16.1", diff --git a/package-lock.json b/package-lock.json index 6bb2b2a4..b679c482 100644 --- a/package-lock.json +++ b/package-lock.json @@ -44,6 +44,7 @@ "@tailwindcss/vite": "^4.1.18", "@tanstack/query-core": "^5.90.14", "@uiw/react-codemirror": "^4.25.3", + "cross-env": "^10.1.0", "file-saver": "^2.0.5", "focus-trap-react": "^12.0.3", "jotai": "^2.16.1", @@ -920,6 +921,12 @@ "integrity": "sha512-snKqtPW01tN0ui7yu9rGv69aJXr/a/Ywvl11sUjNtEcRc+ng/mQriFL0wLXMef74iHa/EkftbDzU9F8iFbH+zg==", "license": "MIT" }, + "node_modules/@epic-web/invariant": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/@epic-web/invariant/-/invariant-1.0.0.tgz", + "integrity": "sha512-lrTPqgvfFQtR/eY/qkIzp98OGdNJu0m5ji3q/nJI8v3SXkRKEnWiOxMmbvcSoAIzv/cGiuvRy57k4suKQSAdwA==", + "license": "MIT" + }, "node_modules/@esbuild/aix-ppc64": { "version": "0.28.1", "resolved": "https://registry.npmjs.org/@esbuild/aix-ppc64/-/aix-ppc64-0.28.1.tgz", @@ -5818,11 +5825,27 @@ "integrity": "sha512-VQ2MBenTq1fWZUH9DJNGti7kKv6EeAuYr3cLwxUWhIu1baTaXh4Ib5W2CqHVqib4/MqbYGJqiL3Zb8GJZr3l4g==", "license": "MIT" }, + "node_modules/cross-env": { + "version": "10.1.0", + "resolved": "https://registry.npmjs.org/cross-env/-/cross-env-10.1.0.tgz", + "integrity": "sha512-GsYosgnACZTADcmEyJctkJIoqAhHjttw7RsFrVoJNXbsWWqaq6Ym+7kZjq6mS45O0jij6vtiReppKQEtqWy6Dw==", + "license": "MIT", + "dependencies": { + "@epic-web/invariant": "^1.0.0", + "cross-spawn": "^7.0.6" + }, + "bin": { + "cross-env": "dist/bin/cross-env.js", + "cross-env-shell": "dist/bin/cross-env-shell.js" + }, + "engines": { + "node": ">=20" + } + }, "node_modules/cross-spawn": { "version": "7.0.6", "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.6.tgz", "integrity": "sha512-uV2QOWP2nWzsy2aMp8aRibhi9dlzF5Hgh5SHaB9OiTGEyDTiJJyx0uy51QXdyWbtAHNua4XJzUKca3OzKUd3vA==", - "dev": true, "license": "MIT", "dependencies": { "path-key": "^3.1.0", @@ -7759,7 +7782,6 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/isexe/-/isexe-2.0.0.tgz", "integrity": "sha512-RHxMLp9lnKHGHRng9QFhRCMbYAcVpn69smSGcq3f36xjgVVWThj4qqLbTLlq7Ssj8B+fIQ1EuCEGI2lKsyQeIw==", - "dev": true, "license": "ISC" }, "node_modules/isomorphic-timers-promises": { @@ -9599,7 +9621,6 @@ "version": "3.1.1", "resolved": "https://registry.npmjs.org/path-key/-/path-key-3.1.1.tgz", "integrity": "sha512-ojmeN0qd+y0jszEtoY48r0Peq5dwMEkIlCOu6Q5f41lfkswXuKtYrhgoTpLnyIcHm24Uhqx+5Tqm2InSwLhE6Q==", - "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -10468,7 +10489,6 @@ "version": "2.0.0", "resolved": "https://registry.npmjs.org/shebang-command/-/shebang-command-2.0.0.tgz", "integrity": "sha512-kHxr2zZpYtdmrN1qDjrrX/Z1rR1kG8Dx+gkpK1G4eXmvXswmcE1hTWBWYUzlraYw1/yZp6YuDY77YtvbN0dmDA==", - "dev": true, "license": "MIT", "dependencies": { "shebang-regex": "^3.0.0" @@ -10481,7 +10501,6 @@ "version": "3.0.0", "resolved": "https://registry.npmjs.org/shebang-regex/-/shebang-regex-3.0.0.tgz", "integrity": "sha512-7++dFhtcx3353uBaq8DDR4NuxBetBzC7ZQOhmTQInHEd6bSrXdiEyzCvG07Z44UYdLShWUyXt5M/yhz8ekcb1A==", - "dev": true, "license": "MIT", "engines": { "node": ">=8" @@ -11813,7 +11832,6 @@ "version": "2.0.2", "resolved": "https://registry.npmjs.org/which/-/which-2.0.2.tgz", "integrity": "sha512-BLI3Tl1TW3Pvl70l3yq3Y64i+awpwXqsGBYWkkqMtnbXgrMD+yj7rhW0kuEDxzJaYXGjEW5ogapKNMEKNMjibA==", - "dev": true, "license": "ISC", "dependencies": { "isexe": "^2.0.0" @@ -12078,6 +12096,7 @@ "server": { "name": "@leanweb/server", "dependencies": { + "cross-env": "^10.1.0", "express": "^5.1.0", "ip-anonymize": "^0.1.0", "memfs": "^4.51.1", diff --git a/server/package.json b/server/package.json index f233d91b..07e258fe 100644 --- a/server/package.json +++ b/server/package.json @@ -6,12 +6,13 @@ }, "type": "module", "scripts": { - "dev": "NODE_ENV=development nodemon index.mjs", - "prod": "NODE_ENV=production nodemon index.mjs", + "dev": "cross-env NODE_ENV=development nodemon index.mjs", + "prod": "cross-env NODE_ENV=production nodemon index.mjs", "build": "echo 'deprecated, use build:projects instead' && npm run build:projects", "build:projects": "./build.sh" }, "dependencies": { + "cross-env": "^10.1.0", "express": "^5.1.0", "ip-anonymize": "^0.1.0", "memfs": "^4.51.1",