Module docstrings

Stream: general

[Yaël Dillies]

In a month we cut down the number of missing module docstrings by a quarter. It went from 192 on the 1st of June to 140 today! :tada:

[Yaël Dillies]

For those interested, here is the number of files without module docstring each top folder still contains

61 tactic
27 category_theory
23 data
9 control
5 topology
3 deprecated
3 order
2 logic
2 set_theory
1 algebra
1 analysis
1 computability
1 measure_theory
1 meta

[Johan Commelin]

@Yaël Dillies Thank you very much for this great effort! It's appreciated! :octopus: :tada: :top_hat:

[Eric Wieser]

Yes, from what I've seen that's a very charitable use of the word "we"! Thanks for taking this on.

[Yaël Dillies]

And we've now cut it down by half! Only 95 to go :tada:
Among others, thanks to Scott Morrison and Bhavik Mehta for category theory, and Bolton Bailey for alists!
Here is the updated breakdown by top folder:

58 tactic
15 category_theory
9 data
4 control
4 topology
2 deprecated
1 logic
1 computability
1 meta

[Patrick Massot]

Could you tell me what are the 4 topology files? Those should be very easy to fix

[Yaël Dillies]

You have them here:

• topology.algebra.group_completion
• topology.algebra.open_subgroup
• topology.algebra.uniform_ring
• topology.category.Top.open_nhds

[Bryan Gin-ge Chen]

(deleted)

[Johan Commelin]

Wow, style_exceptions.txt is only 104 lines long!

[Johan Commelin]

I expected more stuff, apart from module docstrings.

[Yaël Dillies]

#8973 removed a lot of ERR_LIN.

[Patrick Massot]

This is not nolints.txt which has 900 lines

[Johan Commelin]

Yes, I know. But I was still surprised.

[Yaël Dillies]

nolints.txt also got pretty smaller, except for Floris' new fails_quickly linter.

[Johan Commelin]

The errors that are not ERR_MOD:

26:src/data/pfunctor/multivariate/M.lean : line 43 : ERR_LIN : Line has more than 100 characters
27:src/data/pfunctor/multivariate/W.lean : line 42 : ERR_LIN : Line has more than 100 characters
28:src/data/qpf/multivariate/basic.lean : line 73 : ERR_LIN : Line has more than 100 characters
29:src/data/qpf/multivariate/constructions/cofix.lean : line 38 : ERR_LIN : Line has more than 100 characters
30:src/data/qpf/multivariate/constructions/fix.lean : line 47 : ERR_LIN : Line has more than 100 characters
31:src/data/qpf/univariate/basic.lean : line 35 : ERR_LIN : Line has more than 100 characters
54:src/tactic/induction.lean : line 1329 : ERR_RNT : Reserved notation outside tactic.reserved_notation
100:src/testing/slim_check/testable.lean : line 552 : ERR_LIN : Line has more than 100 characters

[Yaël Dillies]

Note that the first 6 ones are all caused by a certain paper that I should not quote written by certain people that I should not quote who decided on a long paper name. :upside_down:

[Rob Lewis]

https://leanprover-community.github.io/mathlib_stats/nolints.png hasn't been posted in a while

[Yaël Dillies]

What's the time span?

[Rob Lewis]

It starts late 2019, would be my guess? The x axis is commits, not dates, so time isn't linear

[Rob Lewis]

Nov 8, 2019

[Scott Morrison]

#9990 does 10 out of the 15 remaining missing module docs in category_theory.

[Yaël Dillies]

You know how to speak to me :blush:

[Patrick Massot]

Yaël Dillies said:

You have them here:

• topology.algebra.group_completion
• topology.algebra.open_subgroup
• topology.algebra.uniform_ring
• topology.category.Top.open_nhds

I opened PRs adding docstrings to those files. In #10111 I also added a lattice instance because it was weird to write the docstring without this instance, and it didn't seem to be implied by the other instances. But maybe our order hierarchy gurus should have a look. We already have docs#open_subgroup.semilattice_inf_top and docs#open_subgroup.semilattice_sup_top but this does not imply the corresponding lattice instance. Is it dangerous or useless to add this instance?

[Yaël Dillies]

Looks fine to me!

[Johan Commelin]

What kind of markdown syntax is this? https://github.com/leanprover-community/mathlib/blob/master/src/data/qpf/univariate/basic.lean#L35 Does it allow for linebreaks in some way?

[Eric Wieser]

You can put line breaks inside the first []

[Yaël Dillies]

Oh really? Then I can fix the last few ERR_LIN!

[Johan Commelin]

#10136 is an attempt at adding an indentation linter. But I would prefer if these are "gentle warnings" instead of "harsh errors".

[Johan Commelin]

There will probably be many false positives

[Johan Commelin]

@Bryan Gin-ge Chen do you know if ::error vs ::warning has different impact on CI checkmars in GH actions?

[Scott Morrison]

Many of the warnings seem spurious!

[Scott Morrison]

Although I'm surprised how few there are.

[Johan Commelin]

I'm trying to improve a bit more. match..end blocks are adding to the problem.

[Johan Commelin]

But that's exactly why I want these to be very gentle warnings. They should be very easy to ignore.

[Johan Commelin]

Ideally, we would invoke the linter by manually running some GH action on PRs that could use a bunch of this advice.

[Johan Commelin]

The current version is better

[Johan Commelin]

I haven't look at everything it flags, but a random sample is showing actual mistakes

[Johan Commelin]

One false positive consisted of an extra-indented simp-config. I think extra-indenting those is good practice.

[Johan Commelin]

calc blocks are another feature where there is a lot of indentation-style-variation. Maybe I should just skip those as well.

[Johan Commelin]

At least for now.

[Alex J. Best]

That was my first thought when I saw the output, how come there aren't a billion warnings about calc blocks already?
Also are you dealing with lists of simp/rw lemmas, there are (at least) two styles in use:

rw [some_lemma,
    some_other_lemma],

and

rw [some_lemma,
  some_other_lemma],

[Alex J. Best]

Also, @Arthur Paulino mentioned a prettier plugin the other day, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20prettier.20pluggin/near/259574899, personally I think this could be worth the effort to make a simple one even in lean 3 :smile:

[Arthur Paulino]

@Alex J. Best count me in if you want to give it a try, even if just as an attempt to get the hang of Prettier.

[Bryan Gin-ge Chen]

Johan Commelin said:

Bryan Gin-ge Chen do you know if ::error vs ::warning has different impact on CI checkmars in GH actions?

I think it just affects the color of the message that GitHub displays by the error, but @Eric Wieser would know better than I would.

[Eric Wieser]

Yes, I think that's correct

[Eric Wieser]

There's an info one too I think, that doesn't cause a CI failure

[Johan Commelin]

Aah, that sounds like what I'm looking for!

[Johan Commelin]

@Alex J. Best Currently, I only lint the indentation of lines starting with {

[Johan Commelin]

I pushed an update that removes some false positives. It now flags 140 indentation errors in mathlib. My N<10 sample shows that they are true positives.

[Johan Commelin]

@Bryan Gin-ge Chen Is it easy to support this linter as an Action that can be manually invoked?

[Johan Commelin]

Because, I'm not sure if we want to include it by default...

[Johan Commelin]

#10163 fixes almost all things flagged by the indentation linter. The remaining six warnings are false positives.

[Bryan Gin-ge Chen]

Johan Commelin said:

Bryan Gin-ge Chen Is it easy to support this linter as an Action that can be manually invoked?

It's probably not too hard, but it would take some time. The way to do this that comes to mind is the following:

1. The linting script would need to be refactored a bit to accept a command line parameter to run only select linters.
2. We'd need an additional GH action which runs when new comments are posted and runs the style linter if it detects certain strings (possibly parsing some provided options); if I were to do this, I'd probably work off the #deploy script in the doc-gen repo.

[Johan Commelin]

Maybe it's possible to always run the linter... there are only a few false positives left.

[Johan Commelin]

The main issues:

• Lines of the form

  exact ⟨some long stuff,
    {x}, more stuff⟩

• Blocks of the form

  split;
  [{ tac1, tac2 },
   { tac3, tac4 }],

[Johan Commelin]

I don't know what people think about the $2n+1$ indentation in the second block.

[Johan Commelin]

The first block is certainly legitimate. It's a pattern that occurs twice in mathlib (according to the linter).

[Johan Commelin]

The 2nd block occurs 3 times

[Eric Wieser]

You could ignore any {}s inside ⟨⟩

[Johan Commelin]

Hmm, good idea. And also inside []. I'll add some tracking.

[Johan Commelin]

Done

[Johan Commelin]

That worked great. The linter is now happy with all of mathlib

[Johan Commelin]

• #10136 is the linter, which doesn't pass CI
• #10163 is all the fixes, which is blocked by :this:

Do we just want the second PR, instead of two separate PRs?

[Floris van Doorn]

You could remove the linter from the second PR (so that it doesn't depend on the first). Or we could accept it in one go.

[Johan Commelin]

Let's go for the "in one go" option.

[Scott Morrison]

Johan Commelin said:

• Blocks of the form

  split;
  [{ tac1, tac2 },
   { tac3, tac4 }],

I don't understand why you'd write it like this in the first place. Why not just remove the ; and [, ]?

[Eric Wieser]

Because {} inside [] is not solve1 but just a sequential combinator

[Eric Wieser]

So if you remove the [], then tac2 and tac4 are required to close all their goals

[Johan Commelin]

That being said: are people in favour of merging #10163?