Repository navigation
v0.12.0
What's Changed
Added
- Added first-party post-update validation. After an update, lean-update now runs
lake build,lake testwhen a test driver is present, andlake lintwhen a lint driver is present. - Added separate lint failure reporting in generated issues via a
Lint Outputsection.
Fixed
- Generated failure issues now separate
Build Output,Test Output, andLint Output, and include only the phases that failed. This makes it clear whetherlake build,lake test, orlake lintcaused the update failure. Fixes #218. - The
latest_leanoutput is now set according torelease_kind_to_fetcheven whenlean-toolchainis not changed. - Projects with dependencies no longer have
lean-toolchainoverwritten while still exposing the latest Lean version throughlatest_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_argsnow explicitly applies to thelake buildphase of post-update validation.
Full Changelog: v0.11.0...v0.12.0