From d4a8a4426b3d738f6442d61abdb7ff3f84bde56e Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 24 Aug 2026 12:11:53 -0400 Subject: [PATCH 1/4] feat: Add a `/**` package directory glob that descends the tree MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `/*` reads only the immediate subdirectories of its parent, so a package required by path from another package — a fixture workspace nested inside the workspace that consumes it — is unreachable: naming the parent misses it, and the parent's own glob stops one level short. Listing every such path by hand works until someone adds another one. `/**` expands like `/*` but walks the whole tree. Both forms now prune dotted directories: `.lake/packages/*` are all package roots carrying their own lakefiles, and a recursive walk that entered one would update vendored copies of other people's packages instead of the repository's own. `/*` keeps its existing semantics, so no current caller changes behavior. --- .envrc | 5 +++ .gitignore | 1 + LeanUpdate/Input.lean | 42 +++++++++++++++---- Test/Main.lean | 4 ++ Test/PackageDirectoryGlob.lean | 76 ++++++++++++++++++++++++++++++++++ action.yml | 9 ++-- 6 files changed, 126 insertions(+), 11 deletions(-) create mode 100644 .envrc create mode 100644 Test/PackageDirectoryGlob.lean diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..13060e1 --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index c0925c2..20491ea 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ /.lake +/.direnv tmp/* !tmp/.gitkeep diff --git a/LeanUpdate/Input.lean b/LeanUpdate/Input.lean index d75773e..cf28c55 100644 --- a/LeanUpdate/Input.lean +++ b/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)) diff --git a/Test/Main.lean b/Test/Main.lean index 71c79bd..cb7af78 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,6 +1,7 @@ module import Test.LakeToolchainResolution +import Test.PackageDirectoryGlob import Test.UpdateDependenciesEnv /-- Run the test suite and dispatch subprocess invocations used by individual tests. -/ @@ -9,6 +10,9 @@ public def main (args : List String) : IO Unit := do | ["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.UpdateDependenciesEnv.test LeanUpdateTest.LakeToolchainResolution.test + LeanUpdateTest.PackageDirectoryGlob.test diff --git a/Test/PackageDirectoryGlob.lean b/Test/PackageDirectoryGlob.lean new file mode 100644 index 0000000..17a64af --- /dev/null +++ b/Test/PackageDirectoryGlob.lean @@ -0,0 +1,76 @@ +module + +import LeanUpdate.IO +import LeanUpdate.Input + +open System + +namespace LeanUpdateTest.PackageDirectoryGlob + +def writeLakefile (dir : FilePath) (name : String) : IO Unit := do + IO.FS.createDirAll dir + IO.FS.writeFile (dir / name) "" + +/-- Lay out a workspace with packages at two depths, a dependency checkout under `.lake`, +and a plain directory holding no lakefile. -/ +def buildWorkspace (root : FilePath) : IO Unit := do + let benchmarks := root / "Benchmarks" + writeLakefile (benchmarks / "Compile") "lakefile.toml" + writeLakefile (benchmarks / "Catalog") "lakefile.toml" + writeLakefile (benchmarks / "Catalog" / "FixtureA") "lakefile.toml" + writeLakefile (benchmarks / "Catalog" / "FixtureB") "lakefile.lean" + writeLakefile (benchmarks / "Compile" / ".lake" / "packages" / "mathlib") "lakefile.lean" + IO.FS.createDirAll (benchmarks / "NotAPackage") + +def checkExpansion (expected : FilePath → Array FilePath) : IO Unit := do + let workspace : FilePath := ⟨← IO.getEnv! "GITHUB_WORKSPACE"⟩ + let got ← getTargetLakePackageDirectories + let want := expected workspace + unless got.map (·.toString) == want.map (·.toString) do + throw <| IO.userError <| + s!"unexpected expansion\n got: {got.map (·.toString)}\n" ++ + s!" expected: {want.map (·.toString)}" + +/-- `/**` reaches the fixtures nested inside `Catalog`, and stops at `.lake`. -/ +public def runRecursive : IO Unit := + checkExpansion fun workspace => + let benchmarks := workspace / "Benchmarks" + #[ + benchmarks / "Catalog", + benchmarks / "Catalog" / "FixtureA", + benchmarks / "Catalog" / "FixtureB", + benchmarks / "Compile" + ] + +/-- `/*` stays one level down, as it did before `/**` existed. -/ +public def runShallow : IO Unit := + checkExpansion fun workspace => + let benchmarks := workspace / "Benchmarks" + #[benchmarks / "Catalog", benchmarks / "Compile"] + +def runInWorkspace (workspace : FilePath) (packageDir : String) (mode : String) : IO Unit := do + let currentExe ← IO.appPath + let out ← IO.Process.output { + cmd := currentExe.toString + args := #[mode] + env := #[ + ("GITHUB_WORKSPACE", some workspace.toString), + ("LAKE_PACKAGE_DIRECTORY", some packageDir) + ] + } + if out.exitCode != 0 then + throw <| IO.userError s!"{mode} failed\nstdout:\n{out.stdout}\nstderr:\n{out.stderr}" + +/-- +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. +-/ +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" + +end LeanUpdateTest.PackageDirectoryGlob diff --git a/action.yml b/action.yml index 8954a09..b9cc8b4 100644 --- a/action.yml +++ b/action.yml @@ -11,9 +11,12 @@ inputs: The directory containing the Lake package to update, relative to the workspace. Accepts a comma- or space-separated list of directories, and an entry ending in `/*` expands to every immediate subdirectory containing a lakefile, so a repository of sibling - packages can be updated in one invocation (e.g. `templates/*`). 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. + 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 + 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 default: "." From 7fe8a249528cca62adc57fef6c0c3bcf75c79daa Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 24 Aug 2026 13:10:14 -0400 Subject: [PATCH 2/4] ci: Sync from upstream via the shared ci-workflows workflow Replace the inline `repo-sync/github-sync` step with a call to `argumentcomputer/ci-workflows/.github/workflows/repo-sync.yml`, so this repo tracks the org's shared implementation rather than its own copy. The shared workflow drops the third-party action for `gh repo sync` and replaces the deprecated `tibdex/github-app-token` with `actions/create-github-app-token`, requesting only the contents and workflows scopes the sync needs. --- .github/workflows/repo-sync.yml | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/.github/workflows/repo-sync.yml b/.github/workflows/repo-sync.yml index a172f35..fe58941 100644 --- a/.github/workflows/repo-sync.yml +++ b/.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 }} From 8f256900de2f88a8bfa5b63e9ead9e672a3cd99f Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 24 Aug 2026 13:27:28 -0400 Subject: [PATCH 3/4] feat: Move a lagging pinned dep as far towards the toolchain as it tags MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. Requiring an exact tag match left such a dependency at whatever it was pinned to before — v4.31.0 under a v4.33.1 toolchain, two releases behind and certain not to build — when v4.33.0 was available and is the pairing a maintainer picks by hand. A managed dependency now moves to the newest tag it publishes that does not exceed the target, and only one with nothing at or below the target keeps its pin. A stable target never falls back onto a pre-release, since pinning to an rc underneath a stable toolchain is worse than staying put; a pre-release target may, having nothing more stable to prefer at that version. The selection is pure and lives in `pickNewestNotExceeding`, covered by `Test.PinnedTagFallback`. It cannot be covered by `#guard` here: evaluating one means calling `parseLeanTagVersion` across a module boundary, which the elaborator resolves to a native symbol it has not loaded. The pinned-tags E2E asserted toolchain and pin were equal, which no longer holds whenever the dependency skipped that release, so it now computes the newest batteries tag at or below the toolchain and expects that. Its manifest check compared against the toolchain version for the same reason, and now compares against the pin. Self-contained tests run before those needing Elan or the network, so a machine lacking either still gets a verdict on the rest. --- .github/workflows/e2e_test.yml | 25 ++++++-- LeanUpdate/BumpPinnedDeps.lean | 95 +++++++++++++++++++++++------ LeanUpdate/UpdateLeanToolchain.lean | 7 ++- Test/Main.lean | 9 ++- Test/PinnedTagFallback.lean | 43 +++++++++++++ action.yml | 8 ++- 6 files changed, 158 insertions(+), 29 deletions(-) create mode 100644 Test/PinnedTagFallback.lean diff --git a/.github/workflows/e2e_test.yml b/.github/workflows/e2e_test.yml index b21c00b..477c566 100644 --- a/.github/workflows/e2e_test.yml +++ b/.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 diff --git a/LeanUpdate/BumpPinnedDeps.lean b/LeanUpdate/BumpPinnedDeps.lean index 53433ad..24d478a 100644 --- a/LeanUpdate/BumpPinnedDeps.lean +++ b/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 diff --git a/LeanUpdate/UpdateLeanToolchain.lean b/LeanUpdate/UpdateLeanToolchain.lean index d8be83f..df42642 100644 --- a/LeanUpdate/UpdateLeanToolchain.lean +++ b/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` diff --git a/Test/Main.lean b/Test/Main.lean index cb7af78..4b82cdf 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -2,9 +2,13 @@ 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 @@ -13,6 +17,7 @@ public def main (args : List String) : IO Unit := do | ["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 - LeanUpdateTest.PackageDirectoryGlob.test diff --git a/Test/PinnedTagFallback.lean b/Test/PinnedTagFallback.lean new file mode 100644 index 0000000..25e4fc8 --- /dev/null +++ b/Test/PinnedTagFallback.lean @@ -0,0 +1,43 @@ +module + +import LeanUpdate.BumpPinnedDeps + +namespace LeanUpdateTest.PinnedTagFallback + +def check (what : String) (tags : Array String) (target : String) (expected : Option String) : + IO Unit := do + let got := pickNewestNotExceeding tags target + unless got == expected do + throw <| IO.userError s!"{what}: pick {tags} at {target} gave {got}, expected {expected}" + +/-- +Lean ships patch releases that most of the ecosystem never tags — there is no `batteries` +`v4.33.1` — so a dependency that cannot match the toolchain exactly moves to the newest tag it +does publish below it, rather than staying stranded at its old pin. +-/ +public def test : IO Unit := do + check "exact tag wins when published" + #["v4.32.0", "v4.33.0", "v4.33.1"] "v4.33.1" (some "v4.33.1") + + check "an untagged patch release falls back to the release below it" + #["v4.31.0", "v4.32.0", "v4.33.0"] "v4.33.1" (some "v4.33.0") + + check "a tag newer than the toolchain is never selected" + #["v4.33.0", "v4.34.0", "v4.34.0-rc1"] "v4.33.1" (some "v4.33.0") + + check "a stable target skips pre-releases that sort higher" + #["v4.33.0", "v4.33.1-rc1"] "v4.33.1" (some "v4.33.0") + + check "a pre-release target may land on a pre-release" + #["v4.33.0", "v4.33.1-rc1"] "v4.33.1-rc2" (some "v4.33.1-rc1") + + check "nothing at or below the target means the pin cannot move" + #["v4.34.0"] "v4.33.1" none + + check "tags that are not Lean versions are ignored" + #["main", "nightly", "v1"] "v4.33.1" none + + check "an unreachable remote reports no tags and cannot move" + #[] "v4.33.1" none + +end LeanUpdateTest.PinnedTagFallback diff --git a/action.yml b/action.yml index b9cc8b4..e57f3c1 100644 --- a/action.yml +++ b/action.yml @@ -62,9 +62,11 @@ inputs: * `lake-update`: run `lake update` to advance dependencies (the upstream behavior). * `pinned-tags`: bump `lean-toolchain` to the latest Lean version tag, moving the pinned `rev` of managed git dependencies with it. A dependency that has not tagged that version - yet keeps its pin and is reported; post-update validation decides whether the result - builds. Use this when dependencies are pinned to Lean-version tags (e.g. `v4.31.0`) - rather than tracking a branch. + — Lean ships patch releases most of the ecosystem skips, so there is no `batteries` + `v4.33.1` — moves to the newest tag it does publish below the target instead. Only one + with nothing at or below the target keeps its pin and is reported; post-update + validation decides whether the result builds. Use this when dependencies are pinned to + Lean-version tags (e.g. `v4.31.0`) rather than tracking a branch. Default: `lake-update` required: false default: "lake-update" From d3a1de40db978277813c4eaf3ad751ce34472a85 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 24 Aug 2026 13:34:15 -0400 Subject: [PATCH 4/4] ci: Open the self-update PR with a GitHub App token MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A pull request opened with the default GITHUB_TOKEN does not start workflow runs — GitHub's guard against a workflow triggering itself — so every self update sat behind a maintainer clicking "Approve and run" before any CI told them whether the bump built. An App token is a distinct identity, so its PRs run unattended. Needs TOKEN_APP_ID and TOKEN_APP_PRIVATE_KEY on this repository, with the App installed on it. --- .github/workflows/update.yml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index 6816119..44f3180 100644 --- a/.github/workflows/update.yml +++ b/.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 }}