Validate project files, add order, insert version

Projects/MathlibDemo/leanweb-config.json

@@ -1,5 +1,5 @@
 {
-  "name": "Latest Mathlib",
+  "name": "_LeanVers_ with Mathlib",
   "default": true,
   "hidden": false,
   "examples": [

Projects/Stable/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:stable
+leanprover/lean4:v4.29.0

Projects/Stable/leanweb-config.json

@@ -1,4 +1,4 @@
 {
-  "name": "Stable Lean",
+  "name": "_LeanVers_",
   "hidden": false
 }

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 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[]
 }

client/src/store/project-atoms.ts

@@ -12,10 +12,19 @@ const projectsQueryAtom = atomWithQuery<LeanWebProject[]>(() => ({
   },
 }))
 
-/** Sort alphabetically while the `default` project always comes first */
+/**
+ * Sort alphabetically while the `default` project always comes first, then
+ * 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 n = q.config.sortOrder - p.config.sortOrder
+  if (n !== 0) return n
+
+  // Fallback: names
   return p.config.name.localeCompare(q.config.name)
 }
 

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("Stable");
     cy.url().should("include", "project=Stable");
 
     cy.contains("div.view-line", payload).should("exist");

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\./);
+  });
+});

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();
   });

doc/Projects.md

@@ -40,19 +40,30 @@ 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" },
     ...
   ]
 }
 ```
 
-- `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
 

server/index.mjs

@@ -12,6 +12,8 @@
 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 @@
 
       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 @@
         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 ?? 0,
           },
         });
       }
@@ -255,7 +271,7 @@
   }
   try {
     conn.send(JSON.stringify(message));
   } catch (e) {
     conn.close();
   }
 };
@@ -277,7 +293,7 @@
       pongReceived = false;
       try {
         conn.ping();
       } catch (e) {
         conn.close();
       }
     }
@@ -455,3 +471,11 @@
   const test = cp.spawnSync("bwrap", ["--version"], { stdio: "ignore" });
   return test.status === 0;
 }
+
+function toolchainToName(toolchain, prefixLean) {
+  const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/);
+  if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1];
+  const release = toolchain.match(/^leanprover\/lean4\:(.*)$/);
+  if (release) return prefixLean ? `Lean ${release[1]}` : release[1];
+  return "Lean";
+}

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",

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().min(0).optional(),
+  examples: z.array(zLeanWebExample).optional(),
+});