ci: Auto-update the Lean toolchain and pinned deps

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

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

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"