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

Create auto-config input #60

Closed
austinletson opened this issue Jun 11, 2024 · 1 comment · Fixed by #61
Closed

Create auto-config input #60

austinletson opened this issue Jun 11, 2024 · 1 comment · Fixed by #61
Assignees
@austinletson
Labels
enhancement New feature or request v1-release Issue to complete for v1 release

Comments

@austinletson
Copy link
Collaborator

Create auto-config input to allow users to specify if lean-action should use the Lake workspace (or grep in some cases) to determine a configuration for lean-action.

Related: #30, #46, #53

This feature still needs to be fleshed out.
@austinletson austinletson self-assigned this Jun 11, 2024
@austinletson austinletson mentioned this issue Jun 11, 2024
Closed
@austinletson austinletson linked a pull request Jun 14, 2024 that will close this issue
feat: add auto-config and build inputs. #61
Merged
@austinletson
Copy link
Collaborator Author

austinletson commented Jun 14, 2024 •
edited
Loading

I created #61 as a first draft of the auto-config input. I am open to any feedback on the semantics of the new auto-config and build inputs or the changes to the test input.

@austinletson austinletson mentioned this issue Jun 14, 2024
Merged
@austinletson austinletson added enhancement New feature or request v1-release Issue to complete for v1 release labels Jun 18, 2024
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.
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 auto-config and build inputs. leanprover/lean-action
1 participant
@austinletson