[dependabot]

Bumps leanprover/lean-action from 1.6.0 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

v1.6.2

Fixed

• save the GitHub cache after testing and linting so their build artifacts can be reused, preserving caching after test or lint failures and skipping saves on an exact cache hit

v1.6.1

Changed

• pin the actions/cache steps, and all actions used by this repository's workflows, to full commit SHAs, so that lean-action works in organizations that require SHA-pinned actions

Changelog

Sourced from leanprover/lean-action's changelog.

Changelog

All notable changes to lean-action will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

Unreleased

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

v1.6.2 - 2026-10-12

Fixed

• save the GitHub cache after testing and linting so their build artifacts can be reused, preserving caching after test or lint failures and skipping saves on an exact cache hit

v1.6.1 - 2026-10-02

Changed

• pin the actions/cache steps, and all actions used by this repository's workflows, to full commit SHAs, so that lean-action works in organizations that require SHA-pinned actions

v1.6.0 - 2026-08-22

Added

• new leanchecker-args input to pass arguments to lake env leanchecker, e.g. leanchecker-args: "-v" for verbose output or explicit module prefixes such as leanchecker-args: "MyPkg.Core" to narrow the set of modules checked
• new axiom-audit input to audit the project's axioms with axiom-audit: fail if any declaration depends on an axiom outside the allowlist (catches sorry, native_decide, and home-rolled axioms). Default: false
• new axiom-audit-allow input for the allowlist (default: propext,Classical.choice,Quot.sound)
• new axiom-audit-root input to set the audited root namespace (default: the lakefile's library name)
• new axiom-audit-status output parameter
• new lint-args input to specify arguments to pass to lake lint

... (truncated)

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)
• 24581d7 fix: cache test and lint build artifacts (#197)
• a1e4f67 chore: finalize v1.6.1 release (#198)
• f061402 chore: pin actions to commit SHAs (#193)
• 96e0613 chore: finalize v1.6.0 release (#188)
• 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 this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)