v0.13.0

What's Changed

Fixed

• Fixed lake update using the action’s Lean/Lake toolchain instead of the target project’s toolchain. lean-update now invokes Lake through the Elan proxy, ensuring the target project’s lean-toolchain is respected. Fixes #257.

Others

• Updated the Lean toolchain of this repository from v4.32.0-rc1 to v4.33.0-rc2.

Full Changelog: v0.12.0...v0.13.0

v0.12.0

What's Changed

Added

• Added first-party post-update validation. After an update, lean-update now runs lake build, lake test when a test driver is present, and lake lint when a lint driver is present.
• Added separate lint failure reporting in generated issues via a Lint Output section.

Fixed

• Generated failure issues now separate Build Output, Test Output, and Lint Output, and include only the phases that failed. This makes it clear whether lake build, lake test, or lake lint caused the update failure. Fixes #218.
• The latest_lean output is now set according to release_kind_to_fetch even when lean-toolchain is not changed.
• Projects with dependencies no longer have lean-toolchain overwritten while still exposing the latest Lean version through latest_lean.
• Disabled GitHub cache usage in the Lean preparation step to avoid failures caused by a broken GitHub cache.

Changed

• Post-update checks are now described and reported as validation rather than as a single lean-action build step.
• build_args now explicitly applies to the lake build phase of post-update validation.

Full Changelog: v0.11.0...v0.12.0

v0.11.0

What's Changed

• Fixed lake update failures when the target package switches to a newer Lean toolchain. lean-update now clears inherited Lean/Lake toolchain environment variables before running lake update, so Lake uses the target package's toolchain consistently. Fixes #237.
• Fixed the same Lean/Lake environment isolation for lake build, preventing stale action-local environment variables from leaking into the build subprocess.

Full Changelog: v0.10.0...v0.11.0

v0.10.0

This release improves issue creation for Lean update workflows by moving the remaining shell-based logic into the Lean implementation.

What's Changed

• Fixed issue creation so it respects the configured build_args input when capturing build output.
• Fixed issue body formatting when build output contains nested code fences.

Full Changelog: v0.9.0...v0.10.0

v0.9.0

v0.9.0

This release is mainly an internal reliability update for the GitHub Action. The action now runs its main update workflow through the Lean-based leanUpdate executable, replacing the previous mix of shell and Node.js logic for several steps.

What's Changed

• Added Lean commands for dependency detection, lean-toolchain updates, dependency updates, and change detection.
• Replaced the old scripts/checkChanges.js implementation with a Lean implementation based on git diff -w.
• Added a dedicated dependency update command that validates legacy_update and runs either lake update or lake -R -Kenv=dev update.
• Improved lean-toolchain handling for projects without dependencies, including clearer support for tagged and nightly Lean releases.
• Switched internal cross-step state to GITHUB_ENV while preserving public action outputs.
• Improved PR text for lean-toolchain updates by showing the full new file content.
• Tightened parsing and validation for action inputs such as update_lean_toolchain, release_kind_to_fetch, legacy_update, and update_if_modified.
• Reorganized the Lean source tree under LeanUpdate and introduced shared helpers for input parsing, GitHub Actions output/environment handling, and wrapper types.

Bug Fixes

• Fixed empty lean-toolchain content being shown in update messages.
• Fixed internal state handling by avoiding GITHUB_OUTPUT for values consumed by later action steps.
• Fixed command argument matching in the leanUpdate entry point.

Migration Notes

No workflow changes are required for existing users.

Invalid values for validated inputs now fail earlier with clearer errors. In particular, legacy_update should be true or false, and update_lean_toolchain should be auto or never.

Full Changelog: v0.8.0...v0.9.0

v0.8.0

What's Changed

New Features

• Added support for selecting which Lean release stream to fetch via the new release_kind_to_fetch input.
  • tagged fetches the latest tagged Lean release, including pre-releases.
  • nightly fetches the latest nightly Lean release.
• Added a new has_dependency output, indicating whether the target Lake package has dependencies.
• Improved the latest_lean output so workflows can inspect the Lean version fetched by the action when updating dependency-free projects.

Improvements

• Updated bundled GitHub Action dependencies:
  • peter-evans/create-pull-request to v8
  • EndBug/add-and-commit to v10
  • README examples now use actions/checkout@v6

Bug Fixes

• Fixed latest Lean release selection logic.
• Fixed oversized GitHub issue bodies by truncating variable sections while preserving the Markdown structure and build output block.

Behavior Notes

• latest_lean is now only set when update_lean_toolchain is auto and the target Lake package has no dependencies.
• release_kind_to_fetch only affects Lean toolchain updates; it does not affect Lake dependency updates.

Full Changelog: v0.7.0...v0.8.0

v0.7.0

What's Changed

• rename postMerge.ps1 to .bash by @Seasawher in #147
• Remove develop by @Seasawher in #151
• remove bash file by @Seasawher in #155
• fix the method of checking for dependencies by @Seasawher in #158
• use actions/checkout@v5 instead of v4 by @Seasawher in #164
• change the way to test by @Seasawher in #169
• remove PR template by @Seasawher in #170
• organize the inputs of action by @Seasawher in #171
• remove redundant doc by @Seasawher in #172
• remove .vscode and AGENTS.md by @Seasawher in #173
• notification test CI by @Seasawher in #174

Full Changelog: v0.6.0...v0.7.0

v0.6.0

What's Changed

• TEST: submitting PR fails if the target repository is private #134 by @Seasawher in #135
• Add update_lean_toolchain input to control whether lean-toolchain is updated to latest stable on projects with no dependencies by @TwoFX in #142

New Contributors

• @TwoFX made their first contribution in #142

Full Changelog: v0.5.0...v0.6.0

v0.5.0

What's Changed

• pretty print of build output by @Seasawher in #122
• possible bug: if new toolchain exists but mathlib uses old toolchain...? by @Seasawher in #130

Full Changelog: v0.4.0...v0.5.0

v0.4.0

What's Changed

• change owner by @Seasawher in #106
• Fix Development problem by @Seasawher in #110
• new toolchain in title/body of PR/issue by @Seasawher in #114

Full Changelog: v0.3.0...v0.4.0