feat: Add a /** package directory glob that descends the tree - #2
Merged
Conversation
`/*` 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.
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.
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.
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.
samuelburnham
marked this pull request as ready for review
August 24, 2026 17:37
samuelburnham
enabled auto-merge (squash)
August 24, 2026 17:42
johnchandlerburnham
approved these changes
Aug 24, 2026
arthurpaulino
approved these changes
Aug 24, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
/*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.Also fixes the repo-sync workflow and updates to the latest available toolchain by default, including for patch releases.