From 441c06980aa082a1c957b12792a4e861eefe6c92 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 11 Aug 2026 14:07:34 -0400
Subject: [PATCH] ci: Auto-update the Lean toolchain and pinned deps
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Runs daily and on demand. argumentcomputer/lean-update (dev, which carries
the pinned-tags support) bumps lean-toolchain to the latest stable release —
the updater's default channel; release candidates are opt-in via
release_channel — and moves plausible's pinned rev with it. 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 rather than only
an issue. The PR is opened with a GitHub App token so that it triggers CI;
the same App as the org repo-sync workflows.

plausible's pin changes from the short hash 6304553 to v4.31.0 — the same
commit, since that hash is what the tag points at. Written as a version tag,
the pin is managed by the updater's defaults; a future deliberate pin to a
plain commit hash will be reported and left alone, pausing the automation
until the pin is back on a tag.
---
 .github/workflows/update.yml | 36 ++++++++++++++++++++++++++++++++++++
 lake-manifest.json           |  2 +-
 lakefile.toml                |  2 +-
 3 files changed, 38 insertions(+), 2 deletions(-)
 create mode 100644 .github/workflows/update.yml

diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
new file mode 100644
index 0000000..f61c0c4
--- /dev/null
+++ b/.github/workflows/update.yml
@@ -0,0 +1,36 @@
+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.
+      - uses: argumentcomputer/lean-update@dev
+        with:
+          bump_mode: pinned-tags
+          on_update_fails: pr
+          build_args: "--wfail"
+          token: ${{ steps.app-token.outputs.token }}
diff --git a/lake-manifest.json b/lake-manifest.json
index 8351540..6f005e3 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -8,7 +8,7 @@
    "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "6304553",
+   "inputRev": "v4.31.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LSpec",
diff --git a/lakefile.toml b/lakefile.toml
index 893c2e9..3ba5ef4 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,7 +6,7 @@ testDriver = "tests"
 [[require]]
 name = "plausible"
 git = "https://github.com/leanprover-community/plausible"
-rev = "6304553"
+rev = "v4.31.0"
 
 [[lean_lib]]
 name = "LSpec"