Style checks in my repo

Stream: general

[Iván Renison]

Hi, I want to have style checks like the ones in Mathlib in my own Lean repo (for example to check line length). I tried using leanprover-community/lint-style-action, but it says that it runs lake exe lint-style, and I don't get lake exe lint-style to give me any error no matter how bad I format my code (not even with very long lines)
Do you know what I have to do so that lake exe lint-style gives me errors of code style?

[Malvin Gattinger]

Does your project use/import Mathlib? What does your lakefile.toml look like? In my project with this toml file I can run lake exe lint-style without any further changes.

Just guessing, but does lake build compile all the files you want it to? / Do you havedefaultTargets set in the toml file? (You can also try lake exe lint-style MyModuleName it seems.)

[Iván Renison]

It does use Mathlib. This is my lakefile (almost the default):

name = "LeanOJProblems"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["LeanOJProblems"]

[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true
maxSynthPendingDepth = 3

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.26.0"

[[lean_lib]]
name = "LeanOJProblems"
globs = ["LeanOJProblems.*"]

I tryed adding the lintDriver option that you have, and the weak.linter.flexible option, but it also does not give any error.
And this is a Lean file that I think should give a style error of having a line to long:

import Mathlib.Data.Real.Sqrt

theorem solution (a b c : ℝ) (ha : a > 0) (hb : b > 0) (hc : c > 0) (h : 1 / a + 1 / b + 1 / c = 1) : a + b + c ≤ √ (b ^ 3 + a * c ^ 2 + a ^ 2 * c) := sorry

But even if I put that in LeanOJProblems/Basic and I do lake exe lint-style LeanOJProblems.Basic I don't get anything

[Kim Morrison]

The long line linter happens under lake build, not lake exe lint-style.

[Iván Renison]

Oh, I see, that was my problem

[Iván Renison]

Thank you!

[Iván Renison]

So what does lake exe lint-style checks?

[Malvin Gattinger]

Spaces before/after ; for example.

[Kim Morrison]

claude -p 'What does lake exe lint-style check for?'

[Iván Renison]

What is claude -p?

[Kim Morrison]

I'm trying to teach you how to fish. If in 2026 you haven't worked out how to use Claude Code, you really really should. :-)

[Kim Morrison]

The command above, run in the Mathlib repo (but probably would work fine anywhere downstream of Mathlib), outputs a moment later:

lake exe lint-style runs text-based style linters on Lean files. It checks for:

Line-level checks:

1. Adaptation notes (ERR_ADN) - Flags "Adaptation note" strings; should use #adaptation_note command instead
2. Windows line endings (ERR_WIN) - Flags \r\n line endings; should use Unix \n
3. Trailing whitespace (ERR_TWS) - Flags lines ending with spaces
4. Space before semicolon (ERR_SEM) - Flags ; patterns
5. Disallowed Unicode (ERR_UNICODE) - Flags blocklisted Unicode characters

Module-level checks:

6. UpperCamelCase naming - Module names must be UpperCamelCase (with some exceptions like lpSpace)
7. Windows-forbidden filenames - No CON, PRN, AUX, NUL, COM1-9, LPT1-9 as components
8. Forbidden characters - No !, ., <, >, ", /, \, |, ?, *, or whitespace in module names

Mathlib-specific checks:

9. Mathlib.Init imports - Every Mathlib file must transitively import Mathlib.Init
10. Scripts documentation - Every file in scripts/ must be documented in scripts/README.md

Usage:

• lake exe lint-style - lint default Lake targets
• lake exe lint-style --fix - auto-fix fixable errors
• lake exe lint-style --github - output for GitHub problem matchers
• lake exe lint-style Mathlib.Foo - lint specific module and its imports

[Kim Morrison]

Helpful, no?

[Iván Renison]

I was using Github Copilot and ChatGPT, but I was not able to solve any Lean configuration things with them. Maybe I should try this

[Iván Renison]

Thank you

[Kevin Buzzard]

I see interesting analogies with a couple of decades ago, when there were two kinds of people in the world: those who had realised that asking google was a good way to get general information, and those that continued to ask easily google-able questions on forums and were occasionally being redirected to google by people for whom the penny had dropped.

[Iván Renison]

One more question, how can I get the style warnings of lake build to be errors? (for CI to fail)
AI suggested to use moreLeanArgs = ["-werror"] in the lakefile, or moreLeanArgs = ["--warningAsError"] or moreLeanArgs = ["--wErr"], but it does not work (also it does not work passing -werror, --warningAsError or --wErr to the command when running it from the command line)

[Ralf Stephan]

Until about November 2025 it was nothing, but then Claude + Opus 4.5 stepped up the quality: for coding, and astonishingly it's also good enough to Lean-formalize undergrad proofs. I make a plan with Gemini (because no one beats Google with web search) and feed the plan to Claude.

[Iván Renison]

I also found --wfail and --fail-level==warning in the documentation, but these are accepted by lake, but do not seem to work
Any way, I would need something that accepts sorrys, which produce a warning