lint-style for downstream libraries

Stream: mathlib4

[Yaël Dillies]

I would like to enforce mathlib style in a downstream library. I tried using lake exe lint-style, but it fails because it hardcodes the name of the sublibraries Archive and Counterexamples. Furthermore, it does extra stuff like checking that the files in scripts are documented and checks that Mathlib.Init is imported in all files.

[Yaël Dillies]

Could we

• move those two extra steps to another executable
• modularise lint-style so that it runs on a specific sublibrary?

[Yaël Dillies]

Actually, I can't see what lint-style does apart from those two extra steps?

[Michael Rothgang]

lint-style currently does three things, which are all mentioned in lintStyleCli:

• run the text-based linters on all .lean files (that's the lintModules) step
• check that every file in scripts is documented
• check that Mathlib.Init is imported in all files

[Michael Rothgang]

Your request ("give me a way to run lint-style on downstream projects") is a very reasonable one. I agree with making the libraries configurable.

[Michael Rothgang]

I'm not sure about moving the extra steps to another executable. I'd prefer one executable lake lint (which could include runLinter, the current lint-style and possibly others, such as shake) over five different executables.

[Michael Rothgang]

I could, however, imagine

• moving those extra checks behind a flag (perhaps lake exe lint-style --mathlib enables them --- or lake exe lint-style --downstream disables them)
• actually, perhaps it's nicer to couple that to subdirectories being passed in: if a library is specified which is not mathlib, don't run these checks?

[Yaël Dillies]

What bothers me is that nothing in lint-style says it's coming from mathlib. In fact, I thought for a second it was a core thing

[Yaël Dillies]

I am of the opinion that, if a generically-named executable is doing mathlib-specific logic, this logic should be hidden behind a mathlib-named flag. Does that sound reasonable?

[Yaël Dillies]

(I doubt lake exe cache get is currently exactly following this rule, but at least it doesn't seem disastrously so from the user side)

[Michael Rothgang]

I had a quick moment on the TGV, and produced #21476. Does that address your use-case/would you like to test on a downstream project?

[Michael Rothgang]

TL;DR Run lake exe lint-style Mathlib or lake exe lint-style inside mathlib for the usual operations; run lake exe lint-style Carleson in a project Carleson depending on mathlib.

[Yaël Dillies]

Thanks Michael for the quick ( :high_speed_train:) turnaround! I will have a look tomorrow