New PRs

Stream: mathlib4

[Reid Barton]

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]

I assume we'll ask them to be backported?

[Johan Commelin]

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]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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

[Scott Morrison]

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]

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

[Yaël Dillies]

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

[Patrick Massot]

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]

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]

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]

which is also what Reid said above

[Yaël Dillies]

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

[Mario Carneiro]

Why?

[Yaël Dillies]

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

[Mario Carneiro]

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

[Yaël Dillies]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Yaël Dillies]

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]

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]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

I suspect that we already have procedures for whatever it is

[Yaël Dillies]

"having a different set of lemmas/definitions"

[Mario Carneiro]

that's what #align is for

[Mario Carneiro]

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

[Mario Carneiro]

and there are a few options for how to proceed

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Yaël Dillies]

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]

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

[Eric Wieser]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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

[Mario Carneiro]

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

[Yaël Dillies]

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

[Scott Morrison]

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

[Yaël Dillies]

I assume this is the solution, yeah.

[Scott Morrison]

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

[Yaël Dillies]

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]

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

[Scott Morrison]

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

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

[Eric Wieser]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Riccardo Brasca]

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]

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

[Yaël Dillies]

Yes, precisely.

[Mario Carneiro]

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

[Yaël Dillies]

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

[Mario Carneiro]

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]

so we end up with two equivalent definitions in mathlib4

[Mario Carneiro]

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]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

it's less bureaucracy to make mathlib4 match mathlib3 though

[Sebastian Ullrich]

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]

No idea, really! But it's reproducible.

[Sebastian Ullrich]

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

[Eric Wieser]

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

[Rémi Bottinelli]

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]

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

[Yaël Dillies]

Why not open an empty PR?

[Eric Wieser]

You can't?

[Eric Wieser]

Oh, maybe with git commit --allow-empty

[Yaël Dillies]

Can you not? I must say I never tried!

[Mario Carneiro]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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]

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]

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]

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

[Yaël Dillies]

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]

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

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

[Reid Barton]

I don't agree that it is "explained"

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Yaël Dillies]

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

[Patrick Stevens]

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

[Yaël Dillies]

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]

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

[Heather Macbeth]

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]

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

[Yaël Dillies]

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]

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]

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

[Yaël Dillies]

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]

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]

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