Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
samuelburnham merged 10 commits into from
Sep 2, 2026
Merged

Exclude dir #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
265fcda
feat: Exclude a directory from a package directory glob
samuelburnham Aug 27, 2026
8075eb8
Update flake.lock
samuelburnham Aug 27, 2026
448b22a
ci: Restrict the E2E workflow to a read-only token
samuelburnham Aug 28, 2026
5951955
ci: Restrict the CI and test workflows to a read-only token
samuelburnham Aug 28, 2026
aece5d9
ci: Open the self-update PR with GITHUB_TOKEN
samuelburnham Aug 28, 2026
ac315a0
docs: Record what the default token cannot do
samuelburnham Sep 1, 2026
50d4c61
fix: Reject a bare `!` package directory exclusion
samuelburnham Sep 1, 2026
fe7af4b
ci: Silence the failure outcome in the test workflow
samuelburnham Sep 1, 2026
b0ed23f
fix: Get the Mathlib cache for every target package
samuelburnham Sep 1, 2026
728a375
feat: Fail validation when a required Mathlib cache is missing
samuelburnham Sep 1, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 40 additions & 0 deletions .github/workflows/e2e_test.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
- dev
workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
contents: read

jobs:
success_e2e_test:
runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
- name: This update should succeed
if: steps.update.outputs.result != 'update-success'
run: exit 1

# An exclusion carves a package back out of the set the action would otherwise
# update, leaving its lean-toolchain untouched.
excluded_directory_e2e_test:
runs-on: ubuntu-latest
steps:
- name: Checkout code
uses: actions/checkout@v6

- name: Bump two packages, excluding one of them
id: update
uses: ./
with:
bump_mode: "pinned-tags"
on_update_succeeds: "silent"
on_update_fails: "silent"
lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

- name: The excluded package must be left alone
run: |
a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
echo "PinnedTags=$a SmokeSuccess=$b"
if [ "$a" = "v4.31.0" ]; then
echo "Error: the included package was not bumped"
exit 1
fi
if [ "$b" != "v4.16.0" ]; then
echo "Error: the excluded package was bumped to $b"
exit 1
fi

- name: This update should succeed
if: steps.update.outputs.result != 'update-success'
run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.
Fixed
5 changes: 5 additions & 0 deletions .github/workflows/lean_action_ci.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
- dev
workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
contents: read

jobs:
build:
runs-on: ubuntu-latest
Expand Down
10 changes: 10 additions & 0 deletions .github/workflows/test.yaml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
- dev
workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
contents: read

jobs:
has_dependency_output_test_true:
runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
uses: ./
with:
on_update_succeeds: "silent"
on_update_fails: "silent"
lake_package_directory: "./Fixtures/HasDep"

- name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
uses: ./
with:
on_update_succeeds: "silent"
on_update_fails: "silent"
lake_package_directory: "./Fixtures/SmokeSuccess"
- name: The result should be no dependency
if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
uses: ./
with:
on_update_succeeds: "silent"
on_update_fails: "silent"
lake_package_directory: "./Fixtures/SmokeSuccess"

- name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
uses: ./
with:
on_update_succeeds: "silent"
on_update_fails: "silent"
lake_package_directory: "./Fixtures/HasDep"

- name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
uses: ./
with:
on_update_succeeds: "silent"
on_update_fails: "silent"
lake_package_directory: "./Fixtures/SmokeSuccess"
update_lean_toolchain: "never"

Expand Down
18 changes: 7 additions & 11 deletions .github/workflows/update.yml
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
- cron: '0 0 * * *' # every day at midnight
workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
contents: write
pull-requests: write
issues: write

jobs:
update:
runs-on: ubuntu-latest
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 }}
87 changes: 81 additions & 6 deletions LeanUpdate/Input.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
found := found ++ (← lakePackagesUnder child.path)
return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
raw.split (fun c => c == ',' || c.isWhitespace)
|>.map (fun s => s.trimAscii.copy)
|>.filter (fun s => !s.isEmpty)
|>.toList

#guard
splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
(pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
let packageDir ← GitHub.Action.Input.get LakePackageDirectory
let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
let raw := packageDir.val.toString
let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
|>.map (fun s => s.trimAscii.copy)
|>.filter (fun s => !s.isEmpty)
let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
for entry in exclusions do
if entry.isEmpty then
throw <| IO.userError <|
"A bare '!' names no directory to exclude. Write the path immediately after it, " ++
"as in '!benchmarks/pinned'."
if entry.any (· == '*') then
throw <| IO.userError <|
s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
"covers everything beneath it."
let mut dirs : Array FilePath := #[]
for entry in entries do
if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
else
dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
if dirs.isEmpty then
let excludedDirs := exclusions.map (fun entry =>
resolveLakePackageDir workspace? (FilePath.mk entry))
-- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
-- cost of the typo is that a package meant to be protected is updated instead.
for (entry, excludedDir) in exclusions.zip excludedDirs do
unless dirs.any (isAtOrUnder excludedDir ·) do
IO.println <| log%
s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
if kept.isEmpty then
throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
return dirs
return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
/-- fail validation when `lake exe cache get` fails -/
| require
/-- report the failure and build without the cache -/
| optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
envName := "MATHLIB_CACHE"
parse := parseAs MathlibCache
localValue? := some .require

#guard
let lst : List MathlibCache := [.require, .optional]
lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down
33 changes: 33 additions & 0 deletions LeanUpdate/PostUpdateValidation.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
!result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
let manifest := cwd / "lake-manifest.json"
if !(← manifest.pathExists) then
return false
return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
unless ← dependsOnMathlib cwd do
return .ok ()
IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
if out.exitCode == 0 then
return .ok ()
let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
match ← GitHub.Action.Input.get MathlibCache with
| .optional =>
IO.println <| log%
s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
return .ok ()
| .require =>
return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
IO PostUpdateValidationResult := do
match ← getMathlibCache targetLakePackageDir with
| .error e =>
return { buildResult := .error e, testResult? := none, lintResult? := none }
| .ok _ => pure ()
let buildResult ← runLakeBuild targetLakePackageDir buildArgs

let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down
12 changes: 9 additions & 3 deletions README.md
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
update_lean:
# this is needed for private repositories
# The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
# Opening the pull request also needs `Allow GitHub Actions to create and approve pull
# requests` under Settings > Actions > General > Workflow permissions.
permissions:
contents: write
pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
update_lean:
# this is needed for private repositories
# The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
# Opening the pull request also needs `Allow GitHub Actions to create and approve pull
# requests` under Settings > Actions > General > Workflow permissions.
permissions:
contents: write
pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
update_lean:
# this is needed for private repositories
# The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
# Opening the pull request also needs `Allow GitHub Actions to create and approve pull
# requests` under Settings > Actions > General > Workflow permissions.
permissions:
contents: write
pull-requests: write
Expand Down
2 changes: 2 additions & 0 deletions Test/Main.lean
View file
Open in desktop
Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
| ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
| ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
| ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
| ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
| ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
| _ => do
LeanUpdateTest.PinnedTagFallback.test
LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading
, 'i'); if (__m === '*' || __re.test(location.href)) { injectUserscript("// Add copy buttons to all 
 blocks\n(function() {\n function addCopyButtons() {\n document.querySelectorAll('pre code').forEach(function(codeBlock) {\n if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;\n codeBlock.parentElement.setAttribute('data-copy-added', 'true');\n \n var btn = document.createElement('button');\n btn.textContent = 'Copy';\n btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';\n btn.onmouseover = function() { this.style.opacity = '1'; };\n btn.onmouseout = function() { this.style.opacity = '0.7'; };\n btn.onclick = function() {\n navigator.clipboard.writeText(codeBlock.textContent).then(function() {\n btn.textContent = 'Copied!';\n setTimeout(function() { btn.textContent = 'Copy'; }, 1500);\n });\n };\n codeBlock.parentElement.style.position = 'relative';\n codeBlock.parentElement.appendChild(btn);\n });\n }\n \n addCopyButtons();\n \n // Re-run on dynamic content\n var observer = new MutationObserver(addCopyButtons);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Add Copy Buttons to Code Blocks");
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Force GitHub README to respect dark mode\n(function() {\n var style = document.createElement('style');\n style.textContent = '\n .markdown-body {\n color-scheme: dark light;\n }\n .markdown-body pre { background: #161b22 !important; }\n .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; }\n .markdown-body table th, .markdown-body table td { border-color: #30363d !important; }\n .markdown-body img { background: #0d1117; }\n .markdown-body blockquote { border-left-color: #8b949e; }\n .markdown-body hr { border-color: #30363d; }\n ';\n document.head.appendChild(style);\n})();", "GitHub Dark Mode README Fix");
}
} catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Highlight search terms from Google/DuckDuckGo/Bing referrer\n(function() {\n var ref = document.referrer;\n var terms = [];\n \n if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) {\n var url = new URL(ref);\n var q = url.searchParams.get('q') || url.searchParams.get('p');\n if (q) {\n terms = q.split(/\\s+/).filter(function(t) { return t.length > 2; });\n }\n }\n \n if (terms.length === 0) return;\n \n var style = document.createElement('style');\n style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }';\n document.head.appendChild(style);\n \n function highlight(node) {\n if (node.nodeType === 3) { // text node\n var text = node.textContent;\n var found = false;\n terms.forEach(function(term) {\n var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\\]\\\\]/g, '\\\\') + ')', 'gi');\n if (regex.test(text)) {\n found = true;\n var frag = document.createDocumentFragment();\n var parts = text.split(regex);\n parts.forEach(function(part, i) {\n if (i % 2 === 0) {\n frag.appendChild(document.createTextNode(part));\n } else {\n var span = document.createElement('span');\n span.className = 'userscript-highlight';\n span.textContent = part;\n frag.appendChild(span);\n }\n });\n node.parentNode.replaceChild(frag, node);\n }\n });\n } else if (node.nodeType === 1 && node.childNodes) { // element\n var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT'];\n if (!skipTags.includes(node.tagName)) {\n Array.from(node.childNodes).forEach(highlight);\n }\n }\n }\n \n highlight(document.body);\n \n // Re-highlight on dynamic content\n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1 || node.nodeType === 3) highlight(node);\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Highlight Search Terms");
}
} catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Strip utm_, fbclid, gclid, etc. from all links on page\n(function() {\n var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content',\n 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid',\n 'ref', 'ref_src', 'source', 'medium', 'campaign'];\n \n function cleanUrl(url) {\n try {\n var u = new URL(url, window.location.origin);\n var changed = false;\n trackingParams.forEach(function(p) {\n if (u.searchParams.has(p)) {\n u.searchParams.delete(p);\n changed = true;\n }\n });\n return changed ? u.toString() : url;\n } catch (e) {\n return url;\n }\n }\n \n function cleanLinks() {\n document.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n \n cleanLinks();\n \n var observer = new MutationObserver(function(mutations) {\n mutations.forEach(function(m) {\n m.addedNodes.forEach(function(node) {\n if (node.nodeType === 1) {\n if (node.tagName === 'A') cleanLinks();\n node.querySelectorAll('a[href]').forEach(function(a) {\n var clean = cleanUrl(a.href);\n if (clean !== a.href) a.href = clean;\n });\n }\n });\n });\n });\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "Remove Tracking Parameters from Links");
}
} catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); }
})();
(function(){
try {
var __m = "youtube.com";
var __re = new RegExp('^' + "youtube\\.com" + '

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Auto-enable theater mode on YouTube\n(function() {\n function tryTheater() {\n var btn = document.querySelector('button[aria-label=\"Theater mode\"], ytd-player #player button[title=\"Theater mode\"]');\n if (btn && !btn.classList.contains('activated')) {\n btn.click();\n }\n }\n \n // Try immediately\n tryTheater();\n \n // Try after navigation (SPA)\n var lastUrl = location.href;\n setInterval(function() {\n if (location.href !== lastUrl) {\n lastUrl = location.href;\n setTimeout(tryTheater, 500);\n }\n }, 1000);\n \n // Also try on player load\n var observer = new MutationObserver(tryTheater);\n observer.observe(document.body, { childList: true, subtree: true });\n})();", "YouTube Theater Mode Default");
}
} catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Remove or un-stick sticky/fixed headers that block content\n(function() {\n function unstick() {\n document.querySelectorAll('header, nav, [role=\"banner\"], .header, .navbar, .sticky, .fixed-top, [style*=\"position: fixed\"], [style*=\"position:sticky\"]').forEach(function(el) {\n if (el.style.position === 'fixed' || el.style.position === 'sticky' || \n getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') {\n el.style.position = 'static';\n el.style.top = 'auto';\n el.style.zIndex = 'auto';\n }\n });\n }\n \n unstick();\n \n var observer = new MutationObserver(unstick);\n observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] });\n})();", "Kill Sticky Headers");
}
} catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); }
})();
(function(){
try {
var __m = "*";
var __re = new RegExp('^' + ".*" + '

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading

, 'i');
if (__m === '*' || __re.test(location.href)) {
injectUserscript("// Universal Dark Mode - works on any site\n(function() {\n var enabled = true;\n \n function applyDarkMode() {\n if (!enabled) return;\n \n // Create style element if it doesn't exist\n var style = document.getElementById('universal-dark-mode-style');\n if (!style) {\n style = document.createElement('style');\n style.id = 'universal-dark-mode-style';\n document.head.appendChild(style);\n }\n \n // Dark mode CSS - inverts colors but preserves images/video\n style.textContent = '\n /* Invert everything except media */\n html {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #1a1a2e !important;\n }\n \n /* Restore images, videos, iframes, canvas */\n img, video, iframe, canvas, svg, picture, [style*=\"background-image\"] {\n filter: invert(1) hue-rotate(180deg) !important;\n }\n \n /* Preserve specific elements that should not be inverted */\n .no-dark-mode, .no-dark-mode *,\n [data-theme=\"light\"], [data-theme=\"light\"],\n .ace_editor, .ace_editor *,\n .CodeMirror, .CodeMirror *,\n .monaco-editor, .monaco-editor *,\n .markdown-body pre, .markdown-body pre *,\n .highlight, .highlight *,\n pre code, pre code * {\n filter: none !important;\n }\n \n /* Fix common UI elements */\n .modal, .popup, .dropdown-menu, .tooltip, .popover {\n filter: invert(1) hue-rotate(180deg) !important;\n background: #2d2d44 !important;\n border-color: #444 !important;\n }\n \n /* Scrollbars */\n ::-webkit-scrollbar { background: #1a1a2e !important; }\n ::-webkit-scrollbar-thumb { background: #444 !important; }\n ::-webkit-scrollbar-thumb:hover { background: #555 !important; }\n \n /* Selection */\n ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; }\n ';\n }\n \n function removeDarkMode() {\n var style = document.getElementById('universal-dark-mode-style');\n if (style) style.remove();\n }\n \n // Toggle with Alt+Shift+D\n document.addEventListener('keydown', function(e) {\n if (e.altKey && e.shiftKey && e.key === 'D') {\n e.preventDefault();\n enabled = !enabled;\n if (enabled) {\n applyDarkMode();\n console.log('[Universal Dark Mode] Enabled');\n } else {\n removeDarkMode();\n console.log('[Universal Dark Mode] Disabled');\n }\n }\n });\n \n // Apply on load\n applyDarkMode();\n \n // Re-apply on dynamic content\n var observer = new MutationObserver(function(mutations) {\n if (enabled && !document.getElementById('universal-dark-mode-style')) {\n applyDarkMode();\n }\n });\n observer.observe(document.head, { childList: true });\n \n console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle');\n})();", "Universal Dark Mode");
}
} catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); }
})();
})();

Skip to content
Exclude dir#4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

 Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and
privacy statement. We’ll occasionally send you account related emails.

Already on GitHub?
Sign in
to your account

 Merged

samuelburnham
merged 10 commits into

from

Sep 2, 2026
 Merged


Exclude dir
#4
Show file tree
Hide file tree
 Changes from all commits
Commits

Show all changes


10 commits


Select commit
Hold shift + click to select a range
265fcda

feat: Exclude a directory from a package directory glob


samuelburnham Aug 27, 2026
8075eb8

Update flake.lock


samuelburnham Aug 27, 2026
448b22a

ci: Restrict the E2E workflow to a read-only token


samuelburnham Aug 28, 2026
5951955

ci: Restrict the CI and test workflows to a read-only token


samuelburnham Aug 28, 2026
aece5d9

ci: Open the self-update PR with GITHUB_TOKEN


samuelburnham Aug 28, 2026
ac315a0

docs: Record what the default token cannot do


samuelburnham Sep 1, 2026
50d4c61

fix: Reject a bare `!` package directory exclusion


samuelburnham Sep 1, 2026
fe7af4b

ci: Silence the failure outcome in the test workflow


samuelburnham Sep 1, 2026
b0ed23f

fix: Get the Mathlib cache for every target package


samuelburnham Sep 1, 2026
728a375

feat: Fail validation when a required Mathlib cache is missing


samuelburnham Sep 1, 2026

File filter

Filter by extension
Filter by extension
Conversations

Failed to load comments. 
Loading
Jump to

Jump to file


Failed to load files. 
Loading
 Diff view

 Diff view


40 changes: 40 additions & 0 deletions
.github/workflows/e2e_test.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job updates fixtures inside the runner's own checkout and never writes back. The
# action's `gh` calls only read the public list of Lean releases.
permissions:
 contents: read

jobs:
 success_e2e_test:
 runs-on: ubuntu-latest
Expand DownExpand Up@@ -331,3 +336,38 @@ jobs:
 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1

 # An exclusion carves a package back out of the set the action would otherwise
 # update, leaving its lean-toolchain untouched.
 excluded_directory_e2e_test:
 runs-on: ubuntu-latest
 steps:
 - name: Checkout code
 uses: actions/checkout@v6

 - name: Bump two packages, excluding one of them
 id: update
 uses: ./
 with:
 bump_mode: "pinned-tags"
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/PinnedTags ./Fixtures/SmokeSuccess !./Fixtures/SmokeSuccess"

 - name: The excluded package must be left alone
 run: |
 a=$(cut -d: -f2 Fixtures/PinnedTags/lean-toolchain)
 b=$(cut -d: -f2 Fixtures/SmokeSuccess/lean-toolchain)
 echo "PinnedTags=$a SmokeSuccess=$b"
 if [ "$a" = "v4.31.0" ]; then
 echo "Error: the included package was not bumped"
 exit 1
 fi
 if [ "$b" != "v4.16.0" ]; then
 echo "Error: the excluded package was bumped to $b"
 exit 1
 fi

 - name: This update should succeed
 if: steps.update.outputs.result != 'update-success'
 run: exit 1
Comment thread
github-advanced-security[bot] marked this conversation as resolved.


Fixed


5 changes: 5 additions & 0 deletions
.github/workflows/lean_action_ci.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# The jobs only build and test fixtures inside the runner's own checkout; the `gh` calls
# made by lean-action read the public Mathlib cache and the public list of Lean releases.
permissions:
 contents: read

jobs:
 build:
 runs-on: ubuntu-latest
Expand Down

10 changes: 10 additions & 0 deletions
.github/workflows/test.yaml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,11 @@ on:
 - dev
 workflow_dispatch:

# Every job asserts on the action's outputs inside the runner's own checkout and never
# writes back, so a read-only token is all they need.
permissions:
 contents: read

jobs:
 has_dependency_output_test_true:
 runs-on: ubuntu-latest
Expand All@@ -28,6 +33,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: The result should be success
Expand All@@ -44,6 +50,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 - name: The result should be no dependency
 if: steps.update.outputs.has_dependency != 'false'
Expand All@@ -60,6 +67,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"

 - name: output assertion of latest_lean
Expand DownExpand Up@@ -92,6 +100,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/HasDep"

 - name: output assertion of latest_lean
Expand All@@ -118,6 +127,7 @@ jobs:
 uses: ./
 with:
 on_update_succeeds: "silent"
 on_update_fails: "silent"
 lake_package_directory: "./Fixtures/SmokeSuccess"
 update_lean_toolchain: "never"

Expand Down

18 changes: 7 additions & 11 deletions
.github/workflows/update.yml

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -5,24 +5,20 @@ on:
 - cron: '0 0 * * *' # every day at midnight
 workflow_dispatch:

# Opening the pull request needs write access to contents and pull requests, and the
# default `on_update_fails: issue` needs to open an issue when the bump does not build.
permissions:
 contents: write
 pull-requests: write
 issues: write

jobs:
 update:
 runs-on: ubuntu-latest
 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 }}

87 changes: 81 additions & 6 deletions
LeanUpdate/Input.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -104,21 +104,65 @@ partial def lakePackagesUnder (root : FilePath) : IO (Array FilePath) := do
 found := found ++ (← lakePackagesUnder child.path)
 return found

/-- Split a directory-list action input into its entries.

Separators are commas and ASCII whitespace, so `a, b`, `a b`, and a YAML block scalar holding one
path per line all parse alike. -/
def splitPackageDirEntries (raw : String) : List String :=
 raw.split (fun c => c == ',' || c.isWhitespace)
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 |>.toList

#guard
 splitPackageDirEntries " Benchmarks/**,\n !Fixtures/Slow " == ["Benchmarks/**", "!Fixtures/Slow"]

/-- The significant components of `path`, dropping empty and `.` segments. -/
def pathComponents (path : FilePath) : List String :=
 path.components.filter (fun s => !s.isEmpty && s != ".")

/-- whether `dir` is `parent` itself or lies somewhere beneath it

Comparing whole components rather than string prefixes keeps `Benchmarks/Slow`, `Benchmarks/Slow/`
and `./Benchmarks/Slow` the same directory, while refusing to read `Benchmarks/SlowFixture` as
living under `Benchmarks/Slow`. -/
def isAtOrUnder (parent dir : FilePath) : Bool :=
 (pathComponents parent).isPrefixOf (pathComponents dir)

#guard isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/Slow"
#guard isAtOrUnder "/w/Benchmarks/Slow/" "/w/Benchmarks/Slow/Nested"
#guard isAtOrUnder "./Benchmarks/Slow" "Benchmarks/Slow"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks/SlowFixture"
#guard !isAtOrUnder "/w/Benchmarks/Slow" "/w/Benchmarks"

/-- 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 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`. -/
path from its parent). Both forms sort by path and skip dotted directories such as `.lake`.

An entry prefixed with `!` subtracts instead of adding: it names a directory and drops that
directory together with everything beneath it, which is what lets a broad `/**` cover a tree that
holds a package the update must leave alone. An exclusion carries no glob of its own, since it
already reaches the whole subtree. -/
public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 let packageDir ← GitHub.Action.Input.get LakePackageDirectory
 let workspace? := (← IO.getEnv "GITHUB_WORKSPACE").map FilePath.mk
 let raw := packageDir.val.toString
 let entries := raw.split (fun c => c == ',' || c == ' ' || c == '\n')
 |>.map (fun s => s.trimAscii.copy)
 |>.filter (fun s => !s.isEmpty)
 let (exclusions, entries) := (splitPackageDirEntries raw).partition (·.startsWith "!")
 let exclusions := exclusions.map (fun entry => (entry.drop 1).copy)
 for entry in exclusions do
 if entry.isEmpty then
 throw <| IO.userError <|
 "A bare '!' names no directory to exclude. Write the path immediately after it, " ++
 "as in '!benchmarks/pinned'."
 if entry.any (· == '*') then
 throw <| IO.userError <|
 s!"Exclusion '!{entry}' contains a glob. An exclusion names a directory and already " ++
 "covers everything beneath it."
 let mut dirs : Array FilePath := #[]
 for entry in entries do
 if entry.endsWith "/**" then
Expand All@@ -136,9 +180,40 @@ public def getTargetLakePackageDirectories : IO (Array FilePath) := do
 dirs := dirs ++ found.qsort (fun a b => a.toString < b.toString)
 else
 dirs := dirs.push (resolveLakePackageDir workspace? (FilePath.mk entry))
 if dirs.isEmpty then
 let excludedDirs := exclusions.map (fun entry =>
 resolveLakePackageDir workspace? (FilePath.mk entry))
 -- An exclusion matching nothing is far more likely a typo than a deliberate no-op, and the
 -- cost of the typo is that a package meant to be protected is updated instead.
 for (entry, excludedDir) in exclusions.zip excludedDirs do
 unless dirs.any (isAtOrUnder excludedDir ·) do
 IO.println <| log%
 s!"warning: exclusion '!{entry}' matched none of the target Lake package directories"
 let kept := dirs.filter (fun dir => !excludedDirs.any (isAtOrUnder · dir))
 if kept.isEmpty then
 throw <| IO.userError s!"No Lake package directories found for input '{raw}'"
 return dirs
 return kept

/-- What to do when a target package's Mathlib cache cannot be fetched.

Defaults to `require`: building Mathlib from source takes hours and usually ends in a timeout,
so a run that silently falls back to it costs far more than the one that stops. -/
public inductive MathlibCache where
 /-- fail validation when `lake exe cache get` fails -/
 | require
 /-- report the failure and build without the cache -/
 | optional
deriving Repr, BEq, ToString, HasParser

public instance : Input MathlibCache where
 envName := "MATHLIB_CACHE"
 parse := parseAs MathlibCache
 localValue? := some .require

#guard
 let lst : List MathlibCache := [.require, .optional]
 lst.map toString == ["require", "optional"]

#guard (parseAs MathlibCache "optional").toOption == some .optional

/-- The input whether to update the `lean-toolchain` file. -/
public inductive UpdateLeanToolchain where
Expand Down

33 changes: 33 additions & 0 deletions
LeanUpdate/PostUpdateValidation.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -91,9 +91,42 @@ public def PostUpdateValidationResult.isSuccess (result : PostUpdateValidationRe
public def PostUpdateValidationResult.isFailure (result : PostUpdateValidationResult) : Bool :=
 !result.isSuccess

/-- Whether the package rooted at `cwd` depends on Mathlib. -/
def dependsOnMathlib (cwd : FilePath) : IO Bool := do
 let manifest := cwd / "lake-manifest.json"
 if !(← manifest.pathExists) then
 return false
 return (← IO.FS.readFile manifest).contains "leanprover-community/mathlib4"

/-- Get Mathlib's prebuilt artifacts for the package rooted at `cwd`, if it needs them.

Every Lake package root carries its own `.lake/packages/mathlib`, so the cache is unpacked once
per package; the downloads behind it are pooled in a single per-user directory, so only the first
package pays for the network. Whether a failure stops the run is `MathlibCache`'s to decide.
-/
def getMathlibCache (cwd : FilePath) : IO (Except String Unit) := do
 unless ← dependsOnMathlib cwd do
 return .ok ()
 IO.println <| log% s!"Getting the Mathlib cache for {cwd}"
 let out ← IO.Process.lakeOutput cwd (args := #["exe", "cache", "get"])
 if out.exitCode == 0 then
 return .ok ()
 let details := out.stdout.trimAscii.copy ++ "\n" ++ out.stderr.trimAscii.copy
 match ← GitHub.Action.Input.get MathlibCache with
 | .optional =>
 IO.println <| log%
 s!"warning: `lake exe cache get` exited with {out.exitCode}; building without the cache"
 return .ok ()
 | .require =>
 return .error s!"`lake exe cache get` exited with {out.exitCode}\n{details}"

/-- Run `lake build`, and `lake test`/`lake lint` when drivers exist, in one directory. -/
def validatePackage (buildArgs : BuildArgs) (targetLakePackageDir : FilePath) :
 IO PostUpdateValidationResult := do
 match ← getMathlibCache targetLakePackageDir with
 | .error e =>
 return { buildResult := .error e, testResult? := none, lintResult? := none }
 | .ok _ => pure ()
 let buildResult ← runLakeBuild targetLakePackageDir buildArgs

 let hasTestDriverResult ← hasTestDriver targetLakePackageDir
Expand Down

12 changes: 9 additions & 3 deletions
README.md

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -20,7 +20,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -49,7 +51,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand DownExpand Up@@ -81,7 +85,9 @@ on:

jobs:
 update_lean:
 # this is needed for private repositories
 # The default GITHUB_TOKEN is read-only, so the write scopes have to be asked for.
 # Opening the pull request also needs `Allow GitHub Actions to create and approve pull
 # requests` under Settings > Actions > General > Workflow permissions.
 permissions:
 contents: write
 pull-requests: write
Expand Down

2 changes: 2 additions & 0 deletions
Test/Main.lean

View file


Open in desktop

Original file line numberDiff line numberDiff line change
Expand Up@@ -16,6 +16,8 @@ public def main (args : List String) : IO Unit := do
 | ["toolchain-resolution-inner"] => LeanUpdateTest.LakeToolchainResolution.testInner
 | ["package-glob-recursive"] => LeanUpdateTest.PackageDirectoryGlob.runRecursive
 | ["package-glob-shallow"] => LeanUpdateTest.PackageDirectoryGlob.runShallow
 | ["package-glob-exclude-subtree"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeSubtree
 | ["package-glob-exclude-nested"] => LeanUpdateTest.PackageDirectoryGlob.runExcludeNested
 | _ => do
 LeanUpdateTest.PinnedTagFallback.test
 LeanUpdateTest.PackageDirectoryGlob.test
Expand Down
Loading
Loading