feat: Add a /** package directory glob that descends the tree

.envrc

@@ -0,0 +1,5 @@
+# Trust the flake's nixConfig (the Cachix substituter) without prompting, so
+# the cache applies to every nix command in this shell, not just the devShell
+# build. Non-direnv users are unaffected: nix asks them before using it.
+export NIX_CONFIG="accept-flake-config = true"
+use flake

.github/workflows/e2e_test.yml

@@ -177,7 +177,10 @@ jobs:
           on_update_fails: "silent"
           lake_package_directory: "./Fixtures/PinnedTags"
 
-      - name: The toolchain and the pinned dependency must move together
+      # batteries does not tag every Lean patch release — there is no batteries v4.33.1 — so the
+      # pin is expected to land on the newest stable batteries tag that does not exceed the
+      # toolchain, which equals the toolchain only when batteries tagged that release.
+      - name: The pinned dependency must move as close to the toolchain as its tags allow
         run: |
           toolchain=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
           pin=$(grep -o '@ "[^"]*"' Fixtures/PinnedTags/lakefile.lean | cut -d'"' -f2)
@@ -186,15 +189,27 @@ jobs:
             echo "Error: lean-toolchain was not bumped"
             exit 1
           fi
-          if [ "$toolchain" != "$pin" ]; then
-            echo "Error: dependency pinned to $pin but toolchain is $toolchain"
+          tags=$(git ls-remote --tags --refs \
+            https://github.com/leanprover-community/batteries \
+            | sed 's#.*refs/tags/##' \
+            | grep -E '^v[0-9]+\.[0-9]+\.[0-9]+$')
+          if printf '%s\n' "$tags" | grep -qx "$toolchain"; then
+            expected="$toolchain"
+          else
+            expected=$(printf '%s\n%s\n' "$tags" "$toolchain" \
+              | sort -V \
+              | awk -v t="$toolchain" '$0 == t { exit } { last = $0 } END { print last }')
+          fi
+          echo "expected=$expected"
+          if [ "$pin" != "$expected" ]; then
+            echo "Error: pinned to $pin, but $expected is the newest batteries tag <= $toolchain"
             exit 1
           fi
 
       - name: The manifest must be refreshed to match the new pin
         run: |
-          if ! grep -q "\"inputRev\": \"$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)\"" \
-            Fixtures/PinnedTags/lake-manifest.json; then
+          pin=$(grep -o '@ "[^"]*"' Fixtures/PinnedTags/lakefile.lean | cut -d'"' -f2)
+          if ! grep -q "\"inputRev\": \"$pin\"" Fixtures/PinnedTags/lake-manifest.json; then
             echo "Error: lake-manifest.json still points at the old revision"
             cat Fixtures/PinnedTags/lake-manifest.json
             exit 1

.github/workflows/repo-sync.yml

@@ -6,23 +6,19 @@ on:
   - cron:  "0 0 * * *"
   workflow_dispatch:
 
+# The sync authenticates with a GitHub App installation token, so the job needs
+# nothing from `secrets.GITHUB_TOKEN`.
+permissions: {}
+
 jobs:
   repo-sync:
     name: Sync upstream changes
-    runs-on: ubuntu-latest
-    steps:
-      - uses: actions/checkout@v4
-        with:
-          persist-credentials: false
-      - uses: tibdex/github-app-token@v2
-        id: generate-token
-        with:
-          app_id: ${{ secrets.TOKEN_APP_ID }}
-          private_key: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}
-      - name: repo-sync
-        uses: repo-sync/github-sync@v2
-        with:
-          source_repo: "https://github.com/leanprover-community/lean-update"
-          source_branch: "main"
-          destination_branch: "main"
-          github_token: ${{ steps.generate-token.outputs.token }}
+    uses: argumentcomputer/ci-workflows/.github/workflows/repo-sync.yml@main
+    with:
+      repository: leanprover-community/lean-update
+      # This fork's default branch is `dev`; `main` is kept as a plain mirror
+      # of upstream, so both sides of the sync share the branch name.
+      branch: main
+    secrets:
+      TOKEN_APP_ID: ${{ secrets.TOKEN_APP_ID }}
+      TOKEN_APP_PRIVATE_KEY: ${{ secrets.TOKEN_APP_PRIVATE_KEY }}

.github/workflows/update.yml

@@ -11,6 +11,18 @@ jobs:
     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 }}

.gitignore

@@ -1,3 +1,4 @@
 /.lake
+/.direnv
 tmp/*
 !tmp/.gitkeep

LeanUpdate/BumpPinnedDeps.lean

@@ -92,13 +92,21 @@ def parseRequireBlocks (lines : Array String) : Array RequireBlock := Id.run do
     blocks[0]!.rev == some "v4.31.0" &&
     blocks[0]!.revLine == some 5
 
-/-- Whether a git remote has a tag with the given name. -/
-def remoteHasTag (gitUrl tag : String) : IO Bool := do
+/-- Every tag a git remote publishes, as bare tag names.
+
+An unreachable remote yields no tags rather than an error, which reads downstream as "this
+dependency cannot move" — the same conclusion as a remote that simply lacks the tag. -/
+def remoteTags (gitUrl : String) : IO (Array String) := do
   let out ← IO.Process.output {
     cmd := "git"
-    args := #["ls-remote", "--tags", gitUrl, s!"refs/tags/{tag}"]
+    args := #["ls-remote", "--tags", "--refs", gitUrl]
   }
-  pure <| out.exitCode == 0 && !out.stdout.trimAscii.copy.isEmpty
+  if out.exitCode != 0 then
+    return #[]
+  return (out.stdout.splitOn "\n").foldl (init := #[]) fun acc line =>
+    match line.splitOn "refs/tags/" with
+    | [_, tag] => acc.push tag.trimAscii.copy
+    | _ => acc
 
 /-- Whether a pinned `rev` looks like a Lean version tag, e.g. `v4.32.0` or `v4.33.0-rc1`.
 
@@ -119,6 +127,44 @@ def isLeanVersionTag (rev : String) : Bool :=
 
 #guard isLeanVersionTag "v1" == false
 
+/-- Whether a Lean version tag names a pre-release, e.g. `v4.33.0-rc1`. -/
+def isPrereleaseTag (tag : String) : Bool :=
+  tag.contains '-'
+
+/-- The newest Lean version tag in `tags` that does not exceed `target`.
+
+Lean ships patch releases that most of the ecosystem never tags: there is no `batteries`
+`v4.33.1`, because `v4.33.0` is still the right batteries for a `v4.33.1` toolchain. Holding
+such a dependency at its old pin would strand it releases behind, so it moves as far as it can
+instead — which is the pairing a maintainer picks by hand.
+
+A stable target never falls back onto a pre-release: pinning a dependency to an rc underneath a
+stable toolchain is worse than leaving it where it is. A pre-release target may, since there is
+nothing more stable to prefer at that version. -/
+public def pickNewestNotExceeding (tags : Array String) (target : String) : Option String :=
+    Id.run do
+  let some targetVer := (parseLeanTagVersion target).toOption
+    | return none
+  let allowPrerelease := isPrereleaseTag target
+  let mut best : Option (String × Lake.StdVer) := none
+  for tag in tags do
+    unless isLeanVersionTag tag do
+      continue
+    if isPrereleaseTag tag && !allowPrerelease then
+      continue
+    let some ver := (parseLeanTagVersion tag).toOption
+      | continue
+    if targetVer < ver then
+      continue
+    match best with
+    | some (_, bestVer) => if bestVer < ver then best := some (tag, ver)
+    | none => best := some (tag, ver)
+  return best.map Prod.fst
+
+-- Cases live in `Test.PinnedTagFallback` rather than in `#guard`s here: evaluating them means
+-- calling `parseLeanTagVersion` across a module boundary, which the elaborator resolves to a
+-- native symbol it has not loaded.
+
 /-- Whether a require block is managed by the `PINNED_DEPS` input.
 
 An empty input list means "every git require pinned to a Lean version tag". A dependency pinned
@@ -254,22 +300,35 @@ def bumpPackage (pinnedDeps : PinnedDeps) (target : String) (targetDir : FilePat
         IO.println <| log% s!"Not managing {name}: {reason}."
 
   -- The toolchain is the thing being updated, so it always moves to the target. Each managed
-  -- dependency moves with it when its remote has the target tag; one that lags keeps its pin
-  -- and is reported, and post-update validation decides whether the mixture still builds.
-  -- Comparing per file also lets a dependency that tagged the release late catch up on a rerun
-  -- after the toolchain has already moved.
+  -- dependency moves with it when its remote has the target tag, and otherwise as far towards it
+  -- as that remote allows; only one with nothing at or below the target keeps its pin, and
+  -- post-update validation decides whether the mixture still builds. Comparing per file also
+  -- lets a dependency that tagged the release late catch up on a rerun after the toolchain has
+  -- already moved.
   let mut newLines := lines
   let mut bumped : Array String := #[]
   for b in managed do
     if b.rev == some target then
       continue
     if let (some url, some idx) := (b.git, b.revLine) then
-      if ← remoteHasTag url target then
-        newLines := newLines.set! idx (setRevLine newLines[idx]! target)
-        bumped := bumped.push (b.name.getD url)
-      else
+      let who := b.name.getD url
+      let tags ← remoteTags url
+      let choice :=
+        if tags.contains target then some target else pickNewestNotExceeding tags target
+      match choice with
+      | some tag =>
+        if b.rev == some tag then
+          IO.println <| log%
+            s!"{who} has no {target} tag; its pin is already at {tag}, the newest below it."
+        else
+          newLines := newLines.set! idx (setRevLine newLines[idx]! tag)
+          bumped := bumped.push who
+          unless tag == target do
+            IO.println <| log%
+              s!"{who} has no {target} tag; pinning it to {tag}, the newest below it."
+      | none =>
         IO.println <| log%
-          s!"{b.name.getD url} has no {target} tag yet; leaving its pin at {b.rev.getD "?"}."
+          s!"{who} has no {target} tag nor any earlier one; leaving its pin at {b.rev.getD "?"}."
 
   let toolchainBumped := s!"leanprover/lean4:{target}" != currentToolchain
   if !toolchainBumped && bumped.isEmpty then
@@ -301,10 +360,12 @@ it.
 
 The toolchain bump is never gated on the dependencies: updating the toolchain is the point of
 this action. A managed dependency whose remote has the target tag is bumped in lockstep and its
-manifest entry refreshed; one that has not tagged the release yet keeps its pin and is
-reported, and post-update validation decides whether the mixture still builds. Because each
-file is compared to the target individually, a dependency that tags the release late catches up
-on a rerun after the toolchain has already moved.
+manifest entry refreshed. One that never tagged the release — Lean ships patch releases that
+most of the ecosystem skips — moves instead to the newest tag it does publish below the target,
+the pairing a maintainer would pick by hand. Only a dependency with nothing at or below the
+target keeps its pin and is reported, and post-update validation decides whether the mixture
+still builds. Because each file is compared to the target individually, a dependency that tags
+the release late catches up on a rerun after the toolchain has already moved.
 
 Managed dependencies are the names listed in `PinnedDeps`, or, when that list is empty, every
 git `require` in the lakefile pinned to a Lean version tag. A dependency pinned to a commit hash

LeanUpdate/Input.lean

@@ -84,12 +84,34 @@ public def getTargetLakePackageDirectory : IO FilePath := do
   let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
   pure <| resolveLakePackageDir workspace? packageDir
 
+/-- whether `dir` is itself a Lake package root -/
+def hasLakefile (dir : FilePath) : IO Bool := do
+  if (← (dir / "lakefile.toml").pathExists) then return true
+  (dir / "lakefile.lean").pathExists
+
+/-- Every descendant of `root` that is a Lake package root, in directory order.
+
+Dotted directories are pruned. `.lake` holds the dependency checkouts of an already-configured
+package, each a package root in its own right, so descending into one would update vendored
+copies of other people's packages instead of the repository's own. -/
+partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
+  let mut found : Array FilePath := #[]
+  for child in (← root.readDir) do
+    if !(← child.path.isDir) then continue
+    if child.fileName.startsWith "." then continue
+    if (← hasLakefile child.path) then
+      found := found.push child.path
+    found := found ++ (← lakePackagesUnder child.path)
+  return found
+
 /-- 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 subdirectories of its parent that
-contain a lakefile, sorted by name, so a repository of sibling packages can be updated in one
-invocation (e.g. `templates/*`). -/
+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`. -/
 public def getTargetLakePackageDirectories : IO (Array FilePath) := do
   let packageDir ← GitHub.Action.Input.get LakePackageDirectory
   let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
@@ -99,14 +121,18 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
     |>.filter (fun s => !s.isEmpty)
   let mut dirs : Array FilePath := #[]
   for entry in entries do
-    if entry.endsWith "/*" then
+    if entry.endsWith "/**" then
+      let parent := resolveLakePackageDir workspace? (FilePath.mk (entry.dropEnd 3).copy)
+      let found ← lakePackagesUnder parent
+      dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
+    else if entry.endsWith "/*" then
       let parent := resolveLakePackageDir workspace? (FilePath.mk (entry.dropEnd 2).copy)
       let mut found : Array FilePath := #[]
       for child in (← parent.readDir) do
-        if (← child.path.isDir) then
-          if (← (child.path / "lakefile.toml").pathExists)
-              || (← (child.path / "lakefile.lean").pathExists) then
-            found := found.push child.path
+        if !(← child.path.isDir) then continue
+        if child.fileName.startsWith "." then continue
+        if (← hasLakefile child.path) then
+          found := found.push child.path
       dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
     else
       dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))

LeanUpdate/UpdateLeanToolchain.lean

@@ -97,8 +97,11 @@ def filterLeanReleaseByTime (releases : Array LeanRelease) (cutoff? : Option Dat
   | none => releases
 
 /-- parse `name` part of LeanRelease.
-This function is only for tagged releases. -/
-def parseLeanTagVersion (s : String) : Except String StdVer :=
+This function is only for tagged releases.
+
+Exposed so that downstream `#guard`s comparing version tags can evaluate it. -/
+@[expose]
+public def parseLeanTagVersion (s : String) : Except String StdVer :=
   StdVer.parse (if s.startsWith "v" then (s.drop 1).copy else s)
 
 -- test for `parseLeanTagVersion`

Test/Main.lean

@@ -1,14 +1,23 @@
 module
 
 import Test.LakeToolchainResolution
+import Test.PackageDirectoryGlob
+import Test.PinnedTagFallback
 import Test.UpdateDependenciesEnv
 
-/-- Run the test suite and dispatch subprocess invocations used by individual tests. -/
+/-- Run the test suite and dispatch subprocess invocations used by individual tests.
+
+The self-contained tests run first, so that a test needing an Elan install or a network fetch
+cannot mask them by failing on a machine that lacks one. -/
 public def main (args : List String) : IO Unit := do
   match args with
   | ["inner"] => LeanUpdateTest.UpdateDependenciesEnv.runInner
   | ["update"] => LeanUpdateTest.UpdateDependenciesEnv.runAsFakeLake args
   | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
+  | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
+  | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
   | _ => do
+    LeanUpdateTest.PinnedTagFallback.test
+    LeanUpdateTest.PackageDirectoryGlob.test
     LeanUpdateTest.UpdateDependenciesEnv.test
     LeanUpdateTest.LakeToolchainResolution.test