Labelling abuse

Stream: mathlib4

[Patrick Massot]

I'm furious @Jeremy Tan took the liberty of editing tags in my PR !4#3383 which got accidentally merged as a result. My PR was correctly tagged as WIP and he removed that tag and put awaiting-review instead. Scott was then misled into thinking that PR should be merged. I realized just now when I pushed a new commit only to discover the PR was already merged.

[Eric Wieser]

In the short term we could revert the commit (by making a PR to do so) on master and re-open the PR

[Eric Wieser]

If you want to do that you should do it soon before people start porting files that depend on it

[Patrick Massot]

It isn't crucial, I only wanted to finish cleaning up the file, in particular in the direction explained in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/induction.20in.20mathlib4. I also wanted to check all names since I'm not yet fully fluent in the new naming convention, but I'll assume they were ok since Scott merged.

[Patrick Massot]

The merged version also has completely messed up indentation, for instance https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Algebra/RingQuot.lean#L693-L698

[Matthew Ballard]

It also looks like comments still have Lean 3 names It looks like Patrick didn’t get a chance edit the Lean 3 names in the comments (edited for clarification)

[Patrick Massot]

Indeed I also didn't had time to check that yet.

[Patrick Massot]

I just opened !4#3577.

[Jeremy Tan]

I have created a not-formatted label. If your port file is compiling but you have not fixed up the formatting and comments, add the label to prevent premature merging

[Eric Wieser]

I don't think that's useful; in general the WIP label means "I am still working on this". If the PR is basically done and just needs fixes to compile then as an author you should label with "awaiting-CI" instead.

[Patrick Massot]

Jeremy Tan, you are not the one deciding how we work on this project.

[Jeremy Tan]

I'm sorry

[Jeremy Tan]

Eric Wieser said:

I don't think that's useful; in general the WIP label means "I am still working on this". If the PR is basically done and just needs fixes to compile then as an author you should label with "awaiting-CI" instead.

If there's a WIP label and the CI passes, those two pieces of information don't give immediate indication that the PR should not be merged immediately because the formatting hasn't been done yet

[Mario Carneiro]

If there is a WIP label, then it's not ready to merge, and only the author can say when it should have that label removed

[Jeremy Tan]

The not-formatted label serves as such an immediate indication

[Mario Carneiro]

CI passing or formatting doesn't really matter for that consideration

[Yaël Dillies]

Jeremy, if I open a WIP empty PR, are you going to mark it awaiting-review? It passes CI after all.

[Jeremy Tan]

In that case I'm concerned of the possibility that a PR porting an important file keeps the WIP label for a long time because the author keeps wanting to make it "perfect", and hinders progress as a result

[Jeremy Tan]

Yaël Dillies said:

if I open a WIP empty PR, are you going to mark it awaiting-review? It passes CI after all.

No

[Yaël Dillies]

Patrick committed https://github.com/leanprover-community/mathlib4/pull/3383/commits/c6c0e3cf19e4c823690361169622768405643100 at 2023-04-20T17:39:00+01:00. You changed the labels at 2023-04-21T02:36:00+01:00. I don't see how this can be considered "a long time".

[Bulhwi Cha]

Jeremy Tan said:

In that case I'm concerned of the possibility that a PR porting an important file keeps the WIP label for a long time because the author keeps wanting to make it "perfect", and hinders progress as a result

In that case, you can discuss it with the author before you make changes to the PR.

[Jeremy Tan]

Sometimes – but more often for me – the authors feel very slow to respond. More often for me because I live on the other side of the world from America (+8)

[Jeremy Tan]

I work best in a setting where I can get instant response from other people

[Bulhwi Cha]

You should wait for others to respond.

[Bulhwi Cha]

By the way, I also live on the other side of America. Korea Standard Time (KST) is UTC+9. I've ported only one file so far, but I'm planning to port more files from now on.

[Jeremy Tan]

Bulhwi Cha said:

You should wait for others to respond.

:squared_ok:

[Arthur Paulino]

@Jeremy Tan working on a big project such as mathlib will require extra patience. The more complex a project is, the easier it is to go chaotic. Slowdown can be welcome in these scenarios, so we avoid stepping on each other's toes.

In situations like this, however, the common practice is to strengthen the guidelines/culture to avoid future similar problems. Believe me, companies have much bigger incidents that cost potentially dozens of thousands of dollars. And the most resilient cultures don't punish employees who make mistakes.

I'm saying this to motivate the enhancement of the guidelines for contributing to mathlib. If the project grows by inviting ppl to be collaborators, this kind of event is always latent.

[Arthur Paulino]

@Jeremy Tan where do you think a guideline that's explicit and specific about this would be better placed at? Is there a page in the mathlib community website you see fit?

[Jeremy Tan]

@Arthur Paulino perhaps the mathlib4 porting wiki would be a good place

[Eric Wieser]

A CONTRIBUTING.md in the github repo would probably be a reasonable thing to have

[Patrick Massot]

I don't think that more documentation would help with users that ignore repeated direct and precise instructions not to mess up with PRs labels.

[Arthur Paulino]

Where are those instructions, Patrick?

[Sebastien Gouezel]

To make it more explicit: @Jeremy Tan , please never change any label on any PR you haven't opened yourself.

[Mauricio Collares]

Arthur Paulino said:

Where are those instructions, Patrick?

On Zulip, for example.

[Arthur Paulino]

Then maybe the community needs stronger processes and mechanisms for inviting people to be collaborators. Like starting out with forks and then after a certain point (20 PRs, say), the person can ask to be a collaborator and then must read and accept explicit guidelines. Exceptions can be made for direct invites by an older collaborator (who has been a collaborator for 6 months, say)

That was just a draft. Imagine where mathlib will be when 1000+ ppl are contributing to it

[Ruben Van de Velde]

I think it's worked really well so far, fwiw. The main thing is that we don't want people to contribute from forks because of CI reasons

[Mauricio Collares]

Regarding this proposal, I think it's fair to say Jeremy is contributing a lot and would probably pass any reasonable PR minimum, especially during the porting process.

[Mauricio Collares]

I honestly believe he means well and just couldn't resist doing the action which would make the process move a bit faster. That does not mean that it was the correct thing to do, but I think it's far from an adversarial situation.

[Arthur Paulino]

Good point. But I still think that an explicit "I have read the guidelines" is a healthy check, especially for those with good intentions

[Mauricio Collares]

As a lurker who really enjoys how friendly everyone is here, I think that whatever guidelines are created should emphasize that collaboration is the main goal. In the grand scheme of things, getting Mathlib ported a month earlier is not nearly as important as having a healthy research project. This has other aspects which are relevant here (for example, pinging people too soon does not acknowledge that people have other priorities, which causes undue stress). I think having a progress bar creates an opposing incentive which must be managed appropriately.