Bump leanprover/lean-action from 1.5.0 to 1.6.0

[dependabot]

Bumps leanprover/lean-action from 1.5.0 to 1.6.0.

Release notes

Sourced from leanprover/lean-action's releases.

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

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)

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

v1.5.0 - 2026-04-21

Added

• new nanoda input to check environment with nanoda external type checker
• new nanoda-allow-sorry input to permit sorryAx axiom when running nanoda (default: true)
• new nanoda-status output parameter
• new reusable workflow nanoda-daily.yml for scheduled daily verification with notifications

Changed

• rename the lean4checker input to leanchecker, while keeping lean4checker as a deprecated alias
• use the bundled leanchecker binary on Lean nightly-2026-01-09 / v4.28.0-rc1 and newer, with fallback to the external lean4checker repository on older toolchains

Fixed

• fixed bug where callling .test.sh instead of lake test on lean4checker on Lean v4.27.x would cause a failure

v1.4.0 - 2026-01-15

Added

... (truncated)

Commits

• 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...
• 236e615 feat: add lint-args configuration input (#149)
• 62e5cb3 chore(deps): bump actions/checkout from 4 to 7 (#174)
• fd79d79 chore(deps): bump peter-evans/create-pull-request from 7 to 8 (#172)
• 44bde84 fix: include lake-package-directory in cache key hashes (#167)
• 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)