chore: update release scripts

script/release/checklist.py

@@ -55,10 +55,9 @@ def check_pr(self, base: str, head: str, title: str) -> bool:
 
         if pr.merged:
             self.cl.success(f"PR merged: {util.fmt_pr(pr)}")
-        else:
-            self.cl.success(f"PR closed: {util.fmt_pr(pr)}")
+            return True
 
-        return True
+        return False
 
     def create_pr(
         self, base: str, head: str, title: str, nightly: ReleaseRepo | None = None
@@ -130,6 +129,8 @@ def _bump_toolchain_deps(self, path: Path) -> None:
         util.run("lake", "update", cwd=path)
 
     def _bump_toolchain_mathlib4(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
+
         pw = self.github.get_repo(repos.PROOFWIDGETS4.gh_full_name)
         tag = util.get_proofwidgets_release_for(pw, self.version)
         if not tag:
@@ -151,7 +152,30 @@ def _bump_toolchain_mathlib4(self) -> None:
 
         self._bump_toolchain_deps(self.lrepo.path)
 
+    def _bump_toolchain_cslib(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
+
+        mathlib_sha = util.find_merged_toolchain_bump_sha(
+            repos.MATHLIB4.local, self.version
+        )
+
+        util.edit(
+            self.lrepo.path / "lakefile.toml",
+            r'(name = "mathlib"\nscope = "leanprover-community"\nrev =) ".+?"',
+            rf'\1 "{mathlib_sha}"',
+        )
+
+        # For rc1 PRs
+        util.edit(
+            self.lrepo.path / "lakefile.toml",
+            r'name = "mathlib"\ngit = ".*"\nrev = ".+?"',
+            f'name = "mathlib"\nscope = "leanprover-community"\nrev = "{mathlib_sha}"',
+        )
+
+        self._bump_toolchain_deps(self.lrepo.path)
+
     def _bump_toolchain_repl(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
         self._bump_toolchain_deps(self.lrepo.path)
 
         mathlib = self.lrepo.path / "test" / "Mathlib"
@@ -171,10 +195,15 @@ def _bump_toolchain_repl(self) -> None:
                 raise e
 
     def _bump_toolchain_verso(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
         self._bump_toolchain_deps(self.lrepo.path)
         util.run("./update-subverso.sh", cwd=self.lrepo.path)
 
+    def _bump_toolchain_verso_templates(self) -> None:
+        util.run("./update-lean-version.sh", self.version.raw, cwd=self.lrepo.path)
+
     def _bump_toolchain_reference_manual(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
         self._bump_toolchain_deps(self.lrepo.path)
 
         if not self.prompt("Run release notes update script"):
@@ -188,18 +217,16 @@ def _bump_toolchain_reference_manual(self) -> None:
         self.prompt("Check release notes before commit")
 
     def _bump_toolchain_lean_fro_org(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
         self._bump_toolchain_deps(self.lrepo.path)
-
-        hero = self.lrepo.path / "examples" / "hero"
-        self._bump_toolchain(hero)
-        self._bump_toolchain_deps(hero)
-
         util.run("scripts/update.sh", cwd=self.lrepo.path)
 
     def _bump_toolchain_bibtex_query(self) -> None:
+        self._bump_toolchain(self.lrepo.path)
+
         lub = self.github.get_repo(repos.LEAN4_UNICODE_BASIC.gh_full_name)
         tag = util.get_lean_unicode_basic_release_for(lub, self.version)
-        rev = str(tag) if tag else "main"
+        rev = tag.name if tag else "main"
 
         util.edit(
             self.lrepo.path / "lakefile.toml",
@@ -209,24 +236,38 @@ def _bump_toolchain_bibtex_query(self) -> None:
 
         self._bump_toolchain_deps(self.lrepo.path)
 
-    def _bump_toolchain_in_worktree(self) -> None:
+    def _bump_toolchain_leansqlite(self) -> None:
         self._bump_toolchain(self.lrepo.path)
+        self._bump_toolchain_deps(self.lrepo.path)
+
+        tests = self.lrepo.path / "tests"
+        self._bump_toolchain(tests)
+        self._bump_toolchain_deps(tests)
 
-        # Special cases
+    def _bump_toolchain_in_worktree(self) -> None:
         if self.rrepo.gh_full_name == repos.MATHLIB4.gh_full_name:
             self._bump_toolchain_mathlib4()
+        elif self.rrepo.gh_full_name == repos.CSLIB.gh_full_name:
+            self._bump_toolchain_cslib()
         elif self.rrepo.gh_full_name == repos.REPL.gh_full_name:
             self._bump_toolchain_repl()
         elif self.rrepo.gh_full_name == repos.VERSO.gh_full_name:
             self._bump_toolchain_verso()
+        elif self.rrepo.gh_full_name == repos.VERSO_TEMPLATES.gh_full_name:
+            self._bump_toolchain_verso_templates()
         elif self.rrepo.gh_full_name == repos.REFERENCE_MANUAL.gh_full_name:
             self._bump_toolchain_reference_manual()
         elif self.rrepo.gh_full_name == repos.LEAN_FRO_ORG.gh_full_name:
             self._bump_toolchain_lean_fro_org()
         elif self.rrepo.gh_full_name == repos.BIBTEX_QUERY.gh_full_name:
             self._bump_toolchain_bibtex_query()
+        elif self.rrepo.gh_full_name == repos.LEANSQLITE.gh_full_name:
+            self._bump_toolchain_leansqlite()
         elif self.rrepo.strong_deps:
+            self._bump_toolchain(self.lrepo.path)
             self._bump_toolchain_deps(self.lrepo.path)
+        else:
+            self._bump_toolchain(self.lrepo.path)
 
     def _bump_toolchain_unicode_basic(self) -> None:
         base = self.grepo.default_branch
@@ -566,8 +607,11 @@ def check_master_branch_cmake_version(self) -> None:
 
         head = f"dev-cycle-{self.version.next_minor}"
         title = f"chore: prepare development cycle for {self.version.next_minor}"
-        if self.check_pr(base=branch_name, head=head, title=title):
-            return
+        try:
+            if self.check_pr(base=branch_name, head=head, title=title):
+                return
+        except SystemExit:
+            return  # Not fatal
 
         self.lrepo.prepare()
         self.lrepo.create_branch(head, branch_name)
@@ -615,8 +659,10 @@ def check_release_tag(self) -> GitRef:
         if not self.prompt(f"{what} does not exist. Create?"):
             self.cl.fatal(f"{what} does not exist")
 
+        branch_name = util.get_releases_branch(self.version)
         self.lrepo.prepare()
-        self.lrepo.create_tag(tag_name, util.get_releases_branch(self.version))
+        self.lrepo.switch(branch_name)
+        self.lrepo.create_tag(tag_name, branch_name)
 
         if not self.prompt(f"Push tag [b]{tag_name}[/b]?"):
             self.cl.fatal(f"{what} does not exist")

script/release/repos.py

@@ -228,6 +228,7 @@ def _register(repo: ReleaseRepo) -> None:
 )
 _register(VERSO)
 
+
 # To create a new release, open a PR into `main`. In it, bump the toolchain and
 # all dependencies. For `v4.X.0-rc1` releases, you may need to merge
 # `nightly-testing` into the PR.
@@ -241,6 +242,30 @@ def _register(repo: ReleaseRepo) -> None:
 _register(VERSO_WEB_COMPONENTS)
 
 
+# To create a new release, open a PR into `main`. In it, bump the toolchain and
+# all dependencies.
+#
+# Once the release PR is merged, tag the resulting commit with the lean version.
+VERSO_SLIDES = ReleaseRepo(
+    github=("leanprover", "verso-slides"),
+    release_tag="lean",
+    strong_deps=[VERSO],
+)
+_register(VERSO_SLIDES)
+
+
+# To create a new release, open a PR into `main`. In it, bump the toolchain and
+# all dependencies.
+#
+# Once the release PR is merged, tag the resulting commit with the lean version.
+VERSO_TEMPLATES = ReleaseRepo(
+    github=("leanprover", "verso-templates"),
+    release_tag="lean",
+    strong_deps=[VERSO, VERSO_SLIDES],
+)
+_register(VERSO_TEMPLATES)
+
+
 # To bump the toolchain, open a PR into `main`. In it, bump the toolchain and
 # all dependencies.
 #
@@ -304,6 +329,7 @@ def _register(repo: ReleaseRepo) -> None:
 )
 _register(LEANSQLITE)
 
+
 # To create a new release, open a PR into `main`. In it, bump the toolchain and
 # all dependencies. For `v4.X.0-rc1` releases, you may need to merge
 # `nightly-testing` into the PR.
@@ -327,22 +353,21 @@ def _register(repo: ReleaseRepo) -> None:
 # and all dependencies.
 #
 # Once the release PR is merged, tag the resulting commit with the lean version.
-COMPARATOR = ReleaseRepo(
-    github=("leanprover", "comparator"),
+LEAN4EXPORT = ReleaseRepo(
+    github=("leanprover", "lean4export"),
     release_tag="lean",
 )
-_register(COMPARATOR)
+_register(LEAN4EXPORT)
 
 
 # To create a new release, open a PR into `master`. In it, bump the toolchain
 # and all dependencies.
 #
 # Once the release PR is merged, tag the resulting commit with the lean version.
-LEAN4EXPORT = ReleaseRepo(
-    github=("leanprover", "lean4export"),
-    release_tag="lean",
+COMPARATOR = ReleaseRepo(
+    github=("leanprover", "comparator"), release_tag="lean", strong_deps=[LEAN4EXPORT]
 )
-_register(LEAN4EXPORT)
+_register(COMPARATOR)
 
 
 ###################

script/release/util.py

@@ -368,7 +368,8 @@ def find_pr(grepo: Repository, head: str, base: str, title: str) -> PullRequest
     for pr in grepo.get_pulls(
         state="all", base=base, sort="created", direction="desc"
     ).get_page(0):
-        if title in pr.title:
+        # Stable versions are prefixes of RC versions, so we can't just use "in"
+        if pr.title.endswith(title) or (title + " ") in pr.title:
             return pr