Exclude dir by samuelburnham · Pull Request #4 · argumentcomputer/lean-update

samuelburnham · 2026-08-28T00:00:33Z

Adds a ! prefix to the lake_package_directory arg which will exclude the given pattern from the paths that lean-update runs over.

Also bumps flake.lock for lean4-nix v4.33.1

A `/**` sweep takes every package under a directory, which is the wrong granularity when one package in the tree must not move — a benchmark pinned to an old toolchain on purpose, say. Without a way to carve it back out, the whole glob has to be abandoned for an explicit list that goes stale as packages are added. An entry prefixed with `!` now subtracts: it names a directory and drops that directory together with everything beneath it, so `benchmarks/** !benchmarks/pinned` covers the tree and spares the one package. Exclusions live in `lake_package_directory` rather than in an input of their own so that no step invoking the action needs a second environment variable kept in sync with the first. Matching compares path components, not string prefixes, so `!benchmarks/slow` cannot swallow `benchmarks/slowfixture`, while trailing slashes and `./` prefixes still name the same directory. An exclusion carrying a glob is rejected, since it already reaches its whole subtree, and one matching nothing is reported: a typo there silently updates the package it was meant to protect.

Without a `permissions` block the jobs run with whatever the repository grants by default, which on many repositories is write access to contents, issues, and pull requests. The E2E jobs update fixtures only inside the runner's own checkout and never write back, and the action's `gh` calls read the public list of Lean releases, so `contents: read` covers everything they do.

Neither workflow writes to the repository: both build and assert inside the runner's own checkout, and the `gh` calls underneath read public data. Without a `permissions` block they ran with whatever the repository grants by default, which is commonly write access to contents, issues, and pull requests.

The App token existed only to work around GitHub's guard against a workflow triggering itself, which leaves a GITHUB_TOKEN pull request with no CI runs until a maintainer releases them. Trading that back for one fewer credential to install and rotate means the self-update PR opens with checks pending until someone pushes to the branch or closes and reopens it. The job needs contents and pull-requests write to open the PR, and issues write for the default `on_update_fails: issue` path.

Opening a pull request with `github.token` carries two constraints that are documented in peter-evans/create-pull-request but nowhere here, so they surface as a 403 or a PR with no checks: the repository must allow GitHub Actions to create pull requests, and such a PR does not trigger workflow runs. The README examples already carried the write scopes, attributed to private repositories. The default token has been read-only regardless of visibility since February 2023, so the note said the right thing for the wrong reason. Also note that a `!` exclusion has to be quoted in YAML, since a scalar opening with `!` is read as a tag.

A `!` with no path after it resolves to the workspace root, which is at or above every target, so the whole expansion is filtered away and the run fails reporting that no package directory was found — true, but not where the reader would start looking. Name the actual mistake.

The jobs set `on_update_succeeds: silent` but left the failure path at its default, so a fixture that stopped building would have the action open an issue. The workflow now runs with a read-only token, which turns that into a 403 on top of the failure it is reporting. A red check is the signal a test workflow owes its reader.

The prefetch delegated to leanprover/lean-action, which takes one directory and uses it as the working directory of its every step. A list, a glob, or an exclusion is not a directory, so the step could not start, and `continue-on-error` turned that into a red mark nobody read. Anyone globbing a tree of Mathlib packages then built them from source. Validation already walks each target package, so fetch the cache there: one manifest check, then `lake exe cache get` for the packages that want it. Every package root has its own `.lake/packages/mathlib` and needs its own unpack, while the downloads pool in one per-user directory, so the extra directories cost no extra network. Elan is installed by this action's own step, so nothing else was keeping lean-action here.

Falling back to a source build is not a smaller version of using the cache: Mathlib takes hours to compile and the run usually dies on the job timeout, so the warning scrolls past and the answer never arrives. Stop instead, before the build starts, and report the directory along with what `lake exe cache get` printed. `mathlib_cache: optional` restores the old behaviour for anyone who would rather have a slow answer than none. The failure travels as a build error rather than an exception because `createIssue` re-runs validation to compose the issue body; raising here would leave the notification path with nothing to report.

samuelburnham · 2026-08-28T00:00:33Z