Zulip Chat Archive
Stream: std4
Topic: PR backlog
James Gallicchio (Jun 25 2023 at 20:49):
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 (Jun 26 2023 at 05:41):
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 (Jun 26 2023 at 05:42):
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 (Jun 26 2023 at 08:29):
@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 (Jun 26 2023 at 08:30):
Perhaps we review each others' PRs :) I am in the same boat as a non-mathlib user
Mario Carneiro (Jun 26 2023 at 08:33):
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 (Jun 26 2023 at 08:41):
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 (Jun 26 2023 at 08:54):
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 (Jun 26 2023 at 09:38):
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 (Jun 26 2023 at 09:44):
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 (Jun 26 2023 at 09:47):
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 (Jun 26 2023 at 09:52):
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 (Jun 27 2023 at 02:06):
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 (Jun 28 2023 at 03:31):
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 (Jun 28 2023 at 03:34):
My eyes admittedly glaze over trying to review these mathlib lemma files, but I'll give it another read myself...
James Gallicchio (Jun 28 2023 at 03:35):
(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 (Jun 28 2023 at 03:40):
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 (Jun 28 2023 at 03:44):
Yeah. It does seem like .. just a lot of theorems about countp :joy:
James Gallicchio (Jun 28 2023 at 03:45):
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 (Jun 28 2023 at 09:53):
@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 (Jun 29 2023 at 05:57):
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 (Jun 30 2023 at 01:09):
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 (Jun 30 2023 at 01:09):
will go thru the ones you pointed out!
François G. Dorais (Jul 03 2023 at 15:27):
@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 (Jul 05 2023 at 17:34):
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 (Jul 06 2023 at 17:26):
PR std4#110 is ready to merge.
François G. Dorais (Jul 07 2023 at 21:02):
PR std4#179 needs maintainer attention. It looks good to me but github workflow needs to run first.
François G. Dorais (Jul 08 2023 at 17:04):
PR std4#179 looks good to merge.
François G. Dorais (Jul 08 2023 at 17:07):
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 (Jul 08 2023 at 17:11):
PR std4#112 only needs a tiny edit.
François G. Dorais (Jul 08 2023 at 17:15):
PR std4#176 which was discussed on zulip looks good to me.
Mario Carneiro (Jul 08 2023 at 20:28):
FYI I will be travelling this week, so expect little movement on std stuff
Patrick Massot (Jul 08 2023 at 20:43):
How far are we to be able to bump mathlib to current Std?
François G. Dorais (Jul 08 2023 at 20:46):
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 (Jul 08 2023 at 21:09):
Ok, thanks.
François G. Dorais (Jul 09 2023 at 00:23):
PR std4#181 is a quick fix for issue #90
François G. Dorais (Jul 11 2023 at 00:11):
PR std4#184 simply moves the alias
tactic from Mathlib.
François G. Dorais (Jul 18 2023 at 12:19):
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 (Aug 10 2023 at 14:57):
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 (Aug 18 2023 at 07:46):
Could I ping on std4#210 std4#211 std4#212 std4#213, prerequisities for upstreaming exact?
?
Scott Morrison (Aug 21 2023 at 02:06):
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 (Aug 22 2023 at 05:39):
Could I get permission to change labels? :)
James Gallicchio (Aug 22 2023 at 06:39):
@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 (Aug 22 2023 at 06:42):
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 (Aug 22 2023 at 08:24):
@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 (Aug 22 2023 at 22:49):
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 (Aug 22 2023 at 23:47):
No, it seems to build by itself. I will agitate for someone to merge.
François G. Dorais (Aug 23 2023 at 00:00):
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 (Aug 23 2023 at 00:05):
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 (Aug 23 2023 at 00:11):
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 (Aug 24 2023 at 17:59):
May I have permission to edit labels?
François G. Dorais (Aug 24 2023 at 18:20):
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 (Aug 24 2023 at 18:22):
@Alex J. Best I added awaiting-review
for you since that seemed to be the one you needed.
Scott Morrison (Aug 24 2023 at 22:28):
If someone wants to write (or find...?) the github action!
Scott Morrison (Aug 24 2023 at 22:29):
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 (Sep 01 2023 at 08:11):
I would probably ask it to use github-script so a to avoid it committing the atrocity of parsing json with regex!
Scott Morrison (Sep 04 2023 at 23:09):
@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 (Sep 04 2023 at 23:09):
Also std4#238 is I think ready to go after your reviews yesterday (this is the left
and right
tactic upstream).
Scott Morrison (Sep 05 2023 at 02:09):
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 (Sep 05 2023 at 09:16):
(note, I'm at AITP this week so I will not be very responsive)
Scott Morrison (Sep 12 2023 at 23:34):
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 (Sep 13 2023 at 00:36):
Also on the path to exact?
: std4#213 (the DeclCache
mechanism) and std4#258 (register_label_attr
).
James Gallicchio (Sep 17 2023 at 22:02):
RE: std4#100, does someone know where all the relevant mathlib bumps are to get mathlib back up to speed?
James Gallicchio (Sep 17 2023 at 22:02):
(the bump for std4#100 seems to not compile for other-std-change reasons)
Scott Morrison (Sep 17 2023 at 23:49):
I don't think there are any significant bumps in between, @James Gallicchio.
Scott Morrison (Sep 17 2023 at 23:50):
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 (Sep 17 2023 at 23:50):
Of course you should expect to have to merge master into your Mathlib bump PR #6743, because master has moved on since.
Scott Morrison (Sep 17 2023 at 23:51):
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 (Sep 17 2023 at 23:53):
That error is just a missed rename of pwFilter_idempotent
to pwFilter_idem
.
Scott Morrison (Sep 18 2023 at 00:02):
I've pushed the fixes and :peace_sign:'d.
James Gallicchio (Sep 18 2023 at 00:05):
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 (Sep 18 2023 at 00:21):
It's essential to have gotten every step wrong yourself, before you're ready to write the bot. :-)
Scott Morrison (Sep 18 2023 at 01:34):
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 (Sep 18 2023 at 02:33):
std4#260 seems unobjectionable. broken simp lemmas should be removed even if they're not replaced immediately...
Scott Morrison (Sep 18 2023 at 04:06):
Both of these PRs have matching mathlib PRs, #7134 and #7141.
Scott Morrison (Sep 26 2023 at 23:19):
@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 (Oct 04 2023 at 00:45):
Still holding up exact?
:
Wojciech Nawrocki (Oct 05 2023 at 02:50):
Could I have PR labelling permissions? :pray:
Wojciech Nawrocki (Oct 06 2023 at 21:44):
Ping @Scott Morrison @Mario Carneiro
Alex J. Best (Oct 14 2023 at 21:16):
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 (Oct 22 2023 at 00:42):
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 (Oct 24 2023 at 05:36):
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 (Oct 24 2023 at 05:40):
Scott Morrison (Nov 01 2023 at 04:59):
I see that @François G. Dorais has recently updated his Std PRs upstreaming lemmas about Nat
:
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 (Nov 01 2023 at 14:56):
Thank you @Scott Morrison and @Mario Carneiro!
By the way, Scott, is there a patch for std4#340?
François G. Dorais (Nov 01 2023 at 15:32):
nvm, the patch is just two lines.
Scott Morrison (Nov 01 2023 at 23:37):
Where are we at with bumping Mathlib to catch up to Std? There are lots of changes to coordinate, I think.
Scott Morrison (Nov 01 2023 at 23:37):
@François G. Dorais, you said "the patch is just two line". Is this somewhere?
Scott Morrison (Nov 01 2023 at 23:40):
It looks like #8074 is the one that needs to go first?
Scott Morrison (Nov 01 2023 at 23:43):
Or do we need to do the patch for std4#340 separately first?
Scott Morrison (Nov 01 2023 at 23:50):
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
andright
for std#238 - rip out
Cache
stuff for std#213 - :peace_sign: #8106 rip out
MVarId.isIndependentOf
for std#254 @ 795918af0b01cd79aea67f828f215cca71699eca
Scott Morrison (Nov 01 2023 at 23:54):
Hopefully the last three can happen all at once.
Scott Morrison (Nov 02 2023 at 00:06):
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 (Nov 02 2023 at 00:21):
Okay, I've replaced #8005 with #8105
Scott Morrison (Nov 02 2023 at 00:35):
Okay, hopefully we are good to go here, and we will have caught up with Std after this.
François G. Dorais (Nov 02 2023 at 07:40):
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 (Nov 02 2023 at 09:44):
Okay, hopefully we are there soon!
Scott Morrison (Nov 04 2023 at 03:53):
std#259 is a requested linter PR that was perhaps forgotten
François G. Dorais (Nov 04 2023 at 23:32):
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 (Nov 04 2023 at 23:40):
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 (Nov 05 2023 at 00:08):
Ah! Noted. (I'm afraid I just did the wrong thing again :/)
François G. Dorais (Nov 05 2023 at 00:10):
Thank you Mario!
Scott Morrison (Nov 05 2023 at 01:03):
Ugh, replacing Nat.succ_eq_one_add
with \l Nat.one_add
seems like a terrible change.
Scott Morrison (Nov 05 2023 at 01:03):
Lemmas should be written with simp normal form on the RHS?
Scott Morrison (Nov 05 2023 at 01:05):
Actually, @François G. Dorais, I don't understand why you have removed uses on succ_eq_one_add
in #6203
Scott Morrison (Nov 05 2023 at 01:05):
succ_eq_one_add
is still available?
François G. Dorais (Nov 05 2023 at 01:06):
Historical reasons, it was deprecated for a bit then came back.
Scott Morrison (Nov 05 2023 at 01:07):
I see. Can we undo that in #6203?
Scott Morrison (Nov 05 2023 at 01:07):
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 (Nov 05 2023 at 01:08):
Yes, I will do in a second.
Scott Morrison (Nov 05 2023 at 01:09):
Changing eq_zero_of_nonpos
to eq_zero_of_not_pos
seems contrary to the naming conventions.
Scott Morrison (Nov 05 2023 at 01:10):
I can do the succ_eq_one_add
reverts if you prefer to address my other questions first. :-)
François G. Dorais (Nov 05 2023 at 01:11):
Apparently not, that one came from Mario: nonpos is ≤ 0
but the lemma uses ¬ 0 <
Scott Morrison (Nov 05 2023 at 01:12):
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 (Nov 05 2023 at 01:13):
I had this on another branch recently and don't understand how it is occurring.
Scott Morrison (Nov 05 2023 at 01:13):
I can transplant the fix from another branch.
Scott Morrison (Nov 05 2023 at 01:17):
Besides the query about @[simp] I'm happy with this one.
Scott Morrison (Nov 05 2023 at 01:19):
I am going to merge #6203 into #8077, so there are ready to go one after the other.
Scott Morrison (Nov 05 2023 at 01:22):
THe changes in #8077 relative to #6203 look fine.
I've #6203 and :peace_sign: #8077.
François G. Dorais (Nov 05 2023 at 01:24):
Thanks Scott!
Scott Morrison (Nov 05 2023 at 03:19):
Both of these are merged now.
Scott Morrison (Nov 05 2023 at 05:52):
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 (Nov 05 2023 at 05:54):
are you working on omega
? :star_struck:
Scott Morrison (Nov 05 2023 at 06:06):
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 (Nov 05 2023 at 06:31):
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 (Nov 05 2023 at 06:32):
https://github.com/leanprover-community/mathlib4/tree/micromega (note: it's very old)
François G. Dorais (Nov 05 2023 at 19:52):
@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 (Nov 05 2023 at 20:46):
PS: I just paid closer attention to the year... Summer 2022 wasn't the right time! I get it now.
Mario Carneiro (Nov 06 2023 at 03:09):
even before upstreaming, it first has to be written and used in mathlib
Reid Barton (Nov 06 2023 at 03:20):
I still don't understand how it's not called omicron
Scott Morrison (Nov 06 2023 at 09:08):
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 (Nov 17 2023 at 03:53):
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 (Nov 17 2023 at 14:54):
std4#354 would be a nice usability improvement for mathlib, and seems to have reasonable buy-in
James Gallicchio (Nov 19 2023 at 09:20):
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 (Nov 19 2023 at 10:37):
Three easy PRs for Std:
- std4#291, some
@[simp]
attributes forInt
- 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 (Nov 19 2023 at 10:38):
(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 (Nov 19 2023 at 10:49):
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 (Nov 19 2023 at 10:52):
Oops, main
is broken. https://github.com/leanprover/std4/pull/375
Scott Morrison (Nov 19 2023 at 10:58):
Ok, std4#372 is good to go again.
Scott Morrison (Nov 19 2023 at 11:15):
@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 (Nov 19 2023 at 11:17):
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 (Nov 19 2023 at 11:18):
SGTM
Mario Carneiro (Nov 19 2023 at 11:18):
I don't think byKey
is used outside of Std, so I don't anticipate any breakage
Scott Morrison (Nov 19 2023 at 11:22):
std4#377 looks good to go.
Scott Morrison (Nov 20 2023 at 04:02):
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 (Nov 20 2023 at 23:47):
@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 (Nov 21 2023 at 12:06):
All done, waiting on some CI. Incidentally, I had to make the Mathlib bump to the current Std: #8548
Scott Morrison (Nov 21 2023 at 12:27):
Thanks.
James Gallicchio (Nov 22 2023 at 00:53):
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 (Nov 23 2023 at 05:06):
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 (Nov 23 2023 at 05:08):
The tactic mode proofs are a bit more readable, but I don't mind short term-mode proofs.
François G. Dorais (Nov 23 2023 at 07:38):
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 (Nov 23 2023 at 08:02):
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 (Nov 23 2023 at 12:51):
I just clarified the review comments...
Mario Carneiro (Nov 23 2023 at 16:21):
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 (Nov 23 2023 at 16:26):
(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 (Nov 23 2023 at 17:06):
Got it, will push those changes real quick
François G. Dorais (Nov 26 2023 at 21:33):
@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 (Nov 26 2023 at 21:42):
Thanks Mario!
François G. Dorais (Nov 27 2023 at 21:47):
Does CI need to be re-enabled every time until they get a merged PR? @Mario Carneiro @Joe Hendrix
Mario Carneiro (Nov 27 2023 at 21:47):
yes
Mario Carneiro (Nov 27 2023 at 21:47):
nothing I can do about that unfortunately
François G. Dorais (Nov 27 2023 at 21:48):
bummer :/
François G. Dorais (Nov 27 2023 at 21:59):
Thanks again!
Eric Wieser (Nov 27 2023 at 22:46):
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 (Nov 28 2023 at 00:06):
@Mario Carneiro if you could speed through std4#405 then that would resolve this recurring problem.
Joe Hendrix (Nov 28 2023 at 00:21):
It's merged
François G. Dorais (Dec 03 2023 at 05:59):
We got a couple of PRs from new contributors who need CI authorization: std4#417, std4#412
François G. Dorais (Dec 08 2023 at 04:47):
std4#197 (Nat add lemmas) got forgotten somehow. It's ready to merge.
Joe Hendrix (Dec 08 2023 at 05:24):
Thanks for persisting!
Last updated: Dec 20 2023 at 11:08 UTC