Skip to content

Bump leanprover/lean-action from 1.4.0 to 1.5.0#134

Merged
mo271 merged 1 commit into
mainfrom
dependabot/github_actions/leanprover/lean-action-1.5.0
May 1, 2026
Merged

Bump leanprover/lean-action from 1.4.0 to 1.5.0#134
mo271 merged 1 commit into
mainfrom
dependabot/github_actions/leanprover/lean-action-1.5.0

Conversation

@dependabot
Copy link
Copy Markdown
Contributor

@dependabot dependabot Bot commented on behalf of github May 1, 2026

Bumps leanprover/lean-action from 1.4.0 to 1.5.0.

Release notes

Sourced from leanprover/lean-action's releases.

v1.5.0

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
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.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

  • new test-args input to specify arguments to pass to lake test
  • fixed bug where elan installation failed but lean-action continued (#143)

v1.3.0 - 2025-07-24

Added

  • Add a step to check all files in the default target's directory are imported in the main file by running lake exe mk_all --check. -
  • Add mk_all-check input to enable the mk_all step and mk_all-status to use the result.

v1.2.0 - 2025-05-16

Added

  • add option to always reinstall lean4-pr-releases toolchains, ensuring CI runs with the latest version

v1.1.2 - 2025-03-28

Fixed

... (truncated)

Commits
  • 38fbc41 fix: use lake test if test.sh is missing from lean4checker (#160)
  • 1831970 feat: add nanoda external type checker support (#145)
  • 5df9cab fix: update actions/cache to v5 to resolve Node.js 20 deprecation warning (#155)
  • 897fc7a chore: fix typo (#158)
  • 844b330 rename lean4checker input to leanchecker (#156)
  • 65f454b test: add functional test for lean4checker in subdirectory (#138)
  • 776a112 doc: update CHANGELOG.md for v1.4.0 (#148)
  • See full diff in compare view

Dependabot compatibility score

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)

Bumps [leanprover/lean-action](https://github.com/leanprover/lean-action) from 1.4.0 to 1.5.0.
- [Release notes](https://github.com/leanprover/lean-action/releases)
- [Changelog](https://github.com/leanprover/lean-action/blob/main/CHANGELOG.md)
- [Commits](leanprover/lean-action@c544e89...38fbc41)

---
updated-dependencies:
- dependency-name: leanprover/lean-action
  dependency-version: 1.5.0
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
@dependabot dependabot Bot added dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code labels May 1, 2026
@mo271 mo271 merged commit 701731c into main May 1, 2026
2 checks passed
@dependabot dependabot Bot deleted the dependabot/github_actions/leanprover/lean-action-1.5.0 branch May 1, 2026 07:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant