From 265fcdac89839098e7c39bcd3700dabbc68ff3e9 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 27 Aug 2026 19:56:44 -0400
Subject: [PATCH 01/10] feat: Exclude a directory from a package directory glob
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A `/**` sweep takes every package under a directory, which is the wrong
granularity when one package in the tree must not move — a benchmark
pinned to an old toolchain on purpose, say. Without a way to carve it
back out, the whole glob has to be abandoned for an explicit list that
goes stale as packages are added.

An entry prefixed with `!` now subtracts: it names a directory and drops
that directory together with everything beneath it, so
`benchmarks/** !benchmarks/pinned` covers the tree and spares the one
package.

Exclusions live in `lake_package_directory` rather than in an input of
their own so that no step invoking the action needs a second environment
variable kept in sync with the first.

Matching compares path components, not string prefixes, so
`!benchmarks/slow` cannot swallow `benchmarks/slowfixture`, while
trailing slashes and `./` prefixes still name the same directory. An
exclusion carrying a glob is rejected, since it already reaches its whole
subtree, and one matching nothing is reported: a typo there silently
updates the package it was meant to protect.
---
 .github/workflows/e2e_test.yml | 35 +++++++++++++++++
 LeanUpdate/Input.lean          | 61 +++++++++++++++++++++++++++---
 Test/Main.lean                 |  2 +
 Test/PackageDirectoryGlob.lean | 68 +++++++++++++++++++++++++++++++---
 action.yml                     |  8 +++-
 5 files changed, 161 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/e2e_test.yml b/.github/workflows/e2e_test.yml
index 477c566..e7049fb 100644
--- a/.github/workflows/e2e_test.yml
+++ b/.github/workflows/e2e_test.yml
@@ -331,3 +331,38 @@ jobs:
       - name: This update should succeed
         if: steps.update.outputs.result != 'update-success'
         run: exit 1
+
+  # An exclusion carves a package back out of the set the action would otherwise
+  # update, leaving its lean-toolchain untouched.
+  excluded_directory_e2e_test:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+
+      - name: Bump two packages, excluding one of them
+        id: update
+        uses: ./
+        with:
+          bump_mode: "pinned-tags"
+          on_update_succeeds: "silent"
+          on_update_fails: "silent"
+          lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"
+
+      - name: The excluded package must be left alone
+        run: |
+          a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
+          b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
+          echo "PinnedTags=$a SmokeSuccess=$b"
+          if [ "$a" = "v4.31.0" ]; then
+            echo "Error: the included package was not bumped"
+            exit 1
+          fi
+          if [ "$b" != "v4.16.0" ]; then
+            echo "Error: the excluded package was bumped to $b"
+            exit 1
+          fi
+
+      - name: This update should succeed
+        if: steps.update.outputs.result != 'update-success'
+        run: exit 1
diff --git a/LeanUpdate/Input.lean b/LeanUpdate/Input.lean
index cf28c55..f46c969 100644
--- a/LeanUpdate/Input.lean
+++ b/LeanUpdate/Input.lean
@@ -104,6 +104,37 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
     found := found ++ (← lakePackagesUnder child.path)
   return found
 
+/-- Split a directory-list action input into its entries.
+
+Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
+path per line all parse alike. -/
+def splitPackageDirEntries (raw : String) : List String :=
+  raw.split (fun c => c == ',' || c.isWhitespace)
+    |>.map (fun s => s.trimAscii.copy)
+    |>.filter (fun s => !s.isEmpty)
+    |>.toList
+
+#guard
+  splitPackageDirEntries " Benchmarks/**,\n  !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]
+
+/-- The significant components of `path`, dropping empty and `.` segments. -/
+def pathComponents (path : FilePath) : List String :=
+  path.components.filter (fun s => !s.isEmpty && s != ".")
+
+/-- whether `dir` is `parent` itself or lies somewhere beneath it
+
+Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
+and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
+living under `Benchmarks/Slow`. -/
+def isAtOrUnder (parent dir : FilePath) : Bool :=
+  (pathComponents parent).isPrefixOf (pathComponents dir)
+
+#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
+#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
+#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
+#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
+#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"
+
 /-- Resolve the target Lake package directories supplied by the action input.
 
 The input is a comma- or whitespace-separated list of paths, each resolved relative to the
@@ -111,14 +142,23 @@ GitHub workspace. An entry ending in `/*` expands to the immediate subdirectorie
 that contain a lakefile, so a repository of sibling packages can be updated in one invocation
 (e.g. `templates/*`). An entry ending in `/**` expands the same way but walks the whole tree, so
 it also reaches a package nested inside another package (e.g. a fixture workspace required by
-path from its parent). Both forms sort by path and skip dotted directories such as `.lake`. -/
+path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.
+
+An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
+directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
+holds a package the update must leave alone. An exclusion carries no glob of its own, since it
+already reaches the whole subtree. -/
 public def getTargetLakePackageDirectories : IO (Array FilePath) := do
   let packageDir ← GitHub.Action.Input.get LakePackageDirectory
   let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
   let raw := packageDir.val.toString
-  let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
-    |>.map (fun s => s.trimAscii.copy)
-    |>.filter (fun s => !s.isEmpty)
+  let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
+  let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
+  for entry in exclusions do
+    if entry.any (· == '*') then
+      throw <| IO.userError <|
+        s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
+        "covers everything beneath it."
   let mut dirs : Array FilePath := #[]
   for entry in entries do
     if entry.endsWith "/**" then
@@ -136,9 +176,18 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
       dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
     else
       dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
-  if dirs.isEmpty then
+  let excludedDirs := exclusions.map (fun entry =>
+    resolveLakePackageDir workspace? (FilePath.mk entry))
+  -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
+  -- cost of the typo is that a package meant to be protected is updated instead.
+  for (entry, excludedDir) in exclusions.zip excludedDirs do
+    unless dirs.any (isAtOrUnder excludedDir ·) do
+      IO.println <| log%
+        s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
+  let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
+  if kept.isEmpty then
     throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
-  return dirs
+  return kept
 
 /-- The input whether to update the `lean-toolchain` file. -/
 public inductive UpdateLeanToolchain where
diff --git a/Test/Main.lean b/Test/Main.lean
index 4b82cdf..e30f611 100644
--- a/Test/Main.lean
+++ b/Test/Main.lean
@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
   | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
   | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
   | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
+  | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
+  | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
   | _ => do
     LeanUpdateTest.PinnedTagFallback.test
     LeanUpdateTest.PackageDirectoryGlob.test
diff --git a/Test/PackageDirectoryGlob.lean b/Test/PackageDirectoryGlob.lean
index 17a64af..5bd36ca 100644
--- a/Test/PackageDirectoryGlob.lean
+++ b/Test/PackageDirectoryGlob.lean
@@ -1,5 +1,6 @@
 module
 
+import Lean
 import LeanUpdate.IO
 import LeanUpdate.Input
 
@@ -48,7 +49,22 @@ public def runShallow : IO Unit :=
     let benchmarks := workspace / "Benchmarks"
     #[benchmarks / "Catalog", benchmarks / "Compile"]
 
-def runInWorkspace (workspace : FilePath) (packageDir : String) (mode : String) : IO Unit := do
+/-- An excluded directory takes the packages nested inside it with it. -/
+public def runExcludeSubtree : IO Unit :=
+  checkExpansion fun workspace => #[workspace / "Benchmarks" / "Compile"]
+
+/-- Excluding a nested package leaves the package containing it in the expansion. -/
+public def runExcludeNested : IO Unit :=
+  checkExpansion fun workspace =>
+    let benchmarks := workspace / "Benchmarks"
+    #[
+      benchmarks / "Catalog",
+      benchmarks / "Catalog" / "FixtureB",
+      benchmarks / "Compile"
+    ]
+
+/-- Expand `packageDir` in a subprocess, returning its exit code and everything it printed. -/
+def runInWorkspace (workspace : FilePath) (packageDir mode : String) : IO (UInt32 × String) := do
   let currentExe ← IO.appPath
   let out ← IO.Process.output {
     cmd := currentExe.toString
@@ -58,19 +74,61 @@ def runInWorkspace (workspace : FilePath) (packageDir : String) (mode : String)
       ("LAKE_PACKAGE_DIRECTORY", some packageDir)
     ]
   }
-  if out.exitCode != 0 then
-    throw <| IO.userError s!"{mode} failed\nstdout:\n{out.stdout}\nstderr:\n{out.stderr}"
+  pure (out.exitCode, out.stdout ++ out.stderr)
+
+/-- Run an expansion that must succeed, and return what it printed. -/
+def runExpectingSuccess (workspace : FilePath) (packageDir mode : String) : IO String := do
+  let (exitCode, output) ← runInWorkspace workspace packageDir mode
+  if exitCode != 0 then
+    throw <| IO.userError s!"{mode} failed for '{packageDir}'\n{output}"
+  pure output
+
+/-- Run an expansion that must fail, and return what it reported. -/
+def runExpectingFailure (workspace : FilePath) (packageDir mode : String) : IO String := do
+  let (exitCode, output) ← runInWorkspace workspace packageDir mode
+  if exitCode == 0 then
+    throw <| IO.userError s!"{mode} should have failed for '{packageDir}'\n{output}"
+  pure output
+
+def checkContains (haystack needle description : String) : IO Unit := do
+  unless haystack.contains needle do
+    throw <| IO.userError s!"{description}: expected to find {needle} in\n{haystack}"
 
 /--
 A package required by path from its parent lives one level below that parent, so `/*` — which
 reads only the immediate subdirectories — cannot see it. `/**` walks the tree instead, while
 still pruning `.lake` so vendored dependency checkouts are never mistaken for the repository's
 own packages.
+
+A `!` entry then carves packages back out of that sweep, which is what makes a `/**` over a
+benchmark tree usable when one package in it must not be updated.
 -/
 public def test : IO Unit := do
   IO.FS.withTempDir fun tempDir => do
     buildWorkspace tempDir
-    runInWorkspace tempDir "Benchmarks/**" "package-glob-recursive"
-    runInWorkspace tempDir "Benchmarks/*" "package-glob-shallow"
+    let _ ← runExpectingSuccess tempDir "Benchmarks/**" "package-glob-recursive"
+    let _ ← runExpectingSuccess tempDir "Benchmarks/*" "package-glob-shallow"
+    let _ ← runExpectingSuccess tempDir "Benchmarks/** !Benchmarks/Catalog"
+      "package-glob-exclude-subtree"
+    let _ ← runExpectingSuccess tempDir "Benchmarks/** !Benchmarks/Catalog/FixtureA"
+      "package-glob-exclude-nested"
+
+    -- A trailing slash and a `./` prefix name the same directory as the bare path.
+    let _ ← runExpectingSuccess tempDir "Benchmarks/** !./Benchmarks/Catalog/"
+      "package-glob-exclude-subtree"
+
+    -- `Benchmarks/Compil` is a string prefix of `Benchmarks/Compile` but not a directory
+    -- containing it, so nothing is excluded and the mismatch is reported.
+    let unmatched ← runExpectingSuccess tempDir "Benchmarks/** !Benchmarks/Compil"
+      "package-glob-recursive"
+    checkContains unmatched "matched none" "an exclusion matching no package directory"
+
+    let globbed ← runExpectingFailure tempDir "Benchmarks/** !Benchmarks/**"
+      "package-glob-recursive"
+    checkContains globbed "contains a glob" "a globbed exclusion"
+
+    let emptied ← runExpectingFailure tempDir "Benchmarks/** !Benchmarks"
+      "package-glob-recursive"
+    checkContains emptied "No Lake package directories found" "an exclusion covering every target"
 
 end LeanUpdateTest.PackageDirectoryGlob
diff --git a/action.yml b/action.yml
index e57f3c1..830d96f 100644
--- a/action.yml
+++ b/action.yml
@@ -14,8 +14,12 @@ inputs:
       packages can be updated in one invocation (e.g. `templates/*`). An entry ending in `/**`
       expands the same way but walks the whole tree, reaching a package nested inside another
       package — a fixture workspace that its parent requires by path, say. Both forms skip
-      dotted directories, so the dependency checkouts under `.lake` are never swept up. With
-      multiple directories the outputs aggregate: an update or failure in any directory reports
+      dotted directories, so the dependency checkouts under `.lake` are never swept up. An entry
+      prefixed with `!` subtracts instead of adding: it names a directory and drops that directory
+      together with everything beneath it, so a broad `benchmarks/**` can still leave one package
+      alone (e.g. `benchmarks/** !benchmarks/pinned`). An exclusion carries no glob of its own,
+      since it already covers its whole subtree, and one matching nothing is reported in the log.
+      With multiple directories the outputs aggregate: an update or failure in any directory reports
       as such, and the Mathlib cache prefetch (which understands a single directory) is skipped.
       This parameter is passed to the lake-package-directory argument of leanprover/lean-action.
     required: false

From 8075eb87ae9af0e8bfc5b6d175a61d356b4497f4 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 27 Aug 2026 19:58:46 -0400
Subject: [PATCH 02/10] Update flake.lock

---
 flake.lock | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/flake.lock b/flake.lock
index 9ecf605..15b4958 100644
--- a/flake.lock
+++ b/flake.lock
@@ -5,11 +5,11 @@
         "nixpkgs-lib": "nixpkgs-lib"
       },
       "locked": {
-        "lastModified": 1782949081,
-        "narHash": "sha256-vp6Y/Grm98ESt6ceOkWiHWyZRDV3J1RID4w+6NWK9yA=",
+        "lastModified": 1787559586,
+        "narHash": "sha256-onL0VLf9vPllmT0H/OlURIU5r5t5WIEl7t4tVNKT0Nw=",
         "owner": "hercules-ci",
         "repo": "flake-parts",
-        "rev": "17c9d6cdfc60c64f4ee8d306f9bc0b4ccb51481e",
+        "rev": "9d0d87172c374f89da73c1cfe6d81ae62feac1f1",
         "type": "github"
       },
       "original": {
@@ -42,11 +42,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1786463392,
-        "narHash": "sha256-5ke9p2DFQcF0FxR/RyrYvZymoVcCR1zyVWlnhqfRyf0=",
+        "lastModified": 1787593167,
+        "narHash": "sha256-TJ/Lq/p8sXXINpodMSjpotERiCoDfoJDuvBn+bVL9Y8=",
         "owner": "argumentcomputer",
         "repo": "lean4-nix",
-        "rev": "c41a770e44a990da275dad0f70da75f22197e597",
+        "rev": "e014934f9c2b634aea3be072c7b0e6053a5cb211",
         "type": "github"
       },
       "original": {
@@ -73,11 +73,11 @@
     },
     "nixpkgs-lib": {
       "locked": {
-        "lastModified": 1782614948,
-        "narHash": "sha256-ePjCwr1sNm9NYUqywL7QfK3JnlS015msC+eBu2zKlp8=",
+        "lastModified": 1785031560,
+        "narHash": "sha256-OmshNvn2vupOFpYinLUu+1Dnpu4n7Q5N3ggGVNHpkUI=",
         "owner": "nix-community",
         "repo": "nixpkgs.lib",
-        "rev": "db3f255737b94216eb71cce308e2912cf6bc2d7c",
+        "rev": "0e79af5e3d4dcfcd676ab5ba3f95d2e3352e078c",
         "type": "github"
       },
       "original": {

From 448b22ac728d232f5f3039b0a8a9a6a25993d043 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 27 Aug 2026 20:17:48 -0400
Subject: [PATCH 03/10] ci: Restrict the E2E workflow to a read-only token

Without a `permissions` block the jobs run with whatever the repository
grants by default, which on many repositories is write access to
contents, issues, and pull requests. The E2E jobs update fixtures only
inside the runner's own checkout and never write back, and the action's
`gh` calls read the public list of Lean releases, so `contents: read`
covers everything they do.
---
 .github/workflows/e2e_test.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/e2e_test.yml b/.github/workflows/e2e_test.yml
index e7049fb..34e690a 100644
--- a/.github/workflows/e2e_test.yml
+++ b/.github/workflows/e2e_test.yml
@@ -16,6 +16,11 @@ on:
       - dev
   workflow_dispatch:
 
+# Every job updates fixtures inside the runner's own checkout and never writes back. The
+# action's `gh` calls only read the public list of Lean releases.
+permissions:
+  contents: read
+
 jobs:
   success_e2e_test:
     runs-on: ubuntu-latest

From 59519553357e22202f94d67c03aa1ce8e96b60b6 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 27 Aug 2026 20:22:16 -0400
Subject: [PATCH 04/10] ci: Restrict the CI and test workflows to a read-only
 token

Neither workflow writes to the repository: both build and assert inside
the runner's own checkout, and the `gh` calls underneath read public
data. Without a `permissions` block they ran with whatever the
repository grants by default, which is commonly write access to
contents, issues, and pull requests.
---
 .github/workflows/lean_action_ci.yml | 5 +++++
 .github/workflows/test.yaml          | 5 +++++
 2 files changed, 10 insertions(+)

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 92185ff..a658258 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -16,6 +16,11 @@ on:
       - dev
   workflow_dispatch:
 
+# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
+# made by lean-action read the public Mathlib cache and the public list of Lean releases.
+permissions:
+  contents: read
+
 jobs:
   build:
     runs-on: ubuntu-latest
diff --git a/.github/workflows/test.yaml b/.github/workflows/test.yaml
index c04a3f4..6b143cf 100644
--- a/.github/workflows/test.yaml
+++ b/.github/workflows/test.yaml
@@ -16,6 +16,11 @@ on:
       - dev
   workflow_dispatch:
 
+# Every job asserts on the action's outputs inside the runner's own checkout and never
+# writes back, so a read-only token is all they need.
+permissions:
+  contents: read
+
 jobs:
   has_dependency_output_test_true:
     runs-on: ubuntu-latest

From aece5d95c1a25dfed81a3d9a16380765273f3c6d Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Thu, 27 Aug 2026 20:22:16 -0400
Subject: [PATCH 05/10] ci: Open the self-update PR with GITHUB_TOKEN

The App token existed only to work around GitHub's guard against a
workflow triggering itself, which leaves a GITHUB_TOKEN pull request
with no CI runs until a maintainer releases them. Trading that back for
one fewer credential to install and rotate means the self-update PR
opens with checks pending until someone pushes to the branch or closes
and reopens it.

The job needs contents and pull-requests write to open the PR, and
issues write for the default `on_update_fails: issue` path.
---
 .github/workflows/update.yml | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml
index 44f3180..97646d0 100644
--- a/.github/workflows/update.yml
+++ b/.github/workflows/update.yml
@@ -5,6 +5,13 @@ on:
     - cron: '0 0 * * *' # every day at midnight
   workflow_dispatch:
 
+# Opening the pull request needs write access to contents and pull requests, and the
+# default `on_update_fails: issue` needs to open an issue when the bump does not build.
+permissions:
+  contents: write
+  pull-requests: write
+  issues: write
+
 jobs:
   update:
     runs-on: ubuntu-latest
@@ -12,17 +19,6 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v6
 
-      # Mint a token from the GitHub App so the opened PR triggers CI. A PR opened with the
-      # default GITHUB_TOKEN does not start workflow runs — GitHub's guard against a workflow
-      # triggering itself — so those runs sit waiting for a maintainer to release them by hand.
-      - uses: actions/create-github-app-token@v3
-        id: app-token
-        with:
-          client-id: ${{ secrets.TOKEN_APP_ID }}
-          private-key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
-
       - name: Update Lean package
         id: update
         uses: ./
-        with:
-          token: ${{ steps.app-token.outputs.token }}

From ac315a05a5a8de7918412a32f92fa3fcbe0f4b82 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 1 Sep 2026 15:52:27 -0400
Subject: [PATCH 06/10] docs: Record what the default token cannot do

Opening a pull request with `github.token` carries two constraints that
are documented in peter-evans/create-pull-request but nowhere here, so
they surface as a 403 or a PR with no checks: the repository must allow
GitHub Actions to create pull requests, and such a PR does not trigger
workflow runs.

The README examples already carried the write scopes, attributed to
private repositories. The default token has been read-only regardless of
visibility since February 2023, so the note said the right thing for the
wrong reason.

Also note that a `!` exclusion has to be quoted in YAML, since a scalar
opening with `!` is read as a tag.
---
 README.md  | 12 +++++++++---
 action.yml | 10 +++++++++-
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 2e15411..4a2bf8a 100644
--- a/README.md
+++ b/README.md
@@ -20,7 +20,9 @@ on:
 
 jobs:
   update_lean:
-    # this is needed for private repositories
+    # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
+    # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
+    # requests` under Settings > Actions > General > Workflow permissions.
     permissions:
       contents: write
       pull-requests: write
@@ -49,7 +51,9 @@ on:
 
 jobs:
   update_lean:
-    # this is needed for private repositories
+    # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
+    # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
+    # requests` under Settings > Actions > General > Workflow permissions.
     permissions:
       contents: write
       pull-requests: write
@@ -81,7 +85,9 @@ on:
 
 jobs:
   update_lean:
-    # this is needed for private repositories
+    # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
+    # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
+    # requests` under Settings > Actions > General > Workflow permissions.
     permissions:
       contents: write
       pull-requests: write
diff --git a/action.yml b/action.yml
index 830d96f..37f34e3 100644
--- a/action.yml
+++ b/action.yml
@@ -19,6 +19,7 @@ inputs:
       together with everything beneath it, so a broad `benchmarks/**` can still leave one package
       alone (e.g. `benchmarks/** !benchmarks/pinned`). An exclusion carries no glob of its own,
       since it already covers its whole subtree, and one matching nothing is reported in the log.
+      Quote the value in YAML: a scalar that starts with `!` is otherwise read as a YAML tag.
       With multiple directories the outputs aggregate: an update or failure in any directory reports
       as such, and the Mathlib cache prefetch (which understands a single directory) is skipped.
       This parameter is passed to the lake-package-directory argument of leanprover/lean-action.
@@ -165,7 +166,14 @@ inputs:
     default: "lake-manifest.json"
   token:
     description: |
-      A Github token to be used for committing
+      A Github token to be used for committing.
+
+      With the default `github.token`, opening a pull request also needs
+      `Settings > Actions > General > Workflow permissions > Allow GitHub Actions to create and
+      approve pull requests` enabled on the repository, and the PR it opens will not start any
+      workflow runs — GitHub's guard against a workflow triggering itself — so its checks sit
+      pending until someone pushes to the branch or reopens it. Pass a PAT or a GitHub App token
+      to avoid both.
     required: false
     default: ${{ github.token }}
 

From 50d4c6147b7ff96554b9cd8e39cce2f57f726246 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 1 Sep 2026 15:52:34 -0400
Subject: [PATCH 07/10] fix: Reject a bare `!` package directory exclusion
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A `!` with no path after it resolves to the workspace root, which is at
or above every target, so the whole expansion is filtered away and the
run fails reporting that no package directory was found — true, but not
where the reader would start looking. Name the actual mistake.
---
 LeanUpdate/Input.lean          | 4 ++++
 Test/PackageDirectoryGlob.lean | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/LeanUpdate/Input.lean b/LeanUpdate/Input.lean
index f46c969..633b239 100644
--- a/LeanUpdate/Input.lean
+++ b/LeanUpdate/Input.lean
@@ -155,6 +155,10 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
   let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
   let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
   for entry in exclusions do
+    if entry.isEmpty then
+      throw <| IO.userError <|
+        "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
+        "as in '!benchmarks/pinned'."
     if entry.any (· == '*') then
       throw <| IO.userError <|
         s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
diff --git a/Test/PackageDirectoryGlob.lean b/Test/PackageDirectoryGlob.lean
index 5bd36ca..96e7bcd 100644
--- a/Test/PackageDirectoryGlob.lean
+++ b/Test/PackageDirectoryGlob.lean
@@ -123,6 +123,9 @@ public def test : IO Unit := do
       "package-glob-recursive"
     checkContains unmatched "matched none" "an exclusion matching no package directory"
 
+    let bare ← runExpectingFailure tempDir "Benchmarks/** !" "package-glob-recursive"
+    checkContains bare "names no directory" "a bare exclusion marker"
+
     let globbed ← runExpectingFailure tempDir "Benchmarks/** !Benchmarks/**"
       "package-glob-recursive"
     checkContains globbed "contains a glob" "a globbed exclusion"

From fe7af4b2adb7e0600a337df0e391c3723538d19e Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 1 Sep 2026 15:52:34 -0400
Subject: [PATCH 08/10] ci: Silence the failure outcome in the test workflow

The jobs set `on_update_succeeds: silent` but left the failure path at
its default, so a fixture that stopped building would have the action
open an issue. The workflow now runs with a read-only token, which turns
that into a 403 on top of the failure it is reporting. A red check is
the signal a test workflow owes its reader.
---
 .github/workflows/test.yaml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/test.yaml b/.github/workflows/test.yaml
index 6b143cf..8cd52c8 100644
--- a/.github/workflows/test.yaml
+++ b/.github/workflows/test.yaml
@@ -33,6 +33,7 @@ jobs:
         uses: ./
         with:
           on_update_succeeds: "silent"
+          on_update_fails: "silent"
           lake_package_directory: "./Fixtures/HasDep"
 
       - name: The result should be success
@@ -49,6 +50,7 @@ jobs:
         uses: ./
         with:
           on_update_succeeds: "silent"
+          on_update_fails: "silent"
           lake_package_directory: "./Fixtures/SmokeSuccess"
       - name: The result should be no dependency
         if: steps.update.outputs.has_dependency != 'false'
@@ -65,6 +67,7 @@ jobs:
         uses: ./
         with:
           on_update_succeeds: "silent"
+          on_update_fails: "silent"
           lake_package_directory: "./Fixtures/SmokeSuccess"
 
       - name: output assertion of latest_lean
@@ -97,6 +100,7 @@ jobs:
         uses: ./
         with:
           on_update_succeeds: "silent"
+          on_update_fails: "silent"
           lake_package_directory: "./Fixtures/HasDep"
 
       - name: output assertion of latest_lean
@@ -123,6 +127,7 @@ jobs:
         uses: ./
         with:
           on_update_succeeds: "silent"
+          on_update_fails: "silent"
           lake_package_directory: "./Fixtures/SmokeSuccess"
           update_lean_toolchain: "never"
 

From b0ed23f2f3410ae5279cff063b634867254872a2 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 1 Sep 2026 16:32:09 -0400
Subject: [PATCH 09/10] fix: Get the Mathlib cache for every target package

The prefetch delegated to leanprover/lean-action, which takes one
directory and uses it as the working directory of its every step. A list,
a glob, or an exclusion is not a directory, so the step could not start,
and `continue-on-error` turned that into a red mark nobody read. Anyone
globbing a tree of Mathlib packages then built them from source.

Validation already walks each target package, so fetch the cache there:
one manifest check, then `lake exe cache get` for the packages that want
it. Every package root has its own `.lake/packages/mathlib` and needs its
own unpack, while the downloads pool in one per-user directory, so the
extra directories cost no extra network.

Elan is installed by this action's own step, so nothing else was keeping
lean-action here.
---
 LeanUpdate/PostUpdateValidation.lean | 24 ++++++++++++++++++++++++
 action.yml                           | 20 ++------------------
 2 files changed, 26 insertions(+), 18 deletions(-)

diff --git a/LeanUpdate/PostUpdateValidation.lean b/LeanUpdate/PostUpdateValidation.lean
index 18ea57b..203cd14 100644
--- a/LeanUpdate/PostUpdateValidation.lean
+++ b/LeanUpdate/PostUpdateValidation.lean
@@ -91,9 +91,33 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
 public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
   !result.isSuccess
 
+/-- Whether the package rooted at `cwd` depends on Mathlib. -/
+def dependsOnMathlib (cwd : FilePath) : IO Bool := do
+  let manifest := cwd / "lake-manifest.json"
+  if !(← manifest.pathExists) then
+    return false
+  return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"
+
+/-- Download Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.
+
+Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
+per package; the downloads behind it are pooled in a single per-user directory, so only the first
+package pays for the network. Failing to get the cache only means a slower build, so it is
+reported rather than raised.
+-/
+def getMathlibCache (cwd : FilePath) : IO Unit := do
+  unless ← dependsOnMathlib cwd do
+    return
+  IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
+  let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
+  if out.exitCode != 0 then
+    IO.println <| log%
+      s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
+
 /-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
 def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
     IO PostUpdateValidationResult := do
+  getMathlibCache targetLakePackageDir
   let buildResult ← runLakeBuild targetLakePackageDir buildArgs
 
   let hasTestDriverResult ← hasTestDriver targetLakePackageDir
diff --git a/action.yml b/action.yml
index 37f34e3..c42a2ba 100644
--- a/action.yml
+++ b/action.yml
@@ -20,9 +20,8 @@ inputs:
       alone (e.g. `benchmarks/** !benchmarks/pinned`). An exclusion carries no glob of its own,
       since it already covers its whole subtree, and one matching nothing is reported in the log.
       Quote the value in YAML: a scalar that starts with `!` is otherwise read as a YAML tag.
-      With multiple directories the outputs aggregate: an update or failure in any directory reports
-      as such, and the Mathlib cache prefetch (which understands a single directory) is skipped.
-      This parameter is passed to the lake-package-directory argument of leanprover/lean-action.
+      With multiple directories the outputs aggregate: an update or failure in any directory
+      reports as such, and each directory gets the Mathlib cache if its own manifest needs it.
     required: false
     default: "."
 
@@ -322,21 +321,6 @@ runs:
         ON_SUCCESS: ${{ steps.outcomes.outputs.on-success }}
         ON_FAILURE: ${{ steps.outcomes.outputs.on-failure }}
 
-    - name: Prepare Lean and get Mathlib cache
-      if: steps.validation-mode.outputs.run == 'true' && env.LEAN_UPDATE_FILES_CHANGED == 'true'
-      id: prepare-lean
-      continue-on-error: true
-      uses: leanprover/lean-action@v1
-      with:
-        auto-config: "false"
-        build: "false"
-        test: "false"
-        lint: "false"
-        use-github-cache: "false"
-        lake-package-directory: ${{ inputs.lake_package_directory }}
-      env:
-        GH_TOKEN: ${{ github.token }}
-
     - name: Validate updated Lean package
       if: steps.validation-mode.outputs.run == 'true' && env.LEAN_UPDATE_FILES_CHANGED == 'true'
       id: validate-update

From 728a37548328e1922948bfd412007b12ce4b98e2 Mon Sep 17 00:00:00 2001
From: samuelburnham <45365069+samuelburnham@users.noreply.github.com>
Date: Tue, 1 Sep 2026 16:58:00 -0400
Subject: [PATCH 10/10] feat: Fail validation when a required Mathlib cache is
 missing

Falling back to a source build is not a smaller version of using the
cache: Mathlib takes hours to compile and the run usually dies on the job
timeout, so the warning scrolls past and the answer never arrives. Stop
instead, before the build starts, and report the directory along with
what `lake exe cache get` printed.

`mathlib_cache: optional` restores the old behaviour for anyone who would
rather have a slow answer than none.

The failure travels as a build error rather than an exception because
`createIssue` re-runs validation to compose the issue body; raising here
would leave the notification path with nothing to report.
---
 LeanUpdate/Input.lean                | 22 ++++++++++++++++++++++
 LeanUpdate/PostUpdateValidation.lean | 23 ++++++++++++++++-------
 action.yml                           | 14 ++++++++++++++
 3 files changed, 52 insertions(+), 7 deletions(-)

diff --git a/LeanUpdate/Input.lean b/LeanUpdate/Input.lean
index 633b239..d9eca6a 100644
--- a/LeanUpdate/Input.lean
+++ b/LeanUpdate/Input.lean
@@ -193,6 +193,28 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
     throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
   return kept
 
+/-- What to do when a target package's Mathlib cache cannot be fetched.
+
+Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
+so a run that silently falls back to it costs far more than the one that stops. -/
+public inductive MathlibCache where
+  /-- fail validation when `lake exe cache get` fails -/
+  | require
+  /-- report the failure and build without the cache -/
+  | optional
+deriving Repr, BEq, ToString, HasParser
+
+public instance : Input MathlibCache where
+  envName := "MATHLIB_CACHE"
+  parse := parseAs MathlibCache
+  localValue? := some .require
+
+#guard
+  let lst : List MathlibCache := [.require, .optional]
+  lst.map toString == ["require", "optional"]
+
+#guard (parseAs MathlibCache "optional").toOption == some .optional
+
 /-- The input whether to update the `lean-toolchain` file. -/
 public inductive UpdateLeanToolchain where
   | auto
diff --git a/LeanUpdate/PostUpdateValidation.lean b/LeanUpdate/PostUpdateValidation.lean
index 203cd14..5bc2348 100644
--- a/LeanUpdate/PostUpdateValidation.lean
+++ b/LeanUpdate/PostUpdateValidation.lean
@@ -98,26 +98,35 @@ def dependsOnMathlib (cwd : FilePath) : IO Bool := do
     return false
   return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"
 
-/-- Download Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.
+/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.
 
 Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
 per package; the downloads behind it are pooled in a single per-user directory, so only the first
-package pays for the network. Failing to get the cache only means a slower build, so it is
-reported rather than raised.
+package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
 -/
-def getMathlibCache (cwd : FilePath) : IO Unit := do
+def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
   unless ← dependsOnMathlib cwd do
-    return
+    return .ok ()
   IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
   let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
-  if out.exitCode != 0 then
+  if out.exitCode == 0 then
+    return .ok ()
+  let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
+  match ← GitHub.Action.Input.get MathlibCache with
+  | .optional =>
     IO.println <| log%
       s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
+    return .ok ()
+  | .require =>
+    return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"
 
 /-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
 def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
     IO PostUpdateValidationResult := do
-  getMathlibCache targetLakePackageDir
+  match ← getMathlibCache targetLakePackageDir with
+  | .error e =>
+    return { buildResult := .error e, testResult? := none, lintResult? := none }
+  | .ok _ => pure ()
   let buildResult ← runLakeBuild targetLakePackageDir buildArgs
 
   let hasTestDriverResult ← hasTestDriver targetLakePackageDir
diff --git a/action.yml b/action.yml
index c42a2ba..28c0ef3 100644
--- a/action.yml
+++ b/action.yml
@@ -102,6 +102,17 @@ inputs:
       Build arguments to pass to `lake build` during post-update validation.
     required: false
     default: "--log-level=warning"
+  mathlib_cache:
+    description: |
+      What to do when a target package depends on Mathlib and `lake exe cache get` fails.
+      Allowed values:
+        * `require`: fail validation, reporting the directory and the cache output (default)
+        * `optional`: report the failure and build without the cache
+      Building Mathlib from source takes hours and usually ends in a timeout, so falling back to
+      it silently costs far more than stopping does. Set `optional` when a slow build is
+      preferable to no answer at all.
+    required: false
+    default: "require"
   validate:
     description: |
       Whether to run post-update validation (`lake build`, and `lake test`/`lake lint` when
@@ -330,6 +341,7 @@ runs:
         lake exe leanUpdate validateUpdate
       env:
         BUILD_ARGS: ${{ inputs.build_args }}
+        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
         LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
       shell: bash
       working-directory: ${{ github.action_path }}
@@ -428,6 +440,7 @@ runs:
         # Could be best to use the default token here
         GH_TOKEN: ${{ inputs.token }}
         BUILD_ARGS: ${{ inputs.build_args }}
+        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
         LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
       shell: bash
       working-directory: ${{ github.action_path }}
@@ -452,6 +465,7 @@ runs:
       env:
         GH_TOKEN: ${{ inputs.token }}
         BUILD_ARGS: ${{ inputs.build_args }}
+        MATHLIB_CACHE: ${{ inputs.mathlib_cache }}
         LAKE_PACKAGE_DIRECTORY: ${{ inputs.lake_package_directory }}
       shell: bash
       working-directory: ${{ github.action_path }}