chore(deps): bump leanprover/lean-action from 1.pre.beta to 1.0.0

[dependabot]

Bumps leanprover/lean-action from 1.pre.beta to 1.0.0.

Release notes

Sourced from leanprover/lean-action's releases.

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.

v1-beta.1 - 2024-06-21

Added

• new use-github-cache input to specify if lean-action should use actions/cache to cache the .lake folder
• build-status and test-status output parameters
• new lake-package-directory input to specify the directory to run Lake commands. This input will enable users to use lean-action when Lake packages are contained in repository subdirectories.

Changed

• upgrade elan version to v3.1.1
• run lake check-test before running lake test
• improved log readability with explicit log group naming and additional white space

Fixed

• remove misleading .toml error message in mathlib detection
• remove elan-init file after elan installation

Changelog

Sourced from leanprover/lean-action's changelog.

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.

v1-beta.1 - 2024-06-21

Added

• new use-github-cache input to specify if lean-action should use actions/cache to cache the .lake folder
• build-status and test-status output parameters
• new lake-package-directory input to specify the directory to run Lake commands. This input will enable users to use lean-action when Lake packages are contained in repository subdirectories.
• new auto-config input to configure lean-action to use the Lake workspace to decide which steps to run

Changed

• upgrade elan version to v3.1.1
• run lake check-test before running lake test
• improved log readability with explicit log group naming and additional white space

Fixed

• remove misleading .toml error message in mathlib detection
• remove elan-init file after elan installation

v1-beta.0 - 2024-05-21

Added

• logs are grouped by step for better readability
• new build-args input to specify arguments to pass to lake build
• install elan step logs lean --version and lake --version

... (truncated)

Commits

• b7cdeeb feat: add lint input to control the lake lint step (#73)
• a7937f1 doc: update RELEASE.md and create release issue template (#78)
• bdc86e7 fix: use input instead of hardcoded toolchain in auto-config tests (#77)
• b3427eb chore(deps): bump raven-actions/actionlint from 1 to 2 (#76)
• df9ad20 feat: add auto-config and build inputs. (#61)
• de3e024 chore: bump functional tests default Lean version to 4.9.0 (#72)
• 16fb934 fix: improve GitHub cache keys (#71)
• a1d3429 test: parameterize functional tests by Lean toolchain (#69)
• d0073fd doc: update CHANGELOG.md for v1.0.0-beta.1 release (#67)
• See full diff in compare view

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 merge will merge this PR after your CI passes on it
• @dependabot squash and merge will squash and merge this PR after your CI passes on it
• @dependabot cancel merge will cancel a previously requested merge and block automerging
• @dependabot reopen will reopen this PR if it is closed
• @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)