Zulip Chat Archive

Stream: mathlib4

Topic: New PRs


Reid Barton (Dec 12 2022 at 08:55):

I'm curious what the status or plan is for PRs to mathlib4 with brand-new content, since the possibility of such doesn't seem that far away.

Yaël Dillies (Dec 12 2022 at 08:56):

I assume we'll ask them to be backported?

Johan Commelin (Dec 12 2022 at 08:57):

I guess brand new content in brand new files isn't much of an issue. But when it's touching existing files (which is very likely) then I think it might cause some headaches.

Reid Barton (Dec 12 2022 at 08:59):

So what you're saying is that even mathlib PRs will now have a for_mathlib directory.

Reid Barton (Dec 12 2022 at 12:35):

Johan and I discussed it a bit and we don't really see any harm in accepting mathlib4 PRs, so long as they don't break backwards compatibility. That is, all of the not-yet-ported files of mathlib 3 are conceptually "clients" of the already-ported files, and we can't break them.

In practice this means that adding new files and likely also new definitions, lemmas etc. is fine but e.g. rearranging imports or changing existing definitions is probably not fine.

Eric Wieser (Dec 12 2022 at 13:06):

I think even adding new definitions to existing files is a bad idea; it makes it much harder to ask "are these files in sync" programatically

Eric Wieser (Dec 12 2022 at 13:07):

Maybe the solution is an #alignnew command to match #align and #noalign, indicating "this is new in mathlib4"

Reid Barton (Dec 12 2022 at 14:32):

Eric Wieser said:

I think even adding new definitions to existing files is a bad idea; it makes it much harder to ask "are these files in sync" programatically

I think the claim is that you don't really need to ask this--all you need to know is "is this mathlib 4 file newer than a given mathlib 3 file"

Eric Wieser (Dec 12 2022 at 14:37):

That doesn't tell you if the mathlib3 file has grown changes not present in mathlib4

Reid Barton (Dec 12 2022 at 16:31):

Ah sorry, what I meant to say was "newer than a given version of a mathlib 3 file"

Reid Barton (Dec 12 2022 at 16:32):

So as long as you have some knowledge of "mathlib 4 file X' contains all of mathlib 3 file X as of commit S", you can detect when new contents in mathlib 3 need to be ported to mathlib 4, while also allowing additions to the mathlib 4 file.

Rémi Bottinelli (Dec 13 2022 at 09:49):

Reid Barton said:

Johan and I discussed it a bit and we don't really see any harm in accepting mathlib4 PRs, so long as they don't break backwards compatibility. That is, all of the not-yet-ported files of mathlib 3 are conceptually "clients" of the already-ported files, and we can't break them.

In practice this means that adding new files and likely also new definitions, lemmas etc. is fine but e.g. rearranging imports or changing existing definitions is probably not fine.

I'm working (with @Antoine Labelle ) on a few PRs only dealing with quivers, which are already almost entirely ported to Mathlib4.
Does it make sense, then, to simply forget about mathlib3 and directly do the PRs for Mathlib4 ? That would be way easier than having to deal with synchronized PRs each time.

Kevin Buzzard (Dec 13 2022 at 09:59):

I think that right now we're trying to keep mathlib3 and mathlib4 in sync, although there are discussions about how to let them diverge.

Scott Morrison (Dec 13 2022 at 10:01):

I wouldn't bet on those discussions concluding real-soon-now, however. It sounds pretty scary to start diverging already.

Scott Morrison (Dec 13 2022 at 10:01):

If you're just adding new files, not touching any files that have matching partners in mathlib3, then I'd guess everyone will be on board with that.

Yaël Dillies (Dec 13 2022 at 10:02):

... until someone who is working on mathlib wants them :upside_down:

Yaël Dillies (Dec 13 2022 at 10:03):

mathport doesn't do Lean 4 -> Lean 3 translation, does it?

Patrick Massot (Dec 13 2022 at 10:03):

Scott Morrison said:

If you're just adding new files, not touching any files that have matching partners in mathlib3, then I'd guess everyone will be on board with that.

In principle this is true, but I expect this would be very frustrating very soon because when writing new files you always want to add a couple of lemmas in an older file. If those are put in the new file in mathlib4 then we'll simply accumulate mess for no good reason.

Mario Carneiro (Dec 13 2022 at 10:04):

Yaël Dillies said:

mathport doesn't do Lean 4 -> Lean 3 translation, does it?

Nope, that's totally out of scope and not what we want to encourage in any case. We can and will use new lean 4 material as an extra carrot to move people across :)

Mario Carneiro (Dec 13 2022 at 10:06):

I think we should allow new theorems to be added to aligned mathlib4 files. As long as you don't reorder the aligned theorems, I don't think this poses any major issues for mathport. It currently isn't even really making use of mathlib4 theorem placement, as long as everything is defined and #aligned some time before Mathlib.lean

Mario Carneiro (Dec 13 2022 at 10:08):

which is also what Reid said above

Yaël Dillies (Dec 13 2022 at 10:10):

This sounds like a headache when other people add similar lemmas to mathlib and want to port them over.

Mario Carneiro (Dec 13 2022 at 10:11):

Why?

Yaël Dillies (Dec 13 2022 at 10:11):

Because we'll have to refactor either mathlib or mathlib4 to account for material coming from the other side.

Mario Carneiro (Dec 13 2022 at 10:12):

the #align statements are the landmarks, just find the ones for the mathlib3 theorems before and after

Yaël Dillies (Dec 13 2022 at 10:12):

Yes, I'm saying similar lemmas, not identical lemmas.

Mario Carneiro (Dec 13 2022 at 10:12):

a synced mathlib4 file has #align statements for every statement in the mathlib3 file, in the same order

Mario Carneiro (Dec 13 2022 at 10:13):

there may also be additional declarations and theorems which have no align statements in between

Mario Carneiro (Dec 13 2022 at 10:13):

if there are similar lemmas in mathlib3 with no mathlib4 equivalents then the file isn't aligned

Reid Barton (Dec 13 2022 at 10:14):

Yaël Dillies said:

This sounds like a headache when other people add similar lemmas to mathlib and want to port them over.

If someone is adding lemmas to mathlib files that have been ported to mathlib4 then there is already a headache

Yaël Dillies (Dec 13 2022 at 10:14):

Yes, but there's no decision to be made while porting. The mathlib file has authority on what the mathlib4 file contains.

Mario Carneiro (Dec 13 2022 at 10:15):

no, the mathlib4 file must be a superset of the mathlib3 file

Yaël Dillies (Dec 13 2022 at 10:15):

Right now, whenever mathlib and mathlib4 diverge, mathlib has the last word and at worse we just report everything later. What you want to do is allow the mathlib4 to have a say.

Reid Barton (Dec 13 2022 at 10:16):

Basically what I mean is in the situation you're describing, it is up to whoever wants to edit mathlib3 to make corresponding changes to mathlib4 appropriately

Yaël Dillies (Dec 13 2022 at 10:16):

Yes, that I agree, but letting mathlib4 diverge means that the "corresponding changes to mathlib4" is not just porting anymore.

Reid Barton (Dec 13 2022 at 10:17):

Sure, and that might be tricky to deal with for whoever wants to edit the mathlib3 file

Mario Carneiro (Dec 13 2022 at 10:17):

I don't know what you mean by mathlib4 diverging here

Mario Carneiro (Dec 13 2022 at 10:17):

I suspect that we already have procedures for whatever it is

Yaël Dillies (Dec 13 2022 at 10:17):

"having a different set of lemmas/definitions"

Mario Carneiro (Dec 13 2022 at 10:17):

that's what #align is for

Mario Carneiro (Dec 13 2022 at 10:18):

you will get a message in mathport if the alignment isn't a defeq match

Mario Carneiro (Dec 13 2022 at 10:18):

and there are a few options for how to proceed

Mario Carneiro (Dec 13 2022 at 10:20):

you can do the alignment anyway, but this will make some statements fail to typecheck, or you can align with \_x which causes the mathport output to pretend it did the alignment without actually doing so in its internal state (this is best for when the alignment is not defeq but the elaborator will make up the difference); or you can align with ' or some other name when it's genuinely a different definition

Yaël Dillies (Dec 13 2022 at 10:20):

That's what I call "headache" now :laughing:

Mario Carneiro (Dec 13 2022 at 10:21):

Sure, which is why we also have the option of doing something in mathlib to make them defeq match

Reid Barton (Dec 13 2022 at 10:22):

In any case, we can't be indiscriminately modifying already-ported files in mathlib3 as though the port doesn't exist. That's going to make the port impractical, regardless of whether mathlib4 has additional stuff that didn't come from mathlib3.

Mario Carneiro (Dec 13 2022 at 10:22):

but in any case the end result should be that #aligns are more or less an exact match to mathlib3

Yaël Dillies (Dec 13 2022 at 10:23):

Reid Barton said:

In any case, we can't be indiscriminately modifying already-ported files in mathlib3 as though the port doesn't exist.

That's what I've been doing, in fact. It's extra work, but straightforward extra work.

Reid Barton (Dec 13 2022 at 10:29):

What do you mean? What is the extra work, and who is doing it?

Eric Wieser (Dec 13 2022 at 10:30):

In this case the extra work is creating the mathlib4 update PRs, and @Yaël Dillies has been doing those themselves.

Yaël Dillies (Dec 13 2022 at 10:31):

The extra work is

  • open a mathlib4 gitpod
  • wait 5 min for it to download Lean, mathlib4
  • replicate the mathlib changes
  • open the PR

Reid Barton (Dec 13 2022 at 10:31):

OK so then I wouldn't really describe this as "as though the port doesn't exist".

Yaël Dillies (Dec 13 2022 at 10:31):

Takes a good 20min every time, because mathlib4 CI isn't great, still.

Mario Carneiro (Dec 13 2022 at 10:32):

well if you didn't start from scratch every time it would be faster

Yaël Dillies (Dec 13 2022 at 10:33):

Well, if the Lean4 install was persistent, I wouldn't start from scratch every time!

Scott Morrison (Dec 13 2022 at 10:33):

Do we need to make a new image for gitpod, for mathlib4?

Yaël Dillies (Dec 13 2022 at 10:33):

I assume this is the solution, yeah.

Scott Morrison (Dec 13 2022 at 10:33):

Hopefully just copying the setup we have for mathlib over should be an easy start.

Yaël Dillies (Dec 13 2022 at 10:34):

Reid Barton said:

OK so then I wouldn't really describe this as "as though the port doesn't exist".

What I mean is that typically I'm not changing my PRs because of the port. Eric in #17895 was adding to a non-ported file a lemma that belonged to an already ported one. So I took it onto myself to move it to the correct spot and open the mathlib4 PR.

Yaël Dillies (Dec 13 2022 at 10:35):

Mario, if I stop and start the mathlib4 gitpod again, I need to reinstall Lean 4.

Scott Morrison (Dec 13 2022 at 10:39):

@Riccardo Brasca, @Eric Wieser, @Yaël Dillies, I saw https://github.com/leanprover-community/mathlib/pull/17895 was merged without there being any sign of the corresponding mathlib4 PR https://github.com/leanprover-community/mathlib4/pull/967 even being looked at.

I suggest that maintainers who are merging either side of a matching pair of PRs either:

  • review and merge both at once, or
  • if you only have time to think about one side, only delegate that one and ask the author to merge once the other side has been approved

Scott Morrison (Dec 13 2022 at 10:40):

i.e. neither should go to bors unless the other one is at the same time / already delegated or merged.

Eric Wieser (Dec 13 2022 at 10:40):

In this case, my initial PR didn't touch mathlib4 files but gained a mathlib4 change in review

Reid Barton (Dec 13 2022 at 10:41):

OK I understand the issue now. You're saying--suppose some new mathlib3 development wants a new lemma in some already-ported file, but oops someone else already added such a lemma in mathlib4, but maybe it's in a different place or has a different name or something--which one do we take?

Eric Wieser (Dec 13 2022 at 10:41):

Perhaps I should have pushed back and said "we can move the lemma into an earlier file in a follow-up"

Reid Barton (Dec 13 2022 at 10:42):

For a single lemma, it doesn't seem like a big deal--just pick something reasonable.

Riccardo Brasca (Dec 13 2022 at 10:42):

My bad, I didn't really read the github message about the mathlib4 file and I thought it was complaining about a long line. I will be more careful.

Reid Barton (Dec 13 2022 at 10:42):

But if it's a whole new definition & set of lemmas, then it's not as obvious how to proceed

Yaël Dillies (Dec 13 2022 at 10:42):

Yes, precisely.

Mario Carneiro (Dec 13 2022 at 10:43):

As long as there is some opportunity to explicitly consider a merge I don't see the issue

Yaël Dillies (Dec 13 2022 at 10:43):

And we might not even notice the duplication before a long time.

Mario Carneiro (Dec 13 2022 at 10:44):

We already have that issue, where a mathlib4 definition is made and #aligned without noticing that a similar lean 4 definition already exists

Mario Carneiro (Dec 13 2022 at 10:44):

so we end up with two equivalent definitions in mathlib4

Mario Carneiro (Dec 13 2022 at 10:45):

this isn't a huge problem in the sense that it doesn't cause any failures, and as soon as someone notices it's fairly easy to deduplicate as long as the merge is defeq

Mario Carneiro (Dec 13 2022 at 10:45):

if it's not then we have the usual issues, backporting etc

Reid Barton (Dec 13 2022 at 10:46):

Right I think the main question is to decide whether, in this situation, it's mathlib4's job to match mathlib3, or mathlib3's job to match mathlib4.

Mario Carneiro (Dec 13 2022 at 10:46):

I think we should try to do the best thing, and it doesn't matter if that is in mathlib3 or mathlib4

Mario Carneiro (Dec 13 2022 at 10:47):

it's basically just two independent implementations of a thing and we have to merge them

Mario Carneiro (Dec 13 2022 at 10:48):

it's less bureaucracy to make mathlib4 match mathlib3 though

Sebastian Ullrich (Dec 13 2022 at 11:19):

Yaël Dillies said:

Mario, if I stop and start the mathlib4 gitpod again, I need to reinstall Lean 4.

Why is that? If you mean opening the same workspace again, I thought they were supposed to be persistent.

Yaël Dillies (Dec 13 2022 at 11:20):

No idea, really! But it's reproducible.

Sebastian Ullrich (Dec 13 2022 at 11:21):

Weird, I should try that. Though I heard Gitpod is declining anyway...

Eric Wieser (Dec 13 2022 at 11:27):

I think the workspace directory is persistant but the user directory is transient

Rémi Bottinelli (Dec 13 2022 at 11:46):

Regarding synchronized PRs to already ported files: Would it be possible to allow doing only a mathlib3 PR first, with some kind of delayed "duty to synchronize" allowing the mathlib3 PR to be merged in order to get the mathport thing running automatically and doing the mathlib4 sync by merging the updated mathport output with the old mathlib4 content ?
In the few such PRs I've made, I kind of had to manually deal with stuff and I guess it's more error-prone.

Eric Wieser (Dec 13 2022 at 11:51):

Opening a mathlib4 issue would be a reasonable way to record that duty

Yaël Dillies (Dec 13 2022 at 11:51):

Why not open an empty PR?

Eric Wieser (Dec 13 2022 at 11:52):

You can't?

Eric Wieser (Dec 13 2022 at 11:52):

Oh, maybe with git commit --allow-empty

Yaël Dillies (Dec 13 2022 at 11:52):

Can you not? I must say I never tried!

Mario Carneiro (Dec 13 2022 at 11:54):

Even if you do nothing, the "duty to synchronize" is recorded in the output of port-status.py

Reid Barton (Dec 13 2022 at 12:08):

In the general case there might be multiple mathlib3 PRs that want to modify the same already-ported file, and it would be tricky to update mathlib4 "atomically" for all of them.

Reid Barton (Dec 13 2022 at 12:09):

I think it's easier to let mathlib3 "go ahead" of mathlib4 for a bit, as long as the mathlib3 PR author has provided a mathlib4 branch or something with the needed changes, which can actually get applied later after the mathlib3 commit is merged

Yaël Dillies (Dec 13 2022 at 12:09):

I guess it's not so bad if a single mathlib4 PR synchronises several mathlib PRs?

Reid Barton (Dec 13 2022 at 12:11):

I think it makes it easier to track what mathlib3 content has been ported to mathlib4, especially if those several mathlib PRs got merged in a single bors run (then we have no way to even identify a subset of them by mathlib3 commit hash)

Anne Baanen (Dec 13 2022 at 15:01):

Along the same lines of this discussion: #16919 changes an already ported file, however the dependencies that actually make use of these changes have not been ported yet AFAICT. I think this should still have a corresponding mathlib4 PR. What do you think?

Reid Barton (Dec 13 2022 at 15:04):

My feeling is that this change to algebra.order.hom.basic is way too big to be practical--why not create a new file?

Yaël Dillies (Dec 13 2022 at 15:05):

For the reasons mentioned in the PR description:

I am explicitly against making a new file for the sake of the port, because by the time we can actually merge the two files again, we will have forgotten about it, and it doesn't make the port any easier anyway.

Yaël Dillies (Dec 13 2022 at 15:06):

The picture here is that algebra.order.hom.basic is an advanced file that accidentally got caught under the tide before its imports were fully fixed.

Reid Barton (Dec 13 2022 at 15:07):

I don't understand how it could not make the port easier

Yaël Dillies (Dec 13 2022 at 15:09):

Because everything that depends on algebra.order.hom.basic will be ported much later than its prerequisites, so the question is just when we want to merge #16919 and when we want to port the changes.

Reid Barton (Dec 13 2022 at 15:09):

(I also separately don't understand why it wouldn't make sense to have two separate files anyways; all the new stuff seems to mention norm, and none of the old stuff mentions norm)

Yaël Dillies (Dec 13 2022 at 15:09):

Once again, it's explained in the PR description.

Reid Barton (Dec 13 2022 at 15:10):

I don't agree that it is "explained"

Yaël Dillies (Dec 13 2022 at 15:11):

I have three arguments there:

* The new file is still small and cohesive.
* There's no use for what was previously `algebra.order.hom.basic` without the new material.
* Increasing the imports of `algebra.order.hom.basic` didn't increase the imports of the two
  files importing it: `algebra.order.absolute_value` and `analysis.normed.group.seminorm`.

Not sure what you want more.

Reid Barton (Dec 13 2022 at 15:11):

But mostly I'm still perplexed about how it doesn't make the porting task more difficult

Yaël Dillies (Dec 13 2022 at 15:13):

It's because this file is very independent from the rest, and I will have a several months window between the port of the dependencies of algebra.order.hom.basic and its children files to port #16919 to mathlib4.

Reid Barton (Dec 13 2022 at 15:13):

Because we have no way to automatically merge synport output of modified files with the already finished ports of earlier versions, right?

Reid Barton (Dec 13 2022 at 15:17):

Basically it means these ~150 lines need to be handled manually. But in a new file they would be handled largely automatically.

Yaël Dillies (Dec 13 2022 at 15:19):

Another option is to simply delete the partial port of algebra.order.hom.basic. It's quite short anyway.

Reid Barton (Dec 13 2022 at 15:20):

It looks to me like a complete port but yes, that might be possible.

Reid Barton (Dec 13 2022 at 15:21):

But in general we cannot just throw away ported files on the whims of mathlib 3 PRs.

Reid Barton (Dec 13 2022 at 15:27):

I think we should also have some general "port-todo" mechanism to keep track of things that we would like to do but are too difficult or not worth doing the port, for example putting lemmas in the correct locations

Reid Barton (Dec 13 2022 at 15:27):

Because that's surely easier than any of the possibilities discussed above.

Yaël Dillies (Dec 13 2022 at 15:36):

Waiting for algebra.group_power.order to be ported is not too hard either, but I agree with you.

Patrick Stevens (Dec 13 2022 at 22:43):

(Would GitHub Issues be a sufficient platform to record such TODOs? Or a GitHub Project for something a little more kanban?)

Yaël Dillies (Jan 05 2023 at 13:10):

Scott Morrison said:

i.e. neither should go to bors unless the other one is at the same time / already delegated or merged.

Is this still true? #17956 has been waiting mathlib4 approval for a week and I think I'll just go ahead and merge it because I can't just wait an eternity on mathlib, then another eternity on mathlib4.

Yaël Dillies (Jan 05 2023 at 13:12):

And the same will happen to #17900, I'm afraid.

Heather Macbeth (Jan 05 2023 at 16:32):

Yaël Dillies said:

#17956 has been waiting mathlib4 approval for a week and I think I'll just go ahead and merge it

I don't think you should go ahead and merge something that was conditionally delegated to you if you're not following the conditions under which it was delegated.

But indeed we should have a policy here. Should we ask that someone reviewing the mathlib3 version also review the mathlib4 version?

Yaël Dillies (Jan 05 2023 at 16:34):

The problem here is that I am unable to fulfill the conditions of the delegation.

Yaël Dillies (Jan 05 2023 at 16:37):

In fact, what are we expecting from a mathlib4 review? I want to say

  • that both PRs' content match
  • that all the #align are correct
  • that the names are properly capitalised

but each of those steps was skipped in the past. Indeed, I fixed mistakes that went against each point after delegation.

Yaël Dillies (Jan 05 2023 at 16:39):

So it seems that the only thing we expect from a mathlib4 review is more design considerations, eg regarding coercions, and compatibility with the port (avoid conflicting PRs, etc...).

Yaël Dillies (Jan 05 2023 at 16:40):

In particular, the content should not get reviewed a second time. Maybe if we make that clearer, #queue4 will empty faster.

Yaël Dillies (Jan 05 2023 at 16:43):

And PRs that are nontechnical (no coercion fiddling, and similar) and away from the tide don't really need their mathlib4 counterpart to be reviewed simultaneously.

Yaël Dillies (Jan 05 2023 at 16:45):

Yaël Dillies said:

The problem here is that I am unable to fulfill the conditions of the delegation.

This I think is particularly bad, because the PR disappears from the radar (long) before being dealt with, so attention isn't drawn to it anymore.

Ruben Van de Velde (Jan 05 2023 at 16:56):

Then you ask for review here on zulip, same as when you need another review? I looked at the mathlib4 pr and it seems fine


Last updated: Dec 20 2023 at 11:08 UTC