Code review for leanprover-community/lean4web#116

Projects/MathlibDemo/leanweb-config.json

@@ -1,5 +1,6 @@
 {
-  "name": "Latest Mathlib",  "default": true,
+  "name": "Latest Mathlib",
+  "default": true,
   "hidden": false,
   "examples": [
     { "file": "MathlibDemo/Bijection.lean", "name": "Bijection" },

Projects/Stable/lean-toolchain

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

Projects/Stable/leanweb-build.sh

@@ -3,5 +3,6 @@
 # Operate in the directory where this file is located
 cd $(dirname $0)
 
+elan update stable
 lake update -R
 lake build

Projects/Stable/leanweb-config.json

@@ -1,4 +1,5 @@
 {
-  "name": "Stable Lean",
-  "hidden": false
+  "name": "Lean _Vers_",
+  "hidden": false,
+  "sortOrder": 10
 }

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, followed by projects with no given sort order  */
+  sortOrder: number
   /** A list of examples which are added under the menu `Examples` */
   examples: LeanWebExample[]
 }

client/src/store/project-atoms.ts

@@ -14,22 +14,15 @@ const projectsQueryAtom = atomWithQuery<LeanWebProject[]>(() => ({
 
 /**
  * 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 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
 
-  // 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) 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(1);
     cy.url().should("include", "project=Stable");
 
     cy.contains("div.view-line", payload).should("exist");

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,18 +40,22 @@ 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.
+  - `_Vers_`: this pattern inside the name will be replaced with the version from the toolchain
 - `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.
+- `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

@@ -71,13 +71,9 @@ app.use("/api/projects", async (req, res) => {
         ).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),
+          toolchainToName(toolchain),
         );
       } catch (err) {
         console.debug(err);
@@ -92,7 +88,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,
           },
         });
       }
@@ -472,13 +468,10 @@ function hasWorkingBwrap() {
   return test.status === 0;
 }
 
-function toolchainToName(toolchain, prefixLean) {
-  console.log(toolchain);
+function toolchainToName(toolchain) {
   const nightly = toolchain.match(/^leanprover\/lean4\:nightly-(.*)$/);
-  if (nightly) return prefixLean ? `Lean ${nightly[1]}` : nightly[1];
-  console.log(nightly);
+  if (nightly) return nightly[1];
   const release = toolchain.match(/^leanprover\/lean4\:(.*)$/);
-  console.log(release);
-  if (release) return prefixLean ? `Lean ${release[1]}` : release[1];
-  return "Lean";
+  if (release) return release[1];
+  return "";
 }

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