introducing docstrings while porting

Stream: mathlib4

[Johan Commelin]

@Eric Wieser I noticed that you asked to not add docstrings while porting. I don't see why it should be a problem to add them. It's not going to break any tooling right?

I agree we shouldn't randomly refactor code. Even though that is still happening due to various factors.

Can you please explain why you wouldn't want docstring fixes while porting?

[Eric Wieser]

I think my objection was primarily "don't do it in a porting PR", not "don't do it at all until the port is done"

[Johan Commelin]

But even in a porting PR, I don't see why it is problematic.

[Eric Wieser]

Because when reviewing a porting PR, the assumption is that all the docstrings are inherited from mathlib3 and therefore out of scope for suggestions beyond name corrections

[Eric Wieser]

The more that becomes in scope for a porting PR, the harder reviewing them becomes

[Johan Commelin]

Well, I've not found it hard in practice. During the port, several typos in docstrings have been fixed. And I think that's a good thing.

[Johan Commelin]

It's not realistic to expect people to make separate PRs for such tiny typos. Then it will just not happen.

[Eric Wieser]

The PR I'm thinking of added some new docstrings that IMO weren't great, and then I had to spend time working out whether the docstrings were the same as what we used to have in mathlib3, or if the not-greatness was introduced in the PR.

[Johan Commelin]

You should review the commits[3:] when reviewing porting PRs. Then it is immediate that they are new.

[Reid Barton]

I've seen the "new docstrings that are not great" behavior too. I think it's due to a hyperactive docBlame linter.
I agree that fixing typos in docstrings is fine.

[Reid Barton]

I think during the port we should just disable the docBlame linter entirely

[Eric Wieser]

From what I remember, reviewing commits[:3] stops working as soon as a merge from master happens

[Johan Commelin]

So we should git rebase and git push -f.

[Johan Commelin]

Without commits[3:] working, the reviews indeed become terrifying.

[Yury G. Kudryashov]

Eric Wieser said:

From what I remember, reviewing commits[:3] stops working as soon as a merge from master happens

That's why I started rebasing instead of merging in mathlib4 PRs.

[Scott Morrison]

I'd forgotten we'd disable the docBlame linter... We are now missing doc-strings in many tactic PRs as a result.