Exclude dir

.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
@@ -331,3 +336,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

.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

.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

.github/workflows/update.yml

@@ -5,24 +5,20 @@ 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
     steps:
       - 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 }}

LeanUpdate/Input.lean

@@ -104,21 +104,61 @@ 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
 GitHub workspace. An entry ending in `/*` expands to the immediate subdirectories of its parent
 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

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

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

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