austinletson/Lean Action - CI for Lean Projects
Standard CI for Lean projects. Steps: - install elan - get Mathlib cache (optional, must be downstream of Mathlib) - lake build - lake test (optional) - lake exe runLinter (optional, must be downstream of Std) - check reservoir eligibility (optional)
View on GitHubTrust Signals
- Scorecard Score
- not yet scored
- Maintenance Recency
- Stale
- License
- None
Inputs
| name | description | required | default |
|---|---|---|---|
| test | Run lake test. Allowed values: "true" or "false". If test input is not provided, tests will run by default. | no | true |
| mathlib-cache | Run "lake exe cache get" before build. Project must be downstream of Mathlib. Allowed values: "true" or "false". If mathlib-cache input is not provided, the action will attempt to automatically detect if the project is downstream of Mathlib. | no | "" |
| lint-module | Run "lake exe runLinter" on the specified module. Project must be downstream of Std. Allowed values: name of module to lint. If lint-module input is not provided, linter will not run. | no | "" |
| check-reservoir-eligibility | Check if the repository is eligible for the reservoir. Allowed values: "true" or "false". If check-reservoir-elibility input is not provided, the action will not check for reservoir eligibility. | no | false |
Outputs
no outputs