Skip to content

chore(deps): bump leanprover/lean-action from 1.4.0 to 1.5.0 in the dependencies group#33

Open
dependabot[bot] wants to merge 1 commit intomainfrom
dependabot/github_actions/dependencies-b1eb36a911
Open

chore(deps): bump leanprover/lean-action from 1.4.0 to 1.5.0 in the dependencies group#33
dependabot[bot] wants to merge 1 commit intomainfrom
dependabot/github_actions/dependencies-b1eb36a911

Conversation

@dependabot
Copy link
Copy Markdown

@dependabot dependabot Bot commented on behalf of github Apr 26, 2026

Bumps the dependencies group with 1 update: leanprover/lean-action.

Updates 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 <dependency name> major version will close this group update PR and stop Dependabot creating any more for the specific dependency's major version (unless you unignore this specific dependency's major version or upgrade to it yourself)
  • @dependabot ignore <dependency name> minor version will close this group update PR and stop Dependabot creating any more for the specific dependency's minor version (unless you unignore this specific dependency's minor version or upgrade to it yourself)
  • @dependabot ignore <dependency name> will close this group update PR and stop Dependabot creating any more for the specific dependency (unless you unignore this specific dependency or upgrade to it yourself)
  • @dependabot unignore <dependency name> will remove all of the ignore conditions of the specified dependency
  • @dependabot unignore <dependency name> <ignore condition> will remove the ignore condition of the specified dependency and ignore conditions

Bumps the dependencies group with 1 update: [leanprover/lean-action](https://github.com/leanprover/lean-action).


Updates `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
  dependency-group: dependencies
...

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 Apr 26, 2026
@dependabot dependabot Bot requested a review from tskovlund as a code owner April 26, 2026 19:03
@dependabot dependabot Bot added dependencies Pull requests that update a dependency file github_actions Pull requests that update GitHub Actions code labels Apr 26, 2026
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.

0 participants