From 0312772a1df13b1ea2195fd5d3cb609a448649ca Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 30 Sep 2026 13:12:04 -0400 Subject: [PATCH 1/2] chore: Update CI --- .github/workflows/update.yml | 48 +++++++++++++++++------------------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index fe5aad0..b0c37a3 100644 --- a/.github/workflows/update.yml +++ b/.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 From 30cf180ba31d13036696ab83e74f245507849f5e Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 30 Sep 2026 13:26:45 -0400 Subject: [PATCH 2/2] ci: Move to RunsOn runners and group Dependabot updates Replace the Warp runners with RunsOn labels matching ix's CI: the same instance families and image, 8 vCPUs like the Warp size they replace. The build and devShell jobs keep `.lake` on a 50 GB sticky disk so Lake's incremental state survives between runs; the Nix test job needs none, since its builds run inside the Nix sandbox against Cachix. The two Lake disks are separate lineages because they are populated by different Lean binaries (elan's and Nix's). Add a Dependabot config for GitHub Actions with a single group, so updates arrive as one weekly PR. --- .github/dependabot.yml | 10 ++++++++++ .github/workflows/ci.yml | 13 ++++++++++++- .github/workflows/nix.yml | 11 +++++++++-- 3 files changed, 31 insertions(+), 3 deletions(-) create mode 100644 .github/dependabot.yml diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 0000000..d15c975 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,10 @@ +version: 2 +updates: + - package-ecosystem: "github-actions" + directory: "/" + schedule: + interval: "weekly" + groups: + actions: + patterns: + - "*" diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d34a7da..7bda0e7 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index a13b3ad..4673c84 100644 --- a/.github/workflows/nix.yml +++ b/.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