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

Jump to bottom

Update the lint step to use the more flexible lake lint #46

Closed
austinletson opened this issue May 27, 2024 · 0 comments · Fixed by #73
Closed

Update the lint step to use the more flexible lake lint #46

austinletson opened this issue May 27, 2024 · 0 comments · Fixed by #73
Assignees
@austinletson
Labels
enhancement New feature or request v1-release Issue to complete for v1 release

Comments

@austinletson
Copy link
Collaborator

leanprover/lean4#4261 adds support for a new lake lint command. We should refactor the lint step to use this more flexible linting command. We should still test that the batteries linting framework works when wrapped with lake lint.
@austinletson austinletson mentioned this issue Jun 4, 2024
Closed
@austinletson austinletson added the enhancement New feature or request label Jun 7, 2024
@austinletson austinletson mentioned this issue Jun 11, 2024
Closed
austinletson added a commit that referenced this issue Jun 14, 2024
@austinletson
feat: add auto-config and build inputs.
7698a08 
`auto-config` allows users to specify if `lean-action` should
use the Lake workspace to automatically decide which CI features to run.

`build` allows users to specify
if `lean-action` should run `lake build`.

By default, `auto-config: true`.

The `test` and `build` (and soon `lint`, see #46) inputs
allow users to override the automatically configured behavior
or configure `lean-action` when `auto-config: false`.

`auto-config: true` is close to the previous default behavior,
however there is a difference in the outcome of the `lake test` step.
When users set `test: true` manually,
`lean-action` must find tests with `lake check-test` and run `lake test`
or it will fail (this was the previous behavior).
However with `auto-config: true`,
if `lake check-test` fails, `lean-action` will not run `lake test`
and this won't cause `lean-action` to fail.
austinletson added a commit that referenced this issue Jun 14, 2024
@austinletson
feat: add auto-config and build inputs.
f983264 
`auto-config` allows users to specify if `lean-action` should
use the Lake workspace to automatically decide which CI features to run.

`build` allows users to specify if `lean-action` runs `lake build`.

By default, `auto-config: true`.

The `test` and `build` (and soon `lint`, see #46) inputs
allow users to override the automatically configured behavior
or configure `lean-action` when `auto-config: false`.

`auto-config: true` is close to the previous default behavior,
however there is a difference in the outcome of the `lake test` step.
When users set `test: true` manually, `lean-action` must find tests
with `lake check-test` and run `lake test` or it will fail
(this was the previous behavior). However with `auto-config: true`,
if `lake check-test` fails, `lean-action` will not run `lake test`
and this won't cause `lean-action` to fail.
@austinletson austinletson mentioned this issue Jun 14, 2024
Merged
@austinletson austinletson added the v1-release Issue to complete for v1 release label Jun 22, 2024
@austinletson austinletson self-assigned this Jul 7, 2024
austinletson added a commit that referenced this issue Jul 7, 2024
@austinletson
feat: add auto-config and build inputs.
ba4217e 
`auto-config` allows users to specify if `lean-action` should
use the Lake workspace to automatically decide which CI features to run.

`build` allows users to specify if `lean-action` runs `lake build`.

By default, `auto-config: true`.

The `test` and `build` (and soon `lint`, see #46) inputs
allow users to override the automatically configured behavior
or configure `lean-action` when `auto-config: false`.

`auto-config: true` is close to the previous default behavior,
however there is a difference in the outcome of the `lake test` step.
When users set `test: true` manually, `lean-action` must find tests
with `lake check-test` and run `lake test` or it will fail
(this was the previous behavior). However with `auto-config: true`,
if `lake check-test` fails, `lean-action` will not run `lake test`
and this won't cause `lean-action` to fail.
austinletson added a commit that referenced this issue Jul 7, 2024
@austinletson
feat: add auto-config and build inputs.
2ec10ab 
`auto-config` allows users to specify if `lean-action` should
use the Lake workspace to automatically decide which CI features to run.

`build` allows users to specify if `lean-action` runs `lake build`.

By default, `auto-config: true`.

The `test` and `build` (and soon `lint`, see #46) inputs
allow users to override the automatically configured behavior
or configure `lean-action` when `auto-config: false`.

`auto-config: true` is close to the previous default behavior,
however there is a difference in the outcome of the `lake test` step.
When users set `test: true` manually, `lean-action` must find tests
with `lake check-test` and run `lake test` or it will fail
(this was the previous behavior). However with `auto-config: true`,
if `lake check-test` fails, `lean-action` will not run `lake test`
and this won't cause `lean-action` to fail.
austinletson added a commit that referenced this issue Jul 11, 2024
@austinletson
feat: add auto-config and build inputs. (#61)
df9ad20 
`auto-config` allows users to specify if `lean-action` should use the
Lake workspace to automatically decide which CI features to run.

`build` allows users to specify if `lean-action` runs `lake build`.

By default, `auto-config: true`.

The `test` and `build` (and soon `lint`, see #46) inputs allow users to
override the automatically configured behavior or configure
`lean-action` when `auto-config: false`.

`auto-config: true` is close to the previous default behavior, however
there is a difference in the outcome of the `lake test` step. When users
set `test: true` manually, `lean-action` must find tests with `lake
check-test` and run `lake test` or it will fail (this was the previous
behavior). However with `auto-config: true`, if `lake check-test` fails,
`lean-action` will not run `lake test` and this won't cause
`lean-action` to fail.

Closes #60, #53, and #30.
austinletson added a commit that referenced this issue Jul 11, 2024
@austinletson
feat: add auto-config and build inputs.
d821ffb 
`auto-config` allows users to specify if `lean-action` should
use the Lake workspace to automatically decide which CI features to run.

`build` allows users to specify if `lean-action` runs `lake build`.

By default, `auto-config: true`.

The `test` and `build` (and soon `lint`, see #46) inputs
allow users to override the automatically configured behavior
or configure `lean-action` when `auto-config: false`.

`auto-config: true` is close to the previous default behavior,
however there is a difference in the outcome of the `lake test` step.
When users set `test: true` manually, `lean-action` must find tests
with `lake check-test` and run `lake test` or it will fail
(this was the previous behavior). However with `auto-config: true`,
if `lake check-test` fails, `lean-action` will not run `lake test`
and this won't cause `lean-action` to fail.

style: white space

doc: sync README.md with action.yml input description

doc: improve readme.md

feat: add `lint` input to control the `lake lint` step

The `lint` input functions similarly to the `test` input,
allowing the user to run `@[lint_driver]` targets with `lean-action`.
@austinletson austinletson mentioned this issue Jul 11, 2024
Merged
@austinletson austinletson linked a pull request Jul 11, 2024 that will close this issue
feat: add lint input to control the lake lint step #73
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@austinletson austinletson

Labels
enhancement New feature or request v1-release Issue to complete for v1 release
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

feat: add lint input to control the lake lint step leanprover/lean-action
1 participant
@austinletson