Zulip Chat Archive

Stream: general

Topic: PR queue

Johan Commelin (Oct 19 2020 at 07:09):

It's been a while, but we have less than 100 open PRs again.

Tl;dr: If you feel like your PR is not getting the attention it deserves, please make sure that it shows up on this list:

To get your PR on that list:

  1. Make sure that it passes CI: mathlib should build, and all linters should be happy.
  2. Label your PR with awaiting-review. Of course you should only do this if you have addressed previous questions and comments by reviewers.
  3. If your PR depends on other PRs, label it with blocked-by-other-PR. But, crucially, please do not forget to remove this label once the dependencies are merged, because otherwise it will not show up on the above list.
  4. If one of our lovely bots has determined that there is a merge conflict it will label your PR with merge-conflict. Please fix the conflict, and then the bot will remove the label again.

Johan Commelin (Oct 19 2020 at 07:10):

To appreciate the amount of churn that mathlib sees: in the last week, we've merged > 100 PRs. For more stats, see https://github.com/leanprover-community/mathlib/pulse.

Johan Commelin (Oct 19 2020 at 09:49):

Scott created a linkifier, so that #queue now links to a bitly URL that forwards to this "narrowed-down" PR queue

Kevin Buzzard (Oct 19 2020 at 10:41):

I was just staring at github yesterday for the first time in a very long while, thinking "golly there's a lot to catch up on"

Kevin Buzzard (Oct 19 2020 at 10:41):

"I wonder if there is any algebra stuff?"

Kevin Buzzard (Oct 19 2020 at 10:42):

I had starred your message but that's a recipe for disaster for me right now

Johan Commelin (Oct 19 2020 at 10:45):

There have been lots of algebra bits and pieces, but nothing big, I think.

Bhavik Mehta (Oct 20 2020 at 00:31):

A very minor quibble but could we make the colours for awaiting-author and merge-conflict different?

Johan Commelin (Oct 20 2020 at 04:13):

@Bhavik Mehta In my mind I liked that they were the same, because both need attention from the author. Would you like them to be very different, or different but similar?

Bhavik Mehta (Oct 20 2020 at 13:57):

I'd like them to be different but similar, I agree that it's nice having them similar because they need attention, but they need different sorts of attention. I don't have strong feelings about this though!

Johan Commelin (Oct 20 2020 at 14:40):

I'm not an expert on colours, but I've tried to change the color a bit

Bhavik Mehta (Oct 20 2020 at 15:33):

Looks great to me, thanks

Johan Commelin (Jan 06 2021 at 19:02):

Wow! I feel like we did a lot of merges today.
https://app.bors.tech/repositories/24316/log suggests that we'll have ~20 PRs merged today.

But... #queue still has 45 items. :shock: :octopus: keep up the good work!

Rob Lewis (Jan 06 2021 at 19:33):

I'm happy some of you have had time to look at the queue, I haven't clicked on it all week!

Eric Wieser (Jan 06 2021 at 19:46):

Note that the log link is only visible to maintainers, the rest of us can only see https://app.bors.tech/repositories/24316

Johan Commelin (Jan 06 2021 at 20:01):

ooh, I didn't realise that... sorry

Oliver Nash (Jan 07 2021 at 13:00):

I know everyone's busy so I'm happy to wait but I claim this PR might now be an easy review if anyone wants to reduce the PR queue by one: https://github.com/leanprover-community/mathlib/pull/5575

Johan Commelin (Jan 18 2021 at 16:10):

I just kicked a PR on the queue with gptf as coauthor :tada: :robot:

they are coming

Rob Lewis (Jan 18 2021 at 16:11):

Sorry to say, they're already arrived :robot:

Rob Lewis (Jan 18 2021 at 16:14):

No one would have believed in the last years of the nineteenth century that this world was being watched keenly and closely by intelligences greater than man’s and yet as mortal as his own; that as men busied themselves about their various concerns they were scrutinised and studied, perhaps almost as narrowly as a man with a microscope might scrutinise the transient creatures that swarm and multiply in a drop of water. With infinite complacency men went to and fro over this globe about their little affairs, serene in their assurance of their empire over matter. It is possible that the infusoria under the microscope do the same.

Eric Wieser (Jan 18 2021 at 16:20):

Note that if we make the refactor suggested by @Anne Baanen here, we'll end up just reverting that PR in its entirety

Sebastien Gouezel (Jan 18 2021 at 16:21):

This PR was in fact the motivation for my question.

Damiano Testa (Jan 18 2021 at 16:54):

This is really exciting!!

Eric Wieser (Jan 27 2021 at 09:06):

19 PRs in a single batch at the moment!

Johan Commelin (Jan 27 2021 at 09:08):

I feel like we are going to break some record today (-;
We probably have to thank GPT :robot:

Alex J. Best (Jan 27 2021 at 09:14):

GPTs Ryder cup winning performance: https://github.com/leanprover-community/mathlib/pulls/jesse-michael-han

Patrick Massot (Jan 27 2021 at 09:31):

What is the actual story here? What are the respective contributions of GPT and humans? Are the proofs directly fom GPT or GPT suggested some lemma and Jesse and Stan polished?

Johan Commelin (Jan 27 2021 at 09:31):

Jesse made some cosmetic changes

Eric Wieser (Jan 27 2021 at 09:32):

It would be neat if the PRs could consist of the gpt-only commit followed by the human one, but I guess bors squashes that out of the history anyway

Damiano Testa (Jan 27 2021 at 10:21):

I believe that one of my PRs made it to the mergefest! It is kind of funky to be squashed at the same time that an AI PR also gets squashed! :grinning_face_with_smiling_eyes:

Damiano Testa (Jan 27 2021 at 10:23):

Not that it is very important, but where can I see the merge queue? Most of the links that I try come up with a Permission denied page.

Johan Commelin (Jan 27 2021 at 10:24):

Hmm, it might be only visible to maintainers... https://app.bors.tech/repositories/24316/log

Eric Wieser (Jan 27 2021 at 10:24):

Remove /log, https://app.bors.tech/repositories/24316. Note we discuss this already a little up-thread :)

Damiano Testa (Jan 27 2021 at 10:24):

Ok, yes: the link that you send gives a Permission denied page. No worries!

Damiano Testa (Jan 27 2021 at 10:25):

Ah, no log works: thanks, Eric!

I had missed the "no log" discussion above, sorry... :face_palm:

Johan Commelin (Jan 27 2021 at 10:26):

Johan Commelin said:

ooh, I didn't realise that... sorry

and now I forgot it :see_no_evil: :face_palm: :head_bandage:

Eric Wieser (Jan 27 2021 at 10:31):

I've opened bors-ng/bors-ng#1137 to hopefully make forgetting not relevant in future

Sebastien Gouezel (Jan 27 2021 at 12:13):

Another way to see what bors is currently doing is to look at https://github.com/leanprover-community/mathlib/tree/staging

Jesse Michael Han (Jan 27 2021 at 13:47):

Johan Commelin said:

Jesse made some cosmetic changes

currently gptf starts with the goal set to the type you see if you #print the theorem statement, so with everything to the right of the colon --- so i remove the first couple of intros, make obvious golfs like inlining apply ...s, haves, lets, squeeze nonterminal simps, etc.

Floris van Doorn (Jan 27 2021 at 19:08):

The changes by gptf are very nice!
Can you do some postprocessing (or teach gptf) to make it output by { tac1, tac2 } instead of by tac1; tac2 as per library style? (like in #5905 and #5911)

Johan Commelin (Jul 27 2021 at 13:59):

Hey everyone! I've been quite busy lately, and therefore the PR #queue didn't get so much of my attention.
I noticed today that I was pinged on several PRs, but GH doesn't shove those PRs in my face :sad:

In general, I'm just going to post here that if you want me to look at my PR, and it's really ready for review, then please ping me here on zulip. I think that will be a lot more effective. The github notification system seems to be a bit of a failure.
(And nope, there are too many notifications, so I'm not going to let GH spam my email inbox with them.)

Kevin Buzzard (Jul 27 2021 at 14:20):

I used to ignore github notifications because there were far too many of them, but I managed to tame things recently by switching a bunch of them off; now I only get a notification if someone explicitly pings me on a PR, and not for anything else, and this is working really well for me now.

Oliver Nash (Jul 27 2021 at 14:22):

I think #8444 (+19, -2) is ready for review.

Last updated: Dec 20 2023 at 11:08 UTC