From 1f5982e76b0219363f23b4acad1f48b7c15e3661 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 14 Oct 2025 12:09:21 +1100 Subject: [PATCH] chore: update mathlib name in nightly-testing workflow MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Update the bump_toolchain_nightly-testing workflow to change the mathlib dependency name to mathlib-nightly-testing in addition to updating the rev. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude --- .github/workflows/bump_toolchain_nightly-testing.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/bump_toolchain_nightly-testing.yml b/.github/workflows/bump_toolchain_nightly-testing.yml index f5f80c337..c7310a994 100644 --- a/.github/workflows/bump_toolchain_nightly-testing.yml +++ b/.github/workflows/bump_toolchain_nightly-testing.yml @@ -52,10 +52,11 @@ jobs: run: | # Update lean-toolchain file echo "leanprover/lean4:${RELEASE_TAG}" > lean-toolchain - - # Update the mathlib rev in lakefile.toml to use the nightly-testing tag + + # Update the mathlib name and rev in lakefile.toml to use nightly-testing + sed -i "s/name = \"mathlib\"/name = \"mathlib-nightly-testing\"/" lakefile.toml sed -i "s/rev = \"[^\"]*\"/rev = \"${NIGHTLY_TESTING_TAG}\"/" lakefile.toml - + # Update dependencies lake update