Bump leanprover/lean-action from 96e06131c0e9943c780388fd166f55d1e2fa0433 to f061402b660e0c34644504b324e830f2991d4865

[dependabot]

Bumps leanprover/lean-action from 96e06131c0e9943c780388fd166f55d1e2fa0433 to f061402b660e0c34644504b324e830f2991d4865.

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

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)

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

... (truncated)

Commits

• f061402 chore: pin actions to commit SHAs (#193)
• 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)