From 0045db87b4d42172e8fc40efd86cb3329af9f2ee Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 26 May 2026 20:17:01 -0400 Subject: [PATCH 1/7] validate project files, add order, insert version --- Projects/MathlibDemo/leanweb-config.json | 2 +- Projects/Stable/lean-toolchain | 2 +- Projects/Stable/leanweb-config.json | 2 +- client/src/api/project-types.ts | 2 ++ client/src/store/project-atoms.ts | 13 +++++++-- package-lock.json | 9 +++--- server/index.mjs | 37 ++++++++++++++++++++---- server/package.json | 3 +- server/types.mjs | 14 +++++++++ 9 files changed, 69 insertions(+), 15 deletions(-) create mode 100644 server/types.mjs diff --git a/Projects/MathlibDemo/leanweb-config.json b/Projects/MathlibDemo/leanweb-config.json index 95b3e57b..69683955 100644 --- a/Projects/MathlibDemo/leanweb-config.json +++ b/Projects/MathlibDemo/leanweb-config.json @@ -1,5 +1,5 @@ { - "name": "Latest Mathlib", + "name": "_LeanVers_ with Mathlib", "default": true, "hidden": false, "examples": [ diff --git a/Projects/Stable/lean-toolchain b/Projects/Stable/lean-toolchain index 7638861c..14791d72 100644 --- a/Projects/Stable/lean-toolchain +++ b/Projects/Stable/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:stable +leanprover/lean4:v4.29.0 diff --git a/Projects/Stable/leanweb-config.json b/Projects/Stable/leanweb-config.json index 167b9282..26c666fd 100644 --- a/Projects/Stable/leanweb-config.json +++ b/Projects/Stable/leanweb-config.json @@ -1,4 +1,4 @@ { - "name": "Stable Lean", + "name": "Stable Release (_Vers_ without Mathlib)", "hidden": false } diff --git a/client/src/api/project-types.ts b/client/src/api/project-types.ts index d5362b55..17be7f50 100644 --- a/client/src/api/project-types.ts +++ b/client/src/api/project-types.ts @@ -16,6 +16,8 @@ export type LeanWebProjectConfig = { hidden: boolean /** The default project. There must be exactly one project marked as default */ default: boolean + /** Sort order: the default project always comes first, followed by projects in increasing sort order, followed by projects with no given sort order */ + sortOrder: number | null /** A list of examples which are added under the menu `Examples` */ examples: LeanWebExample[] } diff --git a/client/src/store/project-atoms.ts b/client/src/store/project-atoms.ts index 4a4385c1..bd86a5fa 100644 --- a/client/src/store/project-atoms.ts +++ b/client/src/store/project-atoms.ts @@ -12,11 +12,20 @@ const projectsQueryAtom = atomWithQuery(() => ({ }, })) -/** Sort alphabetically while the `default` project always comes first */ +/** + * Sort alphabetically while the `default` project always comes first, then + * order by ascending sortOrder if it exists, then order by name. + */ function sortProjects(p: LeanWebProject, q: LeanWebProject): number { if (p.config.default) return -1 if (q.config.default) return 1 - return p.config.name.localeCompare(q.config.name) + if (p.config.sortOrder === null && q.config.sortOrder === null) { + return p.config.name.localeCompare(q.config.name) + } + if (p.config.sortOrder !== null && q.config.sortOrder !== null) + return p.config.sortOrder - q.config.sortOrder + if (q.config.sortOrder === null) return -1 + return 1 } /** All available projects */ diff --git a/package-lock.json b/package-lock.json index dab2fb78..57c760b1 100644 --- a/package-lock.json +++ b/package-lock.json @@ -12868,9 +12868,9 @@ } }, "node_modules/zod": { - "version": "4.3.6", - "resolved": "https://registry.npmjs.org/zod/-/zod-4.3.6.tgz", - "integrity": "sha512-rftlrkhHZOcjDwkGlnUtZZkvaPHCsDATp4pGpuOOMDaTdDDXF91wuVDJoWoPsKX/3YPQ5fHuF3STjcYyKr+Qhg==", + "version": "4.4.3", + "resolved": "https://registry.npmjs.org/zod/-/zod-4.4.3.tgz", + "integrity": "sha512-ytENFjIJFl2UwYglde2jchW2Hwm4GJFLDiSXWdTrJQBIN9Fcyp7n4DhxJEiWNAJMV1/BqWfW/kkg71UDcHJyTQ==", "license": "MIT", "funding": { "url": "https://github.com/sponsors/colinhacks" @@ -12896,7 +12896,8 @@ "ip-anonymize": "^0.1.0", "memfs": "^4.51.1", "nocache": "^4.0.0", - "ws": "^8.18.3" + "ws": "^8.18.3", + "zod": "^4.4.3" }, "bin": { "server": "index.mjs" diff --git a/server/index.mjs b/server/index.mjs index b0f63c8d..d3e6b9ba 100755 --- a/server/index.mjs +++ b/server/index.mjs @@ -12,6 +12,8 @@ import * as rpc from "vscode-ws-jsonrpc"; import * as jsonrpcserver from "vscode-ws-jsonrpc/server"; import { WebSocketServer } from "ws"; +import { zLeanWebProjectConfig } from "./types.mjs"; + let socketCounter = 0; function logStats() { @@ -59,11 +61,24 @@ app.use("/api/projects", async (req, res) => { const projectDir = path.join(PROJECTS_BASE_PATH, entry.name); const configPath = path.join(projectDir, "leanweb-config.json"); + const toolchainPath = path.join(projectDir, "lean-toolchain"); let config = null; try { const raw = await fs.promises.readFile(configPath, "utf-8"); - config = JSON.parse(raw); + const toolchain = ( + await fs.promises.readFile(toolchainPath, "utf-8") + ).trim(); + + config = zLeanWebProjectConfig.parse(JSON.parse(raw)); + config.name = config.name.replaceAll( + "_LeanVers_", + toolchainToName(toolchain, true), + ); + config.name = config.name.replaceAll( + "_Vers_", + toolchainToName(toolchain, false), + ); } catch (err) { console.debug(err); // File missing or invalid JSON — keep config as null @@ -73,10 +88,11 @@ app.use("/api/projects", async (req, res) => { projects.push({ folder: entry.name, config: { - name: String(config.name), // TODO: ensure this is not null - hidden: Boolean(config.hidden) ?? false, - default: Boolean(config.default) ?? false, - examples: config.examples ?? [], // TODO: validate + name: config.name, + hidden: config.hidden ?? false, + default: config.default ?? false, + examples: config.examples ?? [], + sortOrder: config.sortOrder ?? null, }, }); } @@ -455,3 +471,14 @@ function hasWorkingBwrap() { const test = cp.spawnSync("bwrap", ["--version"], { stdio: "ignore" }); return test.status === 0; } + +function toolchainToName(toolchain, prefixLean) { + console.log(toolchain); + const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/); + if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1]; + console.log(nightly); + const release = toolchain.match(/^leanprover\/lean4\:(.*)$/); + console.log(release); + if (release) return prefixLean ? `Lean ${release[1]}` : release[1]; + return "Lean"; +} diff --git a/server/package.json b/server/package.json index 480d71e4..56b8f836 100644 --- a/server/package.json +++ b/server/package.json @@ -15,7 +15,8 @@ "ip-anonymize": "^0.1.0", "memfs": "^4.51.1", "nocache": "^4.0.0", - "ws": "^8.18.3" + "ws": "^8.18.3", + "zod": "^4.4.3" }, "devDependencies": { "@types/node": "^24.10.1", diff --git a/server/types.mjs b/server/types.mjs new file mode 100644 index 00000000..f1496632 --- /dev/null +++ b/server/types.mjs @@ -0,0 +1,14 @@ +import { z } from "zod"; + +export const zLeanWebExample = z.object({ + file: z.string(), + name: z.string(), +}); + +export const zLeanWebProjectConfig = z.object({ + name: z.string(), + hidden: z.boolean().optional(), + default: z.boolean().optional(), + sortOrder: z.number().optional(), + examples: z.array(zLeanWebExample).optional(), +}); From d103e262d7ce3127420dda536dd1412acf6f901e Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 26 May 2026 20:24:51 -0400 Subject: [PATCH 2/7] revise sortProjects --- client/src/store/project-atoms.ts | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/client/src/store/project-atoms.ts b/client/src/store/project-atoms.ts index bd86a5fa..2ab19b6a 100644 --- a/client/src/store/project-atoms.ts +++ b/client/src/store/project-atoms.ts @@ -19,13 +19,18 @@ const projectsQueryAtom = atomWithQuery(() => ({ function sortProjects(p: LeanWebProject, q: LeanWebProject): number { if (p.config.default) return -1 if (q.config.default) return 1 - if (p.config.sortOrder === null && q.config.sortOrder === null) { - return p.config.name.localeCompare(q.config.name) + + // Secondary sort: sortOrder field + const ps = p.config.sortOrder + const qs = q.config.sortOrder + if (ps !== null && qs !== null && ps !== qs) { + return ps - qs } - if (p.config.sortOrder !== null && q.config.sortOrder !== null) - return p.config.sortOrder - q.config.sortOrder - if (q.config.sortOrder === null) return -1 - return 1 + if (ps !== null && qs === null) return -1 + if (ps === null && qs !== null) return 1 + + // Fallback: names + return p.config.name.localeCompare(q.config.name) } /** All available projects */ From e8efedbb7c528fc920ef8b20a0ddaccfb9b647a5 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 27 May 2026 17:58:13 -0400 Subject: [PATCH 3/7] rename project to un-confuse CI --- Projects/MathlibDemo/leanweb-config.json | 3 +-- Projects/Stable/leanweb-config.json | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Projects/MathlibDemo/leanweb-config.json b/Projects/MathlibDemo/leanweb-config.json index 69683955..58c1a478 100644 --- a/Projects/MathlibDemo/leanweb-config.json +++ b/Projects/MathlibDemo/leanweb-config.json @@ -1,6 +1,5 @@ { - "name": "_LeanVers_ with Mathlib", - "default": true, + "name": "Latest Mathlib", "default": true, "hidden": false, "examples": [ { "file": "MathlibDemo/Bijection.lean", "name": "Bijection" }, diff --git a/Projects/Stable/leanweb-config.json b/Projects/Stable/leanweb-config.json index 26c666fd..167b9282 100644 --- a/Projects/Stable/leanweb-config.json +++ b/Projects/Stable/leanweb-config.json @@ -1,4 +1,4 @@ { - "name": "Stable Release (_Vers_ without Mathlib)", + "name": "Stable Lean", "hidden": false } From a26fc2d68e96c4ce4118deb7f47269904c90d5b8 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 3 Jun 2026 13:52:02 -0400 Subject: [PATCH 4/7] Incorporate code review from @joneugster --- Projects/MathlibDemo/leanweb-config.json | 3 ++- Projects/Stable/leanweb-config.json | 2 +- client/src/api/project-types.ts | 4 ++-- client/src/store/project-atoms.ts | 11 +++-------- cypress/e2e/encoding.cy.ts | 2 +- cypress/e2e/spec.cy.ts | 6 +++++- doc/Projects.md | 15 +++++++++++++-- server/index.mjs | 4 +--- server/types.mjs | 2 +- 9 files changed, 29 insertions(+), 20 deletions(-) diff --git a/Projects/MathlibDemo/leanweb-config.json b/Projects/MathlibDemo/leanweb-config.json index 58c1a478..69683955 100644 --- a/Projects/MathlibDemo/leanweb-config.json +++ b/Projects/MathlibDemo/leanweb-config.json @@ -1,5 +1,6 @@ { - "name": "Latest Mathlib", "default": true, + "name": "_LeanVers_ with Mathlib", + "default": true, "hidden": false, "examples": [ { "file": "MathlibDemo/Bijection.lean", "name": "Bijection" }, diff --git a/Projects/Stable/leanweb-config.json b/Projects/Stable/leanweb-config.json index 167b9282..fc3e4cd2 100644 --- a/Projects/Stable/leanweb-config.json +++ b/Projects/Stable/leanweb-config.json @@ -1,4 +1,4 @@ { - "name": "Stable Lean", + "name": "_LeanVers_", "hidden": false } diff --git a/client/src/api/project-types.ts b/client/src/api/project-types.ts index 17be7f50..c66d7ed7 100644 --- a/client/src/api/project-types.ts +++ b/client/src/api/project-types.ts @@ -16,8 +16,8 @@ export type LeanWebProjectConfig = { hidden: boolean /** The default project. There must be exactly one project marked as default */ default: boolean - /** Sort order: the default project always comes first, followed by projects in increasing sort order, followed by projects with no given sort order */ - sortOrder: number | null + /** Sort order: the default project always comes first, followed by projects in decreasing sort order. (No sort order is treated as 0.) */ + sortOrder: number /** A list of examples which are added under the menu `Examples` */ examples: LeanWebExample[] } diff --git a/client/src/store/project-atoms.ts b/client/src/store/project-atoms.ts index 2ab19b6a..8db81c3f 100644 --- a/client/src/store/project-atoms.ts +++ b/client/src/store/project-atoms.ts @@ -14,20 +14,15 @@ const projectsQueryAtom = atomWithQuery(() => ({ /** * Sort alphabetically while the `default` project always comes first, then - * order by ascending sortOrder if it exists, then order by name. + * order by descending sortOrder (nullish treated as 0), then order by name. */ function sortProjects(p: LeanWebProject, q: LeanWebProject): number { if (p.config.default) return -1 if (q.config.default) return 1 // Secondary sort: sortOrder field - const ps = p.config.sortOrder - const qs = q.config.sortOrder - if (ps !== null && qs !== null && ps !== qs) { - return ps - qs - } - if (ps !== null && qs === null) return -1 - if (ps === null && qs !== null) return 1 + const n = q.config.sortOrder - p.config.sortOrder + if (n === 0) return n // Fallback: names return p.config.name.localeCompare(q.config.name) diff --git a/cypress/e2e/encoding.cy.ts b/cypress/e2e/encoding.cy.ts index 05456080..8a1370cd 100644 --- a/cypress/e2e/encoding.cy.ts +++ b/cypress/e2e/encoding.cy.ts @@ -15,7 +15,7 @@ describe("", () => { cy.get("div.view-lines").type(payload); // change project - cy.get("nav>*>select[name='leanVersion']").select("Stable Lean"); + cy.get("nav>*>select[name='leanVersion']").select(1); cy.url().should("include", "project=Stable"); cy.contains("div.view-line", payload).should("exist"); diff --git a/cypress/e2e/spec.cy.ts b/cypress/e2e/spec.cy.ts index c95eb75d..75283922 100644 --- a/cypress/e2e/spec.cy.ts +++ b/cypress/e2e/spec.cy.ts @@ -18,7 +18,11 @@ describe("The Editor", () => { cy.iframe().contains("Stable.lean").should("exist"); cy.get(".dropdown>.nav-link>.fa-bars").click(); cy.contains(".nav-link", "Lean Info").click(); - cy.containsAll(".modal", ["leanprover/lean4:stable", "(no dependencies)"]) + cy.containsAll(".modal", [ + "Stable", + "leanprover/lean4:", + "(no dependencies)", + ]) .find(".modal-close") .click(); }); diff --git a/doc/Projects.md b/doc/Projects.md index 7d72ea1c..56ec1a59 100644 --- a/doc/Projects.md +++ b/doc/Projects.md @@ -40,6 +40,7 @@ The file `leanweb-config.json` takes the following form: "name": "Display name", "default": false, "hidden": false, + "sortOrder": 0, "examples": [ { "file": "MathlibDemo/Bijection.lean", "name": "Example's display name" }, ... @@ -47,12 +48,22 @@ The file `leanweb-config.json` takes the following form: } ``` -- `name`: The display name of the project as shown in the dropdown menu +- `name`: The display name of the project as shown in the dropdown menu. The substrings `_Vers_` and + `_LeanVers_` in the project name will be replaced by indicators of which version is being used: + - If the toolchain is in a recognized format (a regular release like `v4.30.0-rc1` or nightly + release like `2026-04-04`), then `_Vers_` will be replaced by the version number (e.g. + `v4.30.0-rc1`) and `_LeanVers_` will be replaced by "Lean" followed by the version number (e.g. + `Lean v4.30.0-rc1`) + - If the toolchain is not in a recognized format, both `_Vers_` and `_LeanVers_` will be replaced + by "Lean". - `default`: There must be exactly one project with this set to `true`. This is the project loaded by default and when no project is specified in the url. - `hidden`: If set to `true`, then the project does not appear in the dropdown and can only be accessed via direct link. -- `examples`: list of examples. The path is relativ to the project's directory, e.g. `{PROJECTS_BASE_PATH}/{PROJECT_FOLDER}/{EXAMPLE_PATH.lean}` +- `sortOrder`(non-negative number): sort order of the projects in the dropdown. The default always + comes first, then projects with higher `sortOrder` value. Ties are resolved alphabetically. +- `examples`: list of examples. The path is relativ to the project's directory, e.g. + `{PROJECTS_BASE_PATH}/{PROJECT_FOLDER}/{EXAMPLE_PATH.lean}` ## automatic builds diff --git a/server/index.mjs b/server/index.mjs index d3e6b9ba..bc09aa1b 100755 --- a/server/index.mjs +++ b/server/index.mjs @@ -92,7 +92,7 @@ app.use("/api/projects", async (req, res) => { hidden: config.hidden ?? false, default: config.default ?? false, examples: config.examples ?? [], - sortOrder: config.sortOrder ?? null, + sortOrder: config.sortOrder ?? 0, }, }); } @@ -476,9 +476,7 @@ function toolchainToName(toolchain, prefixLean) { console.log(toolchain); const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/); if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1]; - console.log(nightly); const release = toolchain.match(/^leanprover\/lean4\:(.*)$/); - console.log(release); if (release) return prefixLean ? `Lean ${release[1]}` : release[1]; return "Lean"; } diff --git a/server/types.mjs b/server/types.mjs index f1496632..e889a9fe 100644 --- a/server/types.mjs +++ b/server/types.mjs @@ -9,6 +9,6 @@ export const zLeanWebProjectConfig = z.object({ name: z.string(), hidden: z.boolean().optional(), default: z.boolean().optional(), - sortOrder: z.number().optional(), + sortOrder: z.number().min(0).optional(), examples: z.array(zLeanWebExample).optional(), }); From c29792265e8bef316ecbeef83c59763fa9ec199d Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 3 Jun 2026 14:21:46 -0400 Subject: [PATCH 5/7] flip condition --- client/src/store/project-atoms.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/store/project-atoms.ts b/client/src/store/project-atoms.ts index 8db81c3f..5063895a 100644 --- a/client/src/store/project-atoms.ts +++ b/client/src/store/project-atoms.ts @@ -22,7 +22,7 @@ function sortProjects(p: LeanWebProject, q: LeanWebProject): number { // Secondary sort: sortOrder field const n = q.config.sortOrder - p.config.sortOrder - if (n === 0) return n + if (n !== 0) return n // Fallback: names return p.config.name.localeCompare(q.config.name) From a923be0c1a0b953317fcb2c6c0db0d66b82eae27 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 3 Jun 2026 14:23:22 -0400 Subject: [PATCH 6/7] remove console.log --- server/index.mjs | 1 - 1 file changed, 1 deletion(-) diff --git a/server/index.mjs b/server/index.mjs index bc09aa1b..d36bf266 100755 --- a/server/index.mjs +++ b/server/index.mjs @@ -473,7 +473,6 @@ function hasWorkingBwrap() { } function toolchainToName(toolchain, prefixLean) { - console.log(toolchain); const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/); if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1]; const release = toolchain.match(/^leanprover\/lean4\:(.*)$/); From b6bb4f3b037c3a262d4bd4470c44602682fc6452 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 3 Jun 2026 14:50:46 -0400 Subject: [PATCH 7/7] Test updates --- cypress/e2e/encoding.cy.ts | 2 +- cypress/e2e/settings.cy.ts | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/cypress/e2e/encoding.cy.ts b/cypress/e2e/encoding.cy.ts index 8a1370cd..e4c97492 100644 --- a/cypress/e2e/encoding.cy.ts +++ b/cypress/e2e/encoding.cy.ts @@ -15,7 +15,7 @@ describe("", () => { cy.get("div.view-lines").type(payload); // change project - cy.get("nav>*>select[name='leanVersion']").select(1); + cy.get("nav>*>select[name='leanVersion']").select("Stable"); cy.url().should("include", "project=Stable"); cy.contains("div.view-line", payload).should("exist"); diff --git a/cypress/e2e/settings.cy.ts b/cypress/e2e/settings.cy.ts index 282b38ac..aa2cfcb5 100644 --- a/cypress/e2e/settings.cy.ts +++ b/cypress/e2e/settings.cy.ts @@ -56,3 +56,19 @@ describe("The Settings can be changed for", () => { }); }); }); + +describe("The version selection menu", () => { + it("displays a versioned name for the MathlibDemo project", () => { + cy.visit("/"); + cy.get("nav>*>select[name='leanVersion'] option[value='MathlibDemo']") + .invoke("text") + .should("match", /^Lean v4\.[0-9]+\.[0-9]+(-rc[0-9]+)? with Mathlib/); + }); + + it("displays a versioned name for the Stable project", () => { + cy.visit("/"); + cy.get("nav>*>select[name='leanVersion'] option[value='Stable']") + .invoke("text") + .should("match", /^Lean v4\./); + }); +});