Repository navigation
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-toolchainupdates, dependency updates, and change detection. - Replaced the old
scripts/checkChanges.jsimplementation with a Lean implementation based ongit diff -w. - Added a dedicated dependency update command that validates
legacy_updateand runs eitherlake updateorlake -R -Kenv=dev update. - Improved
lean-toolchainhandling for projects without dependencies, including clearer support for tagged and nightly Lean releases. - Switched internal cross-step state to
GITHUB_ENVwhile preserving public action outputs. - Improved PR text for
lean-toolchainupdates 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, andupdate_if_modified. - Reorganized the Lean source tree under
LeanUpdateand introduced shared helpers for input parsing, GitHub Actions output/environment handling, and wrapper types.
Bug Fixes
- Fixed empty
lean-toolchaincontent being shown in update messages. - Fixed internal state handling by avoiding
GITHUB_OUTPUTfor values consumed by later action steps. - Fixed command argument matching in the
leanUpdateentry 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