## 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:
https://github.com/leanprover-community/mathlib/issues?q=is%3Aopen+label%3Aawaiting-review+sort%3Aupdated-asc+-label%3Ablocked-by-other-PR+-label%3Amerge-conflict

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?

#### 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:

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)

Last updated: May 16 2021 at 05:21 UTC