PR backlog

Stream: std4

[James Gallicchio]

I was gonna start making more PRs to move useful definitions from mathlib to standard, but it seems like there's a pretty big PR backlog -- is there any way to help with reviewing PRs before I start adding to the backlog @Mario Carneiro?

[Mario Carneiro]

Certainly adding your voice to existing PRs, pointing out that a PR is blocking this or that, or reviewing will all help with this. I would love to get some mathlib maintainers involved in std as well.

[Mario Carneiro]

I don't think you should use the backlog as a reason not to add more PRs, unless you are building a string of dependent PRs and don't want to go too far in a certain direction without affirmation

[François G. Dorais]

@Mario Carneiro Keep in mind that some PRs are unrelated to mathlib! (Since I rarely ever need to use mathlib, this is 100% the case for my PRs!) How should I motivate reviews? All of my projects depend on std and none depend on mathlib...

Right now I use my own libraries (which were mostly written before std4 existed) but I eventually want to get rid of most of that since it's pointless to duplicate the work.

[James Gallicchio]

Perhaps we review each others' PRs :) I am in the same boat as a non-mathlib user

[Mario Carneiro]

I don't think I said that PRs are related to mathlib, I mean that mathlib maintainers might also get involved in std maintenance as well

[François G. Dorais]

But that doesn't answer the main question: how can I (and James and others) motivate PR reviews? Almost nothing gets through unless it's mathlib related!

[François G. Dorais]

I just noticed that I am now able to review PRs on Std4. I'm assuming I have to thank Mario? Thank you very much!

[Mario Carneiro]

François G. Dorais said:

But that doesn't answer the main question: how can I (and James and others) motivate PR reviews? Almost nothing gets through unless it's mathlib related!

I like to have second opinions on new design stuff, and if it's just me it's hard to get second opinions about things. Mathlib has a leg up here because it has been through one review process and people have given their opinions already, but I don't think I am explicitly selecting for mathlib-sourced PRs.

[François G. Dorais]

I didn't mean to sound harsh, sorry! I know you have been doing the best you could. I promise to help a lot more in July. (And whenever I can otherwise but I do have a day job :sad:)

[Mario Carneiro]

I think the biggest thing here is that I really don't have much time to spend on std reviews. Keep poking me if it looks like it's just waiting for merge, but if it's waiting on design review open a topic here and get people to agree it's a good idea

[François G. Dorais]

Sounds good! First ping: PR#96 is ready to merge.

PS: I'll be very busy this week but I will be back in July.

[Scott Morrison]

Could I request a review of https://github.com/leanprover/std4/pull/129? There's now a second place I'd like to have this functionality. :-)

[James Gallicchio]

Trying to get everything up to List.Perm merged this week -- std4#99 is next in the chain and should be good for review/merge if anyone has some time.

[James Gallicchio]

My eyes admittedly glaze over trying to review these mathlib lemma files, but I'll give it another read myself...

[James Gallicchio]

(And as Mario has said, mathlib's content has been through development cycles already, so maybe these reviews don't have to be in-depth :P)

[Mario Carneiro]

Actually last time I read std4#99 I started refactoring and petered out after I couldn't get it done in one sitting. Perhaps it was a bit too big to chew off at once...

[James Gallicchio]

Yeah. It does seem like .. just a lot of theorems about countp :joy:

[James Gallicchio]

almost certainly more than we need for std4#100, but it felt weird to cherrypick since I don't really know what else downstream might be pulled into Std

[François G. Dorais]

@James Gallicchio The main issue I saw as a glance are some debatable simps. I think Std should be conservative with simps to allow users to tailor their own simp NF.

I don't have a neatly packaged example of this, but there are a few instances where I wanted to locally reverse some simps for one file... the bottom line was that it's easier to add simps than to remove them.

[Bulhwi Cha]

std4#151 golfs proofs in Data.String.Lemmas. @Mario Carneiro, can you take a quick look at this PR and merge it? (Edit: it's now merged! Thanks.)

[James Gallicchio]

François G. Dorais said:

James Gallicchio The main issue I saw as a glance are some debatable simps. I think Std should be conservative with simps to allow users to tailor their own simp NF.

I don't have a neatly packaged example of this, but there are a few instances where I wanted to locally reverse some simps for one file... the bottom line was that it's easier to add simps than to remove them.

Yeah, I should check how often they are being used in mathlib

[James Gallicchio]

will go thru the ones you pointed out!

[François G. Dorais]

@Mario Carneiro std4#174 is a first step in cleaning up Nat lemmas. I just reorganized everything into sections. I did not change any of the lemmas. The purpose is to make actual cleanup easier later on.

[François G. Dorais]

I did a bunch of golfing and cleaning of Nat lemmas in std4#177. There's no rush but if anyone has spare time to review, please go ahead!

[François G. Dorais]

PR std4#110 is ready to merge.

[François G. Dorais]

PR std4#179 needs maintainer attention. It looks good to me but github workflow needs to run first.

[François G. Dorais]

PR std4#179 looks good to merge.

[François G. Dorais]

My PR std4#178 (KMP Matching) which now includes @James Gallicchio PR std4#172 (S[ubs]tring.{posOf,contains}S[ubs]tr) is ready for review.

[François G. Dorais]

PR std4#112 only needs a tiny edit.

[François G. Dorais]

PR std4#176 which was discussed on zulip looks good to me.

[Mario Carneiro]

FYI I will be travelling this week, so expect little movement on std stuff

[Patrick Massot]

How far are we to be able to bump mathlib to current Std?

[François G. Dorais]

I think the blockage is now on the Mathlib end: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/std4.20.2F.20Lean4.20bump/near/373469912

[Patrick Massot]

Ok, thanks.

[François G. Dorais]

PR std4#181 is a quick fix for issue #90

[François G. Dorais]

PR std4#184 simply moves the alias tactic from Mathlib.

[François G. Dorais]

Ping @Mario Carneiro: Here are some PRs in the queue that can be merged with little effort when you have a chance.

std4#112 is ready as is.
std4#125 is ready with a few edits. (awaiting-author)
std4#176 is ready as is.
std4#179 is ready as is.
std4#184 is ready, it just moves alias from Mathlib verbatim. (superseded by std4#200)
std4#185 is ready as is. (awaiting-author)

[François G. Dorais]

Update @Mario Carneiro:

std4#112 is ready to merge.
std4#125 could use awaiting-author tag.

I don't like pressing for my own PRs but std4#200 and std4#193 are high priority for my projects.

[Scott Morrison]

Could I ping on std4#210 std4#211 std4#212 std4#213, prerequisities for upstreaming exact??

[Scott Morrison]

Okay, minor milestone: every PR to std4 has at least one label. :-) Ideally everyone will ensure that their own PRs always have exactly one of awaiting-review / awaiting-author / WIP, and this is up-to-date. If you don't have permission to change labels you'll need to ask here.

[James Gallicchio]

Could I get permission to change labels? :)

[James Gallicchio]

@Scott Morrison RE the chain of list file upstreams, I think I'm not gonna update the later PRs until they're at the head of the stack (it doesn't take me long to rebase the PR and get stuff compiling, but is a decent amount of manual work that I have to redo every time the dependent PR changes). I'm marking the dependent PRs as drafts for now!

[James Gallicchio]

Maybe we try to get std4#99 merged in the next day or two? We can always do further refactors once it's in Std :)

[Scott Morrison]

@James Gallicchio, I've incorporated your changes from #6575 into the larger Std bump at #6721. I doubt it builds yet.

[François G. Dorais]

It should build after incorporating #6172. This is the issue that I mentioned before where Std patches to Mathlib often need to be merged in the same order they were merged into Std. That's an annoying issue that needs a better solution. Unfortunately, I do not have an easy solution.

[Scott Morrison]

No, it seems to build by itself. I will agitate for someone to merge.

[François G. Dorais]

It builds on top of 61a6507... but that doesn't actually include std4#99 which is at d9c3146... so it sounds like you're just testing an old branch.

[Scott Morrison]

Sorry, @François G. Dorais, I don't understand your comment. #6721 has a green tick, and is using b5f7bd40d2162fe148e585543f284a5d8cc0ef26 from Std4, which is exactly main.

[François G. Dorais]

Sorry, my bad. It's shocking though. I guess the old Mathlib alias completely shadows the new alias in Std. That is really lucky!

[Alex J. Best]

May I have permission to edit labels?

[François G. Dorais]

I think @Adrien Champion also needs that.

Is there a way to add that permission to everyone after their first accepted PR? That way it would work as intended even if they didn't encounter the need to ask.

[François G. Dorais]

@Alex J. Best I added awaiting-review for you since that seemed to be the one you needed.

[Scott Morrison]

If someone wants to write (or find...?) the github action!

[Scott Morrison]

I couldn't resist: GPT claims to be able to write this action. I only looked for 30 seconds, but it doesn't seem obviously insane. :-)

[Eric Wieser]

I would probably ask it to use github-script so a to avoid it committing the atrocity of parsing json with regex!

[Scott Morrison]

@Mario Carneiro, could we please review and/or merge std4#210 and std4#213, which have been open for almost a month, and are steps towards upstreaming exact?.

[Scott Morrison]

Also std4#238 is I think ready to go after your reviews yesterday (this is the left and right tactic upstream).

[Scott Morrison]

PRs belonging to others that I think should be merged when possible: std4#237 std4#183 std4#100 std4#194 std4#195 std4#196 std4#197 std4#203

[Mario Carneiro]

(note, I'm at AITP this week so I will not be very responsive)

[Scott Morrison]

Most useful to me in the near future would be review of std4#244 (upstream of symm tactic) and std4#254 (upstream of MVarId.isIndependentOf).

(These are both on the path to exact?.)

[Scott Morrison]

Also on the path to exact?: std4#213 (the DeclCache mechanism) and std4#258 (register_label_attr).

[James Gallicchio]

RE: std4#100, does someone know where all the relevant mathlib bumps are to get mathlib back up to speed?

[James Gallicchio]

(the bump for std4#100 seems to not compile for other-std-change reasons)

[Scott Morrison]

I don't think there are any significant bumps in between, @James Gallicchio.

[Scott Morrison]

mathlib master already uses 80089ff4cd1808ad1506a62dac557517d9b875ff of Std, and after that there are two minor changes that shouldn't matter, and then your std4#100.

[Scott Morrison]

Of course you should expect to have to merge master into your Mathlib bump PR #6743, because master has moved on since.

[Scott Morrison]

I'm doing that locally, and so far the only error I've seen is

./././Mathlib/Data/List/Pairwise.lean:209:33: error: Declaration List.pwFilter_idempotent not found.

which sounds like it is #6743's responsibility.

[Scott Morrison]

That error is just a missed rename of pwFilter_idempotent to pwFilter_idem.

[Scott Morrison]

I've pushed the fixes and :peace_sign:'d.

[James Gallicchio]

Scott Morrison said:

Of course you should expect to have to merge master into your Mathlib bump PR #6743, because master has moved on since.

:man_facepalming: I forgot step 2 of how to be a bump bot

[Scott Morrison]

It's essential to have gotten every step wrong yourself, before you're ready to write the bot. :-)

[Scott Morrison]

I would like to have std4#260 and std4#261 reviewed and merged. I am maintaining a branch of Mathlib that relies on both, making it essentially impossible for me to also keep up with master.

[James Gallicchio]

std4#260 seems unobjectionable. broken simp lemmas should be removed even if they're not replaced immediately...

[Scott Morrison]

Both of these PRs have matching mathlib PRs, #7134 and #7141.

[Scott Morrison]

@Mario Carneiro, would you be able to take another look at std4#260? It is a moderately impactful PR on mathlib, as it changes the simp set substantially. There is a matching mathlib PR #7134.

[Scott Morrison]

Still holding up exact?:

• std4#244 (symm)
• std4#254 (MVarId.isIndependentOf)
• std4#213 (DeclCache)

[Wojciech Nawrocki]

Could I have PR labelling permissions? :pray:

[Wojciech Nawrocki]

Ping @Scott Morrison @Mario Carneiro

[Alex J. Best]

Can I bmup https://github.com/leanprover/std4/pull/268 ? It's not especially important of course but it already approved once so hopefully not too hard to review

[François G. Dorais]

I submitted std4#194 (Nat order lemmas) and std4#196 (Nat min/max lemmas) this summer since I expected I would need those this fall... Well, now I need them for real!

I just fixed recent issues with std4#196 that @Mario Carneiro pointed out (thanks!). I think that one is fine now but it needs further review.

As for std4#194, there are still issues because there are so many synonyms! I purposefully did not choose one over any other and I tried to collect them together in one spot. I also used the alias command to emphasize the fact that these are synonyms. There's a lot of potential debate here. I'm hoping we can get this version with all variants merged in and then deprecate some variants in later updates but I understand if the community prefers a different path.

[Scott Morrison]

I've just revived #210 and #254, which had recently acquired conflicts. #254 is blocking progress on upstreaming exact? (and has been doing so for more than a month now :-)

[Mario Carneiro]

(std#210, std#254)

[Scott Morrison]

I see that @François G. Dorais has recently updated his Std PRs upstreaming lemmas about Nat:

• std#194
• std#196
• std#203
• std#195
• std#198

As they have simultaneously revived the matching Mathlib PRs, now might be an opportune moment to get these reviewed and in, as keeping Mathlib up to date will be easier until these rot again.

[François G. Dorais]

Thank you @Scott Morrison and @Mario Carneiro!

By the way, Scott, is there a patch for std4#340?

[François G. Dorais]

nvm, the patch is just two lines.

[Scott Morrison]

Where are we at with bumping Mathlib to catch up to Std? There are lots of changes to coordinate, I think.

[Scott Morrison]

@François G. Dorais, you said "the patch is just two line". Is this somewhere?

[Scott Morrison]

It looks like #8074 is the one that needs to go first?

[Scott Morrison]

Or do we need to do the patch for std4#340 separately first?

[Scott Morrison]

Okay's here my plan for catching up (I'll edit this message in place):

• #8104 for std4#340 @ 123e2f1e31355f79b95396b2d83de61bd9b485e7
• #8074 for std4#196 @ b541ac2085f0970ef3d3a2d44daba50e34488aab
• :peace_sign: #8105 for std#329 @ fb43b83c13d10b90299d10d96512d20d33daa658
• nothing required? for std#328
• nothing required? for std#325
• rip out left and right for std#238
• rip out Cache stuff for std#213
• :peace_sign: #8106 rip out MVarId.isIndependentOf for std#254 @ 795918af0b01cd79aea67f828f215cca71699eca

[Scott Morrison]

Hopefully the last three can happen all at once.

[Scott Morrison]

There is #8005 for std#329, but it seems to be completely borked and I can't make head or tail of it. I think I will try starting over for that step?

[Scott Morrison]

Okay, I've replaced #8005 with #8105

[Scott Morrison]

Okay, hopefully we are good to go here, and we will have caught up with Std after this.

[François G. Dorais]

Thanks for fixing #8005, I got busy with other things and had to leave it incomplete. #8105 looks good to me! I'll be busy for the next couple of days but I'm always happy to help!

[Scott Morrison]

Okay, hopefully we are there soon!

[Scott Morrison]

std#259 is a requested linter PR that was perhaps forgotten

[François G. Dorais]

I just refreshed std4#194 (order lemmas for Nat) and std4#195 (succ/pred lemmas for Nat) along with their Mathlib patches. Both were approved by @Mario Carneiro a few days ago. Now would be a great time to merge them especially since std4#194 tends to break quickly.

[Mario Carneiro]

note for the future: use merge, not rebase, if you are making changes to a PR that has already been reviewed. Otherwise it is difficult to review the changes that happened since the last review

[François G. Dorais]

Ah! Noted. (I'm afraid I just did the wrong thing again :/)

[François G. Dorais]

Thank you Mario!

[Scott Morrison]

Ugh, replacing Nat.succ_eq_one_add with \l Nat.one_add seems like a terrible change.

[Scott Morrison]

Lemmas should be written with simp normal form on the RHS?

[Scott Morrison]

Actually, @François G. Dorais, I don't understand why you have removed uses on succ_eq_one_add in #6203

[Scott Morrison]

succ_eq_one_add is still available?

[François G. Dorais]

Historical reasons, it was deprecated for a bit then came back.

[Scott Morrison]

I see. Can we undo that in #6203?

[Scott Morrison]

I would like to merge the mathlib PRs asap, so they don't rot and we can stay close to Std's main branch.

[François G. Dorais]

Yes, I will do in a second.

[Scott Morrison]

Changing eq_zero_of_nonpos to eq_zero_of_not_pos seems contrary to the naming conventions.

[Scott Morrison]

I can do the succ_eq_one_add reverts if you prefer to address my other questions first. :-)

[François G. Dorais]

Apparently not, that one came from Mario: nonpos is ≤ 0 but the lemma uses ¬ 0 <

[Scott Morrison]

Are you seeing:

./././Mathlib/Util/DischargerAsTactic.lean:15:20: error: unknown namespace 'Tactic'
./././Mathlib/Util/DischargerAsTactic.lean:20:30: error: unknown identifier 'Simp.Discharge'
./././Mathlib/Util/DischargerAsTactic.lean:20:48: error: unknown identifier 'TacticM'

on #6203?

[Scott Morrison]

I had this on another branch recently and don't understand how it is occurring.

[Scott Morrison]

I can transplant the fix from another branch.

[Scott Morrison]

Besides the query about @[simp] I'm happy with this one.

[Scott Morrison]

I am going to merge #6203 into #8077, so there are ready to go one after the other.

[Scott Morrison]

THe changes in #8077 relative to #6203 look fine.

I've #6203 and :peace_sign: #8077.

[François G. Dorais]

Thanks Scott!

[Scott Morrison]

Both of these are merged now.

[Scott Morrison]

Here are my Std PRs that I would like to see reviewed soon, mostly because I want them for omega:

• [ ] std4#351 upstream norm_cast
• [ ] std4#347 upstream @[simps] attribute
• [ ] std4#345 upstream change at tactic
• [ ] std4#324 lemmas about if-then-else
• [ ] std4#293 lemmas about List.findIdx?
• [ ] std4#291 simp lemmas about Int

[Mario Carneiro]

are you working on omega? :star_struck:

[Scott Morrison]

Getting there. I have a basic version working over Int (no "dark" and "grey" shadows yet, so only a semidecision procedure), but it needs lots of speedups. I'm going to build more of the Nat preprocessing frontend next, so it's usable, and then go back to completeness/optimization.

[Mario Carneiro]

I was kind of hoping someone would pick up my micromega port (which despite the name is quite a comprehensive suite of tactics and more complete than the lean 3 omega tactic)

[Mario Carneiro]

https://github.com/leanprover-community/mathlib4/tree/micromega (note: it's very old)

[François G. Dorais]

@Mario Carneiro At a quick glance, mircomega looks like a good fit for Std. It's light weight and powerful. Why did you drop it?

[François G. Dorais]

PS: I just paid closer attention to the year... Summer 2022 wasn't the right time! I get it now.

[Mario Carneiro]

even before upstreaming, it first has to be written and used in mathlib

[Reid Barton]

I still don't understand how it's not called omicron

[Scott Morrison]

std4#351 and then #8122 (upstreaming norm_cast to Std) would be very useful for me, as I'll be depending on these branches in the interim.

[Scott Morrison]

std4#368 and std4#369 are easy bug fixes / improvements, that each have a mathlib PR waiting for them that improves the behaviour of exact?.

[Eric Wieser]

std4#354 would be a nice usability improvement for mathlib, and seems to have reasonable buy-in

[James Gallicchio]

I finally did a careful read through of std4#89 and left some comments/work for myself. @Mario Carneiro @Wojciech Nawrocki if you have some time to look over the comments I'd appreciate bikeshedding input on lemma names and statements.

[Scott Morrison]

Three easy PRs for Std:

• std4#291, some @[simp] attributes for Int
• std4#369, making DiscrTreeCache.mk more flexible by deferring an opinionated filter to the caller
• std4#372, some basic lemmas about LT and LE.

[Scott Morrison]

(There are many others in my open backlog that I'd like to see merged, but those three should require very little effort!)

[Mario Carneiro]

two down, but the remaining one is more than a 20 second job, looks like something broke in DivMod when reverting the alias import

[Scott Morrison]

Oops, main is broken. https://github.com/leanprover/std4/pull/375

[Scott Morrison]

Ok, std4#372 is good to go again.

[Scott Morrison]

@Mario Carneiro, oh, I missed something in std4#372. The Std namespace was opened at the top of the file, so the le_of_le_of_eq lemmas I added are in the Std namespace instead of _root_ as I intended.

Presumably it is okay to change this quickly?

[Scott Morrison]

Hmm, actually my take is that most of the file is right, but byKey should be Ordering.byKey rather than Std.byKey, and then the new theorems should be in _root_.

[Mario Carneiro]

SGTM

[Mario Carneiro]

I don't think byKey is used outside of Std, so I don't anticipate any breakage

[Scott Morrison]

std4#377 looks good to go.

[Scott Morrison]

The awaiting-review + has an approving review list has 8 items on it: https://github.com/leanprover/std4/pulls?q=is%3Apr+is%3Aopen+label%3Aawaiting-review+review%3Aapproved+-label%3Amerge-conflict

Perhaps this would be a good place to start to clear the backlog?

(Only one is mine! :-)

[François G. Dorais]

@Scott Morrison @Mario Carneiro I have time to refresh and finalize std4#197 (Nat add) and std4#203 (Nat sub) and Mathlib patches tomorrow. Is this a good time? (I'm flexible.)

[François G. Dorais]

All done, waiting on some CI. Incidentally, I had to make the Mathlib bump to the current Std: #8548

[Scott Morrison]

Thanks.

[James Gallicchio]

std4#89 is good for review; I'll make a mathlib patch tonight or tomorrow, since this one is going to be messy

[James Gallicchio]

RE: @François G. Dorais' review of std4#89 is there any stylistic or maintenance preference between term-mode and tactic-mode proofs in Std? The suggested proof changes are essentially tactic mode translations of the current term mode proofs.

[James Gallicchio]

The tactic mode proofs are a bit more readable, but I don't mind short term-mode proofs.

[François G. Dorais]

I like short term-mode proofs. I'm sure there is no style preference for tactic-mode proofs in general. The suggestions are made are all about using the induction tactic instead of using Perm.rec directly. The goal there is readability since recursors are not generally meant for human consumption.

[François G. Dorais]

Bulleted arguments would also work well here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Fun.20macro.20-.20bulleted.20argument.20lists

Maybe that should be included in Std?

[François G. Dorais]

I just clarified the review comments...

[Mario Carneiro]

the only reason they were written with recursors in the first place was because lean 3 induction did not work in that position. I think we should have a style rule saying don't use T.rec if there are any other options which are not significantly worse on other axes

[Mario Carneiro]

(I believe this rule is currently followed in std, in the sense that you will not find any direct references to T.rec theorems, except for some use of Or.rec and And.rec in some golfed Std.Logic proofs)

[James Gallicchio]

Got it, will push those changes real quick

[François G. Dorais]

@Mario Carneiro @Joe Hendrix could either one of you enable CI on PR std4#394. I think that would really help this first-time contributor.

[François G. Dorais]

Thanks Mario!

[François G. Dorais]

Does CI need to be re-enabled every time until they get a merged PR? @Mario Carneiro @Joe Hendrix

[Mario Carneiro]

yes

[Mario Carneiro]

nothing I can do about that unfortunately

[François G. Dorais]

bummer :/

[François G. Dorais]

Thanks again!

[Eric Wieser]

Mario Carneiro said:

nothing I can do about that unfortunately

You could recommend they open a trivial documentation PR fixing a typo somewhere; as soon as the first PR is merged, this behavior goes away

[François G. Dorais]

@Mario Carneiro if you could speed through std4#405 then that would resolve this recurring problem.

[Joe Hendrix]

It's merged

[François G. Dorais]

We got a couple of PRs from new contributors who need CI authorization: std4#417, std4#412

[François G. Dorais]

std4#197 (Nat add lemmas) got forgotten somehow. It's ready to merge.

[Joe Hendrix]

Thanks for persisting!