From eb086bd4b36f40b80cfbf68ab7d89da35525a348 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 11 Aug 2026 16:19:10 -0400
Subject: [PATCH] ci: Auto-update the Lean toolchain and pinned deps

Runs daily and on demand. argumentcomputer/lean-update (dev, which carries
the pinned-tags support) bumps lean-toolchain to the latest stable release
and moves dependencies pinned to Lean version tags with it; a dependency
pinned to a commit hash is reported and left alone. The action opens a PR on
an update/lean-{release} branch whether or not the build passes, so an
incompatible release shows up as a failing PR to review. The PR is opened
with a GitHub App token so that it triggers CI; the same App as the org
repo-sync workflows.
---
 .github/workflows/update.yml | 37 ++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 .github/workflows/update.yml

diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
new file mode 100644
index 00000000..78293653
--- /dev/null
+++ b/.github/workflows/update.yml
@@ -0,0 +1,37 @@
+name: Update Lean toolchain and pinned deps
+
+on:
+  schedule:
+    # Daily at 00:00 UTC
+    - cron: "0 0 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: write
+  pull-requests: write
+
+jobs:
+  update:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+
+      # Mint a token from the GitHub App so the opened PR triggers CI; pushes
+      # made with GITHUB_TOKEN do not. Same App as the org repo-sync workflows.
+      - uses: actions/create-github-app-token@v3
+        id: app-token
+        with:
+          client-id: ${{ secrets.TOKEN_APP_ID }}
+          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
+
+      # `dev` carries the fork's bump_mode/release_channel support; `main` only
+      # mirrors upstream, which silently ignores these inputs. 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. Dependencies
+      # pinned to a Lean version tag move with the toolchain; a dependency
+      # pinned to a commit hash is reported and left alone.
+      - uses: argumentcomputer/lean-update@dev
+        with:
+          bump_mode: pinned-tags
+          on_update_fails: pr
+          token: ${{ steps.app-token.outputs.token }}