PR queue

Stream: general

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

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]

"I wonder if there is any algebra stuff?"

[Kevin Buzzard]

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

[Johan Commelin]

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

[Bhavik Mehta]

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

[Johan Commelin]

@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]

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]

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

[Bhavik Mehta]

Looks great to me, thanks

[Johan Commelin]

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]

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

[Eric Wieser]

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]

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

[Oliver Nash]

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]

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

they are coming

[Rob Lewis]

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

[Rob Lewis]

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]

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]

This PR was in fact the motivation for my question.

[Damiano Testa]

This is really exciting!!

[Eric Wieser]

19 PRs in a single batch at the moment!

[Johan Commelin]

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

[Alex J. Best]

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

[Patrick Massot]

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]

Jesse made some cosmetic changes

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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

[Damiano Testa]

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

[Damiano Testa]

Ah, no log works: thanks, Eric!

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

[Johan Commelin]

Johan Commelin said:

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

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

[Eric Wieser]

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

[Sebastien Gouezel]

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

[Jesse Michael Han]

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]

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]

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]

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]

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