chore: Update CI

.github/dependabot.yml

@@ -0,0 +1,10 @@
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
+    groups:
+      actions:
+        patterns:
+          - "*"

.github/workflows/ci.yml

@@ -16,10 +16,20 @@ concurrency:
 jobs:
   build:
     name: Build and test
-    runs-on: warp-ubuntu-latest-x64-8x
+    # `sticky=` keeps `.lake` on a RunsOn sticky disk across runs, so Lake's
+    # incremental build state survives instead of round-tripping through the
+    # GitHub cache. Snapshots are per Git ref: a PR starts from `main`'s latest
+    # snapshot without writing back to it, so the `push` runs on `main` are
+    # what keep the shared baseline warm.
+    # https://runs-on.com/docs/runners/capabilities/sticky-disks/
+    runs-on: runs-on=${{ github.run_id }}-build-${{ github.run_attempt }}/cpu=8/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/sticky=ci-build:50gb
     timeout-minutes: 60
     steps:
       - uses: actions/checkout@v7
+      - uses: runs-on/action@v2
+        with:
+          sticky_cache: |
+            custom,path=.lake
 
       # Installs the toolchain pinned in `lean-toolchain` and runs `lake build`,
       # i.e. the `defaultTargets`: the `Lean4Lean` library, the `lean4lean` exe,
@@ -31,6 +41,7 @@ jobs:
         uses: leanprover/lean-action@v1
         with:
           build-args: --wfail
+          use-github-cache: false
 
       # `Lean4Lean.Experimental` is WIP and deliberately not a default target, but it still has to
       # compile. No `--wfail`: this is parked proof work outside the audited surface, so its

.github/workflows/nix.yml

@@ -20,7 +20,8 @@ jobs:
   # but are not built here, so they never gate CI.
   nix-test:
     name: Nix Tests
-    runs-on: warp-ubuntu-latest-x64-8x
+    # /nix lives on the root volume; Cachix is the binary cache, so no sticky disk
+    runs-on: runs-on=${{ github.run_id }}-nix-test-${{ github.run_attempt }}/cpu=8/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb
     steps:
       - uses: actions/checkout@v7
       - uses: cachix/install-nix-action@v31
@@ -42,9 +43,15 @@ jobs:
   # Verify the dev shell provides a working Lake toolchain.
   nix-devshell:
     name: Nix devShell
-    runs-on: warp-ubuntu-latest-x64-8x
+    # `lake build` below runs outside the Nix sandbox, so `.lake` can persist
+    # on a sticky disk like ci.yml's
+    runs-on: runs-on=${{ github.run_id }}-nix-devshell-${{ github.run_attempt }}/cpu=8/family=r7i+r8i+r7a+r8a/image=ubuntu26-full-x64/volume=100gb/sticky=nix-devshell:50gb
     steps:
       - uses: actions/checkout@v7
+      - uses: runs-on/action@v2
+        with:
+          sticky_cache: |
+            custom,path=.lake
       - uses: cachix/install-nix-action@v31
         with:
           nix_path: nixpkgs=channel:nixos-unstable

.github/workflows/update.yml

@@ -2,8 +2,8 @@ name: Update Lean toolchain and pinned deps
 
 on:
   schedule:
-    # Daily at 00:00 UTC
-    - cron: "0 0 * * *"
+    - cron: "0 12 * * *"
+      timezone: America/New_York
   workflow_dispatch:
 
 permissions:
@@ -21,33 +21,31 @@ jobs:
         with:
           ref: main
 
-      # Mint a token from the GitHub App so the opened PR triggers CI; pushes
-      # made with GITHUB_TOKEN do not.
-      - uses: actions/create-github-app-token@v3
-        id: app-token
+      # `update_lean4_nix` below runs `nix flake update`
+      - uses: cachix/install-nix-action@v31
         with:
-          client-id: ${{ secrets.TOKEN_APP_ID }}
-          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
+          github_access_token: ${{ github.token }}
 
-      # `dev` carries the fork's bump_mode/release_channel support; `main` only
-      # mirrors upstream, which silently ignores these inputs. `pinned-tags`
-      # suits this package: batteries is pinned to a Lean version tag rather
-      # than tracking a branch, so its `rev` moves with the toolchain; a
-      # dependency pinned to a commit hash is reported and left alone. A PR is
-      # opened on an update/lean-{release} branch whether or not the build
-      # passes, so an incompatible release shows up as a failing PR to review --
-      # expected here, where a toolchain bump can break the kernel internals
-      # this package mirrors.
+      # `dev` carries the fork's bump_mode/release_channel support and the
+      # lean4-nix gating; `main` only mirrors upstream, which silently ignores
+      # these inputs. `pinned-tags` suits this package: batteries is pinned to
+      # a Lean version tag rather than tracking a branch, so its `rev` moves
+      # with the toolchain; a dependency pinned to a commit hash is reported
+      # and left alone. A PR is opened on an update/lean-{release} branch
+      # whether or not the build passes, so an incompatible release shows up
+      # as a failing PR to review -- expected here, where a toolchain bump can
+      # break the kernel internals this package mirrors.
       #
-      # Only the Lean half is automated. flake.nix resolves the toolchain from
-      # `lean-toolchain` through lean4-nix's vendored release table, so nix.yml
-      # fails at evaluation on a release that table has not recorded yet. Those
-      # hashes arrive through lean4-nix's own lean-update PR, which will not
-      # have merged by the time this job runs, so bumping the `lean4-nix` flake
-      # input here would only add unrelated churn. It stays a manual follow-up
-      # on the update PR once lean4-nix has landed the release.
+      # flake.nix resolves the toolchain from `lean-toolchain` through
+      # lean4-nix's vendored release table, so nix.yml fails at evaluation on
+      # a release that table has not recorded yet. `update_lean4_nix` defers
+      # the update until lean4-nix's default branch carries the release, then
+      # bumps the `lean4-nix` flake input in the same PR.
+      #
+      # The PR is opened with `GITHUB_TOKEN`, so it does not start CI on its
+      # own; push to it or close and reopen it to run the checks.
       - uses: argumentcomputer/lean-update@dev
         with:
           bump_mode: pinned-tags
           on_update_fails: pr
-          token: ${{ steps.app-token.outputs.token }}
+          update_lean4_nix: true