You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This commit was created on GitHub.com and signed with GitHub’s verified signature.
v1.0.0 - 2024-07-20
Added
new auto-config input to specify if lean-action should use the Lake workspace to automatically determine which CI features to run, i.e., lake build, lake test, lake lint.
new build input to specify if lean-action should run lake build.
new lint input to specify if lean-action should run lake lint.
parameterize functional tests by Lean toolchain to allow for testing lean-action on any Lean version.
Changed
test input now defaults to auto-config. Users can still specify test: true to force lean-action to run lake test.
removed lint-module input. Users should now use a @[lint_driver] to integrate with the Batteries testing framework.
Fixed
improved GitHub cache keys to make caching more efficient and avoid edge cases when upgrading Lean version.