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 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