Zulip Chat Archive

With the recent reboot of the tactic porting effort, I've noticed some mathlib4 PRs that could benefit from the "style linter" from mathlib3. Thus I've opened https://github.com/leanprover-community/mathlib4/pull/352, which ports across the mathlib3 style linter (written in python) for the mathlib4 repository. That PR just contains the minimal changes required to have it run.

Scott Morrison (Jul 27 2022 at 00:23):

There are a few style linters that probably just need to be removed (e.g. curly brace style is evolving, so we should certainly throw out that one).

Scott Morrison (Jul 27 2022 at 00:24):

Eventually of course we'd like to rewrite these in Lean rather than python, and even have code suggestions to fix them before CI. But perfect is the enemy of good, and I think it's worthwhile to use the old style linters now to ensure basics like module docs and copyright headers get written.

Scott Morrison (Jul 27 2022 at 00:25):

I don't propose that we go back and fix the style exceptions in the entire Mathlib/ directory, as hopefully these will mostly be clobbered as mathport runs anyway.

Scott Morrison (Jul 27 2022 at 00:26):

However it would be reasonable / helpful if we could fix the style exceptions for the Mathlib/Lean/ Mathlib/Util/ and Mathlib/Tactics/ directories, before they age too much. I'll aim to do at least some of this.

Heather Macbeth (Oct 18 2022 at 18:44):

I got a couple of "missing docstring" linter issues on mathlib4#478:

#check Fin2.IsLt.h /- definition missing documentation string -/
#check Fin2.term&_ /- definition missing documentation string -/

The first is a field of a class; the class itself has a docstring. I don't think mathlib3 would have asked for a docstring here. Is this a new policy? Is this something I can mark as nolint?

The second I don't even recognise, it's not in the file. Is it autogenerated?

David Renshaw (Oct 18 2022 at 18:46):

I'm guessing that the second one is referring to local prefix:arg "&" => ofNat'

Heather Macbeth (Oct 18 2022 at 18:47):

Hmm ... in mathlib3 you also did not have to (in fact were not allowed to) give docstrings to notation.

Mario Carneiro (Oct 18 2022 at 18:48):

For the first thing: It's a new policy. You should not mark it as nolint, but you should add it to the nolints file (although if it's not too hard to add docs then please do)