diff --git a/.github/workflows/build-template.yml b/.github/workflows/build-template.yml
index d3a8c2c9eb..c74d950098 100644
--- a/.github/workflows/build-template.yml
+++ b/.github/workflows/build-template.yml
@@ -101,7 +101,7 @@ jobs:
           # NOTE: must be in sync with `save` below and with `restore-cache` in `update-stage0.yml`
           path: |
             .ccache
-            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
+            ${{ matrix.lake-actions-cache && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
             build/stage1/**/*.ir
@@ -188,7 +188,7 @@ jobs:
           # NOTE: must be in sync with `restore` above
           path: |
             .ccache
-            ${{ matrix.name == 'Linux Lake' && 'build/stage1/**/*.trace
+            ${{ matrix.lake-actions-cache && 'build/stage1/**/*.trace
             build/stage1/**/*.olean*
             build/stage1/**/*.ilean
             build/stage1/**/*.ir
@@ -199,7 +199,7 @@ jobs:
         name: Upload Lake Cache
         # Caching on cancellation created some mysterious issues perhaps related to improper build
         # shutdown. Also, since this needs access to secrets, it cannot be run on forks.
-        if: matrix.name == 'Linux Lake' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
+        if: matrix.name == 'Linux release' && !cancelled() && (github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository)
         run: |
           curl --version
           cd src
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index b03858b605..a422cbb503 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -264,29 +264,8 @@ jobs:
               {
                 // portable release build: use channel with older glibc (2.26)
                 "name": "Linux release",
-                // usually not a bottleneck so make exclusive to `fast-ci`
-                "os": large && fast ? chonk : "ubuntu-latest",
-                "release": true,
-                // Special handling for release jobs. We want:
-                // 1. To run it in PRs so developers get PR toolchains (so secondary without tests is sufficient)
-                // 2. To skip it in merge queues as it takes longer than the
-                //    Linux lake build and adds little value in the merge queue
-                // 3. To run it in release (obviously)
-                // 4. To run it for pushes to master so that pushes to master have a Linux toolchain
-                //    available as an artifact for Grove to use.
-                "enabled": isPr || level != 1 || isPushToMaster,
-                "test": level >= 1,
-                "secondary": level == 0,
-                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
-                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst",
-                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
-                "binary-check": "ldd -v",
-                // foreign code may be linked against more recent glibc
-                "CTEST_OPTIONS": "-E 'foreign'",
-              },
-              {
-                "name": "Linux Lake",
                 "os": large ? chonk : "ubuntu-latest",
+                "release": true,
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
                 // Done as part of test-bench
@@ -294,8 +273,16 @@ jobs:
                 "test": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
-                // We are not warning-free yet on all platforms, start here
-                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror -DUSE_LAKE_CACHE=ON",
+                "shell": "nix develop .#oldGlibc -c bash -euxo pipefail {0}",
+                "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst",
+                "prepare-llvm": "../script/prepare-llvm-linux.sh lean-llvm*",
+                "binary-check": "ldd -v",
+                // We are not warning-free yet on all platforms, start with Linux
+                // Do not (yet) use Lake cache on release
+                "CMAKE_OPTIONS": "-DLEAN_EXTRA_CXX_FLAGS=-Werror" + (level < 3 ? " -DUSE_LAKE_CACHE=ON" : ""),
+                "lake-actions-cache": level < 3,
+                // foreign code may be linked against more recent glibc
+                "CTEST_OPTIONS": "-E 'foreign'",
               },
               {
                 "name": "Linux Lake (Cached)",
@@ -366,7 +353,9 @@ jobs:
                 "prepare-llvm": "../script/prepare-llvm-macos.sh lean-llvm*",
                 "binary-check": "otool -L",
                 "tar": "gtar", // https://github.com/actions/runner-images/issues/2619
-                // See "Linux release" for release job levels; Grove is not a concern here
+                // Run in PRs so developers get PR toolchains (so secondary without tests is sufficient);
+                // skip in merge queues as it takes longer than the Linux release build and adds little
+                // value in the merge queue; run in release (obviously)
                 "enabled": isPr || level != 1,
                 "test": level >= 1,
                 "secondary": level == 0,
diff --git a/.github/workflows/update-stage0.yml b/.github/workflows/update-stage0.yml
index eb61c660f4..0615fee242 100644
--- a/.github/workflows/update-stage0.yml
+++ b/.github/workflows/update-stage0.yml
@@ -19,6 +19,10 @@ concurrency:
 jobs:
   update-stage0:
     runs-on: nscloud-ubuntu-22.04-amd64-8x16
+    defaults:
+      run:
+        # like Linux release
+        shell: nix develop .#oldGlibc -c bash -euxo pipefail {0}
     env:
       CCACHE_DIR: ${{ github.workspace }}/.ccache
       CCACHE_COMPRESS: true
@@ -30,9 +34,11 @@ jobs:
     - uses: actions/checkout@v6
       with:
         ssh-key: ${{secrets.STAGE0_SSH_KEY}}
-    - run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
+    - shell: bash
+      run: echo "should_update_stage0=yes" >> "$GITHUB_ENV"
     - name: Check if automatic update is needed
       if: github.event_name == 'push'
+      shell: bash
       run: |
         if diff -u src/stdlib_flags.h stage0/src/stdlib_flags.h
         then
@@ -41,6 +47,7 @@ jobs:
         fi
     - name: Setup git user
       if: env.should_update_stage0 == 'yes'
+      shell: bash
       run: |
           git config --global user.name "Lean stage0 autoupdater"
           git config --global user.email "<>"
@@ -50,12 +57,10 @@ jobs:
     - name: Open Nix shell once
       if: env.should_update_stage0 == 'yes'
       run: true
-      shell: 'nix develop -c bash -euxo pipefail {0}'
     - name: Set up NPROC
       if: env.should_update_stage0 == 'yes'
       run: |
         echo "NPROC=$(nproc 2>/dev/null || sysctl -n hw.logicalcpu 2>/dev/null || echo 4)" >> $GITHUB_ENV
-      shell: 'nix develop -c bash -euxo pipefail {0}'
     - name: Restore Cache
       if: env.should_update_stage0 == 'yes'
       uses: actions/cache/restore@v5
@@ -69,20 +74,23 @@ jobs:
           build/stage1/**/*.ir
           build/stage1/**/*.c
           build/stage1/**/*.c.o*
-        key: Linux Lake-build-v4-${{ github.sha }}
+        key: Linux release-build-v4-${{ github.sha }}
         # fall back to (latest) previous cache
         restore-keys: |
-          Linux Lake-build-v4
+          Linux release-build-v4
     - if: env.should_update_stage0 == 'yes'
-      # sync options with `Linux Lake` to ensure cache reuse
+      name: Configure Build
+      # sync options with `Linux release` to ensure cache reuse
       run: |
         mkdir -p build
-        cmake --preset release -B build -DWFAIL=ON
-      shell: 'nix develop -c bash -euxo pipefail {0}'
+        cd build
+        wget -q https://github.com/leanprover/lean-llvm/releases/download/22.1.4/lean-llvm-x86_64-linux-gnu.tar.zst
+        PREPARE="$(../script/prepare-llvm-linux.sh lean-llvm*)"
+        eval "OPTIONS=($PREPARE)"
+        cmake .. --preset release -B . -DWFAIL=ON -DLEAN_EXTRA_CXX_FLAGS=-Werror "${OPTIONS[@]}"
     - if: env.should_update_stage0 == 'yes'
       run: |
         make -j$NPROC -C build update-stage0-commit
-      shell: 'nix develop -c bash -euxo pipefail {0}'
     - if: env.should_update_stage0 == 'yes'
       run: git show --stat
     - if: env.should_update_stage0 == 'yes' && github.event_name == 'push'