From 4d5aae838ab674576da50466ac0b7377cc5e32f4 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Thu, 6 Aug 2026 19:18:50 +0200
Subject: [PATCH] chore: fix version in lakefile and add CI check

main should not depend on nightlies, but it's easy for this to slip
through with our process for keeping up to date.
---
 .github/workflows/check-nightly-revs.yml | 27 ++++++++++++++++++++++++
 lake-manifest.json                       |  8 +++----
 lakefile.lean                            |  2 +-
 3 files changed, 32 insertions(+), 5 deletions(-)
 create mode 100644 .github/workflows/check-nightly-revs.yml

diff --git a/.github/workflows/check-nightly-revs.yml b/.github/workflows/check-nightly-revs.yml
new file mode 100644
index 000000000..952d0dcc5
--- /dev/null
+++ b/.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
diff --git a/lake-manifest.json b/lake-manifest.json
index c1784f6de..7e250998d 100644
--- a/lake-manifest.json
+++ b/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",
diff --git a/lakefile.lean b/lakefile.lean
index 310b96df8..5cc6d86cf 100644
--- a/lakefile.lean
+++ b/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