leanprover-community/Mathlib style linter
Text-based linters to ensure Lean code meets Mathlib style guidelines. This action will automatically make suggestions to PRs to fix style issues. Write "bot fix style" in a comment to have a bot apply all style suggestions. This action is intended to run in multiple workflows, with different `mode` settings. * on pushes to branches, run this action in mode `check` to run the linters. * on `pull_request`, run this action in mode `suggest` to run the linters and comment with suggestions. * on `issue_comment`, `pull_request_review` or `pull_request_review_comment` (with types `[created, edited`), run this action in mode `fix` to listen for "bot fix style" comments and apply the suggestions.
View on GitHubTrust Signals
- Scorecard Score
- not yet scored
- Maintenance Recency
- Activelast commit May 12, 2026
- License
- None
Pinned Snippet
uses: leanprover-community/lint-style-action@e6128ab22cb03b509075ae46c33727e3952ffab7 # no releases — HEAD as of 2026-07-11tags can be moved; commit SHAs can't. why a SHA?
Inputs
| name | description | required | default |
|---|---|---|---|
| mode | The actions taken based on style linter output. When set to `check`, this action runs the style linters. When set to `suggest`, this action adds review comments with suggestions. When set to `fix`, this action looks for a "bot fix style" comment and pushes a commit with the suggested fixes. Allowed values: "check", "suggest" or "fix". | yes | — |
| lint-bib-file | Enables linting of the bibiliography using `./scripts/lint-bib.sh`. | no | false |
| BOT_FIX_STYLE_TOKEN | Secret token used by the style bot to interact with GitHub. Only required for the `fix` mode. | no | — |
| ref | The branch, tag or SHA to lint. This defaults to the reference or SHA for the event that triggered the workflow. | no | "" |
Outputs
| name | description |
|---|---|
| user_permission | (In `fix` mode:) Did the user ask for "bot fix style" and have enough permission? Allowed values: "true" | "false" |