From 47bd389cd363a940d90b91a295b73c8a2603e77e Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Wed, 30 Sep 2026 13:09:53 -0400
Subject: [PATCH] chore: Update CI

---
 .github/workflows/repo-sync.yml | 25 +++++++++--------
 .github/workflows/update.yml    | 48 ++++++++++++++++-----------------
 2 files changed, 37 insertions(+), 36 deletions(-)

diff --git a/.github/workflows/repo-sync.yml b/.github/workflows/repo-sync.yml
index fbe12b0b..590f72de 100644
--- a/.github/workflows/repo-sync.yml
+++ b/.github/workflows/repo-sync.yml
@@ -6,19 +6,22 @@ on:
   - cron: "0 0 * * *"
   workflow_dispatch:
 
-# The sync authenticates with a GitHub App installation token, so the job needs
-# nothing from `secrets.GITHUB_TOKEN`.
 permissions: {}
 
 jobs:
   repo-sync:
     name: Sync upstream changes
-    uses: argumentcomputer/ci-workflows/.github/workflows/repo-sync.yml@main
-    with:
-      repository: digama0/lean4lean
-      # This fork's default branch is `dev`; `master` is kept as a plain mirror
-      # of upstream, so both sides of the sync share the branch name.
-      branch: master
-    secrets:
-      TOKEN_APP_ID: ${{ secrets.TOKEN_APP_ID }}
-      TOKEN_APP_PRIVATE_KEY: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
+    runs-on: ubuntu-latest
+    # `contents` for the sync itself, `issues` for the manual-sync issue the
+    # action opens when `GITHUB_TOKEN` cannot push, e.g. an upstream change
+    # under `.github/workflows/`
+    permissions:
+      contents: write
+      issues: write
+    steps:
+      - uses: argumentcomputer/ci-workflows/.github/actions/repo-sync@main
+        with:
+          repository: digama0/lean4lean
+          # This fork's default branch is `dev`; `master` is kept as a plain mirror
+          # of upstream, so both sides of the sync share the branch name.
+          branch: master
diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index 03b7f223..21295947 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:
@@ -23,33 +23,31 @@ jobs:
         with:
           ref: dev
 
-      # Mint a token from the GitHub App so the opened PR triggers CI; pushes
-      # made with GITHUB_TOKEN do not. Same App as repo-sync.yml.
-      - 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