[dependabot]

Bumps leanprover/lean-action from 1.5.0 to 1.6.2.

Release notes

Sourced from leanprover/lean-action's releases.

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

v1.6.0

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
• new mk_all-args input to pass arguments to lake exe mk_all --check, e.g. mk_all-args: "--lib Carleson" to restrict the check to a specific library
• new release.yml workflow which automates the release process (see RELEASING.md)

Fixed

• include lake-package-directory when hashing lean-toolchain and lake-manifest.json for the GitHub cache key, so projects whose Lake package lives in a subdirectory get a version-specific key instead of an empty one (the empty key previously caused stale, cross-version cache restores)
• use a more portable shebang, useful for self-hosted runners

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

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
• new mk_all-args input to pass arguments to lake exe mk_all --check, e.g. mk_all-args: "--lib Carleson" to restrict the check to a specific library
• new release.yml workflow which automates the release process (see RELEASING.md)

Changed

• document the LEAN_NUM_THREADS workaround for leanchecker memory exhaustion on projects with a Mathlib dependency

Fixed

... (truncated)

Commits

• 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)
• 50fcf42 feat: add mk_all-args input (#185)
• 6835ef4 feat: automate the release process with a release workflow (#183)
• 0e73be8 feat: add leanchecker-args input (#162)
• 18a0628 feat: add opt-in axiom-audit check (#166)
• 6871e54 fix: pass resolved toolchain to lake-lint-args functional test (#182)
• c7d824f docs: document LEAN_NUM_THREADS workaround for leanchecker memory exhaust...
• Additional commits viewable 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)