weak.linter.mathlibStandardSet and lint-style-action

Stream: general

[Chris Henson]

I am confused about the setup for a project using

[leanOptions]
weak.linter.mathlibStandardSet = true

in lakefile.toml and how this interacts with lint-style-action. Can/does lint-style-action run these lints? In our workflow log we also get these errors:

warning: nolints file could not be read; treating as empty: scripts/nolints-style.txt
error: `print-style-error.sh` exited with code 255
could not execute external process './scripts/print-style-errors.sh'

Are we meant to add these (and ./scripts/lint-style.py) to our repo? Doing so does still not seem to report the lints enabled by weak.linter.mathlibStandardSet.

[Michael Rothgang]

CC @Anne Baanen

[Michael Rothgang]

I'll try to take a look tomorrow - if you haven't heard an answer by 2025-08-06T14:00:00+02:00, feel free to @mention me as a reminder.

[Michael Rothgang]

Anne: is this action supposed to only run in projects depending on mathlib? If not, where does the action get the lint-style executable from?

[Michael Rothgang]

Until tomorrow, let me explain some background:

• this action was made to run some of mathlib's linters in other repositories also --- this is why a mathlib assumption might be (unintentionally) present or undocumented
• mathlib has three different kinds of linters: text-based linters, syntax linters and environment linters
• environment linters are defined in batteries; you can run them with lake exe runLinter (but currently not enable or disable individual lints[1])
  This action is not about these.

[1] I have an old work in progress branch which implemented this. If you need this, I could certainly resurrect it, or help you do so. So far, it never became important enough.

[Michael Rothgang]

• you can run environment linters during editing by writing #lint in your Lean file

[Michael Rothgang]

• syntax linters provide direct feedback on your code (i.e., some of the squiggly yellow lines you may see if you work in mathlib). They are controlled by mathlib options like linter.style.refine. You can enable or disable them in your file using something like set_option linter.style.refine true.

[Michael Rothgang]

• you can also configure which syntax linters to run using your lakefile

[Michael Rothgang]

• a recent feature are linter sets, allowing you to control a lot of linters at once: there is one for all the mathlib linters --- that's basically equivalent to enabling each mathlib linter one by one

[Michael Rothgang]

• the final kind of linters are text-based linters. They were originally writing as a Python script (scripts/lint-style.py). Most of them have been rewritten in either Lean (scripts/lint-style.lean) or as syntax linters. The remaining ones also will be, but doing so is not the highest priority --- hence may take a while. (Help is welcome!)

[Michael Rothgang]

I haven't verified this yet, but my guess is that

• lint-style-action is only about running the text-based linters,
• while linter.mathlibStandardSet is about syntax linters.

In other words, what you're asking about are two different things, that can be used independently of each other.

[Michael Rothgang]

I'll further guess that

• the lint-style-action assumes your repository depends on mathlib (so you'd have the lint-styleexecutable accessible, as well as all the other scripts) --- so, no, you're not meant to copy script/lint-style.py, script/nolints-style.txt or print-style-errors.sh).

[Michael Rothgang]

I'll have to run now, I can double-check tomorrow.

[Chris Henson]

I see, I was vaguely aware of the different linters, but this description is helpful. I think this refines my questions to:

1) Our project (https://github.com/cs-lean/cslib) does depend on Mathlib. For some reason, the action is still not able to access the appropriate scripts for text-based lints.

2) What would be the preferred way to check for syntax lints, as enabled in our lakefile with weak.linter.mathlibStandardSet, in CI? Is there a lake command to run for these? (I do see them when when running lake build, but I was looking for something with an exit code to use in CI)

[Michael Rothgang]

I'll have to think about (1), but can answer (2) already: I would

• ensure you have the linter set enabled: doing so in your lakefile is good; I would even go one step further and replace it by linter.mathlibStandardSet. (If a file in your project doesn't import anything in mathlib, the weak version will not run any of the syntax linters, whereas the other version will error and tell you you forgot to import this. Importing almost any file from mathlib will do. You could have a file CSLib/Init.lean which everything imports, which imports some mathlib.)

[Michael Rothgang]

• as you said, running lake build already runs all syntax linters: the only part is to error when you get any warning. There's a lake option for that.

[Michael Rothgang]

I believe it's the --wfail option.

[Anne Baanen]

Michael Rothgang said:

Anne: is this action supposed to only run in projects depending on mathlib? If not, where does the action get the lint-style executable from?

The Python script was supposed to migrate to the lint-style-action but that doesn't seem to have actually happened.

[Kim Morrison]

I've just needed to add

weak.linter.pythonStyle = false
weak.linter.checkInitImports = false
weak.linter.allScriptsDocumented = false

to the Cslib lakefile, unfortunately, so this is still a live issue.

[Kim Morrison]

Can we modify the setup in Mathlib so that these three are not activated by mathlibStandardSet?

[Kim Morrison]

The pythonStyle linters could be made to work, but more care would be needed so that when run in a downstream repo the script is actually findable (because it will be somewhere under .lake, rather in the ./scripts/).

[Kim Morrison]

(Better of course is not to have python scripts. :-)

[Kim Morrison]

I think it is safe to say checkInitImports and allScriptsDocumented should not be activated in downstream projects: #30541

[Kevin Buzzard]

Is checkInitImports the reason I get a really annoying error every time I make a scratch file in a local copy of FLT? invalid -D parameter, unknown configuration option 'linter.mathlibStandardSet'

[Kim Morrison]

@Kevin Buzzard, if you read the rest of the error message you quote you'll see it says:

invalid -D parameter, unknown configuration option 'linter.mathlibStandardSet'

If the option is defined in this library, use '-Dweak.linter.mathlibStandardSet' to set it conditionally

and indeed if you modify your lakefile by replacing the lines

linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`)
# Enable all mathlib linters: automatically matches what mathlib uses.
linter.mathlibStandardSet = true

with

weak.linter.flexible = true # no rigid tactic (e.g. `exact`) after a flexible tactic (e.g. `simp`)
# Enable all mathlib linters: automatically matches what mathlib uses.
weak.linter.mathlibStandardSet = true

then the error messages in scratch files disappear. :-)

[Kim Morrison]

(Acknowleding that the error message is not ideal: instead of "If the option is defined in this library" it should say "If the option is defined in a library".)

[Kim Morrison]

lean#10844

[Kevin Buzzard]

My rule of thumb is: I have no understanding of my lakefile or of any consequences of fiddling with it, so don't touch it. In short, if I change the lakefile to silence that error then I have no understanding of the other consequences. Basically it is always other people who are editing my lakefile. I'll give it a go... (edit: FLT#753)

[Michael Rothgang]

Late to the party, but let me try to help: does that scratch file import Mathlib/Init.lean (perhaps transitively)? I would expect the answer is "no", and importing it to fix your error.

[Michael Rothgang]

Short explaination: the mathlibStandardSet is a "linter set", i.e. you can enable or disable a collection of linters at the same time. (In other words, set_option linter.mathlibStandardSet true is just a shorthand for saying set_option linter.foo true for various linters foo in mathlib.)

[Michael Rothgang]

That linter set is defined in Mathlib/Init.lean (search mathlib for mathlibStandardSet and you'll find that). So if you don't have that file imported, lean complains about the unknown option.

[Michael Rothgang]

Mathlib/Init.lean is imported by every other file in mathlib, so any mathlib import in your scratch file will make the error go away.

[Michael Rothgang]

Can we emit a custom error message for this particular option, that explains how to fix this? I.e., for this particular error, append a

hint: this linter is defined in mathlib, make sure you import any file from `Mathlib` to get access to this linter

to the error message?

[Michael Rothgang]

(Up to word-smithing: perhaps "this linter set" or "this option" would be better.)

[Kim Morrison]

The problem is rather when you make an empty file, linter.mathlibStandardSet doesn't exist, so you get an error! This is why it needs to have weak. prepended.

Creating empty files in downstream repositories should not generate errors: these can be useful for quickly checking syntax, documentation, etc.

[Michael Rothgang]

But the weak will silence any errors about this linter being unintentionally imported in non-empty files. I think we should do better here.

[Michael Rothgang]

I agree that the user experience of errors in an empty file is not great. But I think we should strive for a different solution.

[Chris Henson]

To rephrase, your ideal behavior is that in this error we give instructions on how to import the linter, rather than the distinct decision to suppress an error with weak? This has merit IMO. I've been thinking about this for CSLib where we use weak, opening the door to some leaf files independent of Mathlib not being linted as we would like.

As a practical matter, how would the library specific error message get appended? The error message is from core where it's just checking that the option declarations exist.

[Kevin Buzzard]

@Michael Rothgang Basically, my workflow is:

I'm working on FLT and take a break to browse Zulip.
I see a post from someone saying "I'm learning Lean, I'm a beginner, here is my basic question, this is core Lean, my MWE doesn't import mathlib".
I dump the question into a scratch file in FLT and I get an error rather than warning.

I am happy to ignore warnings but I am super-scared about ignoring errors; my rule of thumb is not to trust any output whatsoever after the first error, and in this case the first error is always on the first line.

I totally understand that import Mathlib.Init will fix this. However it will also import random other things which might even stop me answering the question, e.g. because the behaviour of the code might change if I add this import.

[Michael Rothgang]

Thanks for explaining. I understand better now.

[Michael Rothgang]

In this particular case, I don't think you need to be scared about import Mathlib.Initchanging the behaviour of your code. (Its imports are intentionally minimal: syntax linters, two of mathlib's environment linters and the #min_imports command. In particular, the file defines no new syntax, no new notation and enables no linters by itself. That's seems pretty innocuous.)

[Michael Rothgang]

That said: a different solution could be to use the weak prefix, but add a linter (you can enable in FLT) that checks every file imports Mathlib.Init (or FLT.Init or something) transitively. This would allow you to work with an empty scratch file, but also ensure that you don't accidentally forget to lint an FLT file.

[Michael Rothgang]

(Though I guess almost every non-trivial FLT file will import something from mathlib anyway, so perhaps using weak is just fine and there's no reason for me to be worried?)