chore: fix version in lakefile and add CI check

.github/workflows/check-nightly-revs.yml

@@ -0,0 +1,27 @@
+on:
+    push:
+        branches:
+            - main
+    pull_request:
+        branches:
+            - main
+    merge_group:
+
+name: "Check dependency revisions"
+
+jobs:
+    check:
+        name: Forbid nightly dependency revisions on main
+        runs-on: ubuntu-latest
+        # Merge queues may serve branches where nightly revisions are expected,
+        # so restrict merge_group runs to those targeting main.
+        if: github.event_name != 'merge_group' || github.event.merge_group.base_ref == 'refs/heads/main'
+        steps:
+            - uses: actions/checkout@v4
+
+            - name: Check lakefile for nightly revisions
+              run: |
+                  if grep -nE '@"[^"]*nightly[^"]*"' lakefile.lean; then
+                      echo '::error file=lakefile.lean::lakefile.lean pins a dependency to a nightly revision. On main, dependencies must track a stable branch such as main.'
+                      exit 1
+                  fi

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f62e380bcf8e11a2df70697916c8333bafdf3540",
+   "rev": "d6127db3a003afaa497fdcbf9c84ce2f4df74446",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/illuminate",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
+   "rev": "123d15766ba49356c02ebad2a4462dfe12d79899",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "859ab80c32c5851151919a7d757d7c0c0b6e39d2",
+   "rev": "4343da18d95390b09fde98efb18125677c4b500c",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -10,7 +10,7 @@ open System (FilePath)
 
 require versowebcomponents from git "https://github.com/leanprover/verso-web-components"@"main"
 require illuminate from git "https://github.com/leanprover/illuminate"@"main"
-require verso from git "https://github.com/leanprover/verso.git"@"nightly-testing"
+require verso from git "https://github.com/leanprover/verso.git"@"main"
 
 
 open Lean System in