Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

docs: release notes for v1-beta #39

Merged
merged 1 commit into from
May 21, 2024
+13 −7
Merged

docs: release notes for v1-beta #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,20 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0

## Unreleased

## v1-beta - 2024-05-21

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

### Changed
- `lean-action` no longer contains an `actions/checkout` step
- `mathlib-cache` renamed to `get-mathlib-cache`

### Fixed
- improved default value for `get-mathlib-cache`

## v1-alpha - 2024-05-12

### Added
Expand Down
12 changes: 6 additions & 6 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,13 +23,13 @@ jobs:
steps:
- uses: actions/checkout@v4
# uses lean standard action with all default input values
- uses: leanprover/lean-action@v1-alpha
- uses: leanprover/lean-action@v1-beta
```

## Usage

```yaml
- uses: leanprover/lean-action@v1-alpha
- uses: leanprover/lean-action@v1-beta
with:
# Run lake test.
# Allowed values: "true" or "false".
Expand Down Expand Up @@ -70,7 +70,7 @@ jobs:
### Lint the `MyModule` module and check package for reservoir eligibility

```yaml
- uses: leanprover/lean-action@v1-alpha
- uses: leanprover/lean-action@v1-beta
with:
lint-module: MyModule
check-reservoir-eligibility: true
Expand All @@ -79,7 +79,7 @@ jobs:
### Don't run `lake test` or use Mathlib cache

```yaml
- uses: leanprover/lean-action@v1-alpha
- uses: leanprover/lean-action@v1-beta
with:
test: false
use-mathlib-cache: false
Expand All @@ -88,7 +88,7 @@ jobs:
### Run lake build with `--wfail`

```yaml
- uses: leanprover/lean-action@v1-alpha
- uses: leanprover/lean-action@v1-beta
with:
build-args: "--wfail"
```
Expand All @@ -101,7 +101,7 @@ For example, `leanprover-community/import-graph` uses the setup from `lean-actio

```yaml
steps:
- uses: leanprover/lean-action@v1-alpha
- uses: leanprover/lean-action@v1-beta
with:
check-reservoir-eligibility: true
# use setup from lean-action to perform the following steps
Expand Down