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/.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/.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 }} 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 }} 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/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/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/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 71c79bd..4b82cdf 100644 --- a/Test/Main.lean +++ b/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 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/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 8954a09..e57f3c1 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: "." @@ -59,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"