[dependabot]

Bumps the actions group with 1 update: leanprover/lean-action.

Updates leanprover/lean-action from 1.6.2 to 1.7.0

Release notes

Sourced from leanprover/lean-action's releases.

v1.7.0

Changed

• set MATHLIB_CACHE_GET_URL to https://cache.mathlib.org/mathlib4 for lake exe cache get, so Mathlib cache clients that read this variable download from cache.mathlib.org. A value that the workflow sets takes precedence. An empty value unsets the variable, so the cache client uses its own default endpoint

Fixed

• pass --no-modify-path to elan-init so installing elan no longer edits the runner's persistent environment (HKCU\Environment\PATH on Windows, ~/.profile and friends elsewhere). lean-action already puts $HOME/.elan/bin on $GITHUB_PATH, so this is a no-op on GitHub-hosted runners; on self-hosted runners it stops every job from accumulating PATH entries that outlive it

Changelog

Sourced from leanprover/lean-action's changelog.

v1.7.0 - 2026-10-27

Changed

• set MATHLIB_CACHE_GET_URL to https://cache.mathlib.org/mathlib4 for lake exe cache get, so Mathlib cache clients that read this variable download from cache.mathlib.org. A value that the workflow sets takes precedence. An empty value unsets the variable, so the cache client uses its own default endpoint

Fixed

• pass --no-modify-path to elan-init so installing elan no longer edits the runner's persistent environment (HKCU\Environment\PATH on Windows, ~/.profile and friends elsewhere). lean-action already puts $HOME/.elan/bin on $GITHUB_PATH, so this is a no-op on GitHub-hosted runners; on self-hosted runners it stops every job from accumulating PATH entries that outlive it

Commits

• fe40864 feat: set MATHLIB_CACHE_GET_URL to cache.mathlib.org (#202)
• a2cd0b8 fix: do not let elan-init modify the runner's persistent PATH (#189)
• 28dca45 chore: add missing CHANGELOG entries for #153 and #181 (#184)
• f8f95d2 chore: finalize v1.6.2 release (#201)
• See full diff in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore <dependency name> major version will close this group update PR and stop Dependabot creating any more for the specific dependency's major version (unless you unignore this specific dependency's major version or upgrade to it yourself)
• @dependabot ignore <dependency name> minor version will close this group update PR and stop Dependabot creating any more for the specific dependency's minor version (unless you unignore this specific dependency's minor version or upgrade to it yourself)
• @dependabot ignore <dependency name> will close this group update PR and stop Dependabot creating any more for the specific dependency (unless you unignore this specific dependency or upgrade to it yourself)
• @dependabot unignore <dependency name> will remove all of the ignore conditions of the specified dependency
• @dependabot unignore <dependency name> <ignore condition> will remove the ignore condition of the specified dependency and ignore conditions

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 59bf4e8e-b03e-4531-aa39-2761eec2a8ed

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• Trigger review

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn