CI was passing with PRs with long lines even before you proposed deleting the line which was supposed to be catching them?

Well, as I see it

• the grep step was supposed to catch lines longer than 100 characters --- but didn't quite work, since there were longer lines
• the syntax linter step also catches long lines: but it works wherever it is imported. (Ensuring the flexible linter is imported everywhere, as your last PR did, suffices.)
• Thus, both steps should have worked the same --- except that in practice, the grep check didn't work.

Let me fix the linter invocation, just a moment.

(You need to re-click the "approve workflow" button: github wants to prevent me from mining cryptocurrency on your CI, presumably against your will. I approve of the goal, but that means extra work for you...)

I added the mk_all --check step to CI as well, which pointed out that something was missing. #430 updates the file.

The CI step works - the workflow fails because there are a couple of linter errors to fix :-)

Update: this PR can be merged once all pre-requisites have landed:
#430 will fix FLT.lean; #427 will fix the environment linter warnings (or nolint them), then this PR should should pass CI.

(There is of course a policy question: should one mandate new PRs adding doc-strings to all definitions? I'll leave that to you to decide.)

(There is of course a policy question: should one mandate new PRs adding doc-strings to all definitions? I'll leave that to you to decide.)

Yes I would like to do that! How do I do that?

NB I won't be closing #418 just yet -- I am now basically using it as a tracking issue for linters which I might want.

OK so I have rerun CI and there are a ton of errors. I will start on the definition docstrings. What do I do about #431 ? Should that be merged into this?

Oh I see -- I can just merge #431 independently, and also I can merge definition docstrings independently, and we can keep running CI on this until it passes? 💡

@grunweg I don't understand the workflow here. #431 has added this huge scripts/nolints.json file to the project, which makes me feel guilty, so now I made #437 adding some docstrings to definitions, and now this huge file needs to be edited right? How did you create it? IIRC in mathlib we occasionally get auto-generated PRs from Gabriel saying "let me remove some nolints for you". I'm not suggesting we need this but I guess it would be nice to know how you made the file, so I can remake it every time I fix some of the remaining issues.

Hopefully #439 is all that's left.

Once again, thanks so much!

You're very welcome!