Zulip Chat Archive
Stream: mathlib4
Topic: Port Status Webpage
Shreyas Srinivas (Jan 19 2023 at 21:15):
The port status webpage seems to be showing some --help output before the port list:
https://math.commelin.net/files/port_status.html
port-status-Screenshot-from-2023-01-19-21-44-03.png port-status-Screenshot-from-2023-01-19-21-44-23.png
Johan Commelin (Jan 19 2023 at 21:21):
Looks like some git command is failing. I'll investigate tomorrow
Moritz Firsching (Jan 20 2023 at 01:47):
mathlib#18237
Seems like there is a ref to a blob, which somehow got in.
318fa77a2ba140a221a5b6cabae466ba855c2ffc
This is not a commit, but a blob. A quick fix is to add a check for that in the script...
Johan Commelin (Jan 20 2023 at 04:36):
@Moritz Firsching Feel free to PR, I might have time to look into it ~3 hrs from now.
Moritz Firsching (Jan 20 2023 at 04:40):
Yeah I made a PR
Johan Commelin (Jan 20 2023 at 04:48):
Ooh, I missed that :oops: :see_no_evil: :face_palm:
Johan Commelin (Jan 20 2023 at 04:48):
Thanks so much!
Johan Commelin (Jan 20 2023 at 04:48):
I kicked it on the queue!
Eric Wieser (Jan 20 2023 at 08:01):
Which file contains the blob?
Eric Wieser (Jan 20 2023 at 08:04):
Just ignoring that without diagnostic feels like a mistake
Reid Barton (Jan 20 2023 at 08:11):
It's in Mathlib/Data/Nat/Dist.lean
Reid Barton (Jan 20 2023 at 08:11):
Eric Wieser (Jan 20 2023 at 08:42):
Oops
Eric Wieser (Jan 20 2023 at 08:43):
I was tricked into thinking that the sha in the git diff output was a commit
Reid Barton (Jan 20 2023 at 10:27):
Yes, understandable.
Reid Barton (Jan 20 2023 at 10:27):
We need much better tooling/automation for dealing with these resynchronization PRs.
Reid Barton (Jan 20 2023 at 10:27):
Or (my preference) simply stop changing already-ported files in mathlib3.
Eric Wieser (Jan 20 2023 at 10:49):
I'll update my status page to show the actual SHAs in the next few days
Kevin Buzzard (Jan 20 2023 at 11:59):
There are now far more PRs on #queue4 editing already-ported files than there are PRs porting files (compare mathlib3-pair labels to mathlib-port labels), meaning that a lot of my reviewing effort is going into looking at these PRs instead of porting PRs.
Patrick Massot (Jan 20 2023 at 12:34):
Yes, there is a lot of wasted energy there. Maybe the porting strategy will change in the near future.
Eric Wieser (Jan 20 2023 at 13:00):
Perhap the approach should be that we assign all mathlib3-pair PRs to the person who reviewed/merged the mathlib3 PR?
Kevin Buzzard (Jan 20 2023 at 13:12):
Right now it's not too hard in theory to review a paired PR, once the mathlib3 PR is merged; you just have to compare the diffs in the mathlib3 PR and the mathlib4 PR. But in practice it can be tricky because github doesn't always react in the same way to changes. One of Yael's PRs was only a few lines long but I had to carefully look at both the mathlib3 and mathlib4 source files (not just the changed lines) to make sure that some apparently-different variables changes were in fact the same, and one much larger PR had got "de-synced" the way sometimes happens in github (it's diffing a lemma against the lemma two below the one that it should be comparing it with etc) and this made it much harder than expected, but it certainly wasn't impossible, it was just time-consuming. I can't really imagine automation being able to solve these two issues.
Eric Wieser (Jan 20 2023 at 13:52):
If the automation were just "look at the mathport output" then I think that would still help a lot
Eric Wieser (Jan 20 2023 at 13:53):
You don't need to be comparing the lean3 source; we don't do that for any fresh ports, so we shouldn't need to do it for updating ports either
Kevin Buzzard (Jan 20 2023 at 15:07):
I'm comparing the lean 3 diff. I don't see any other viable way to review these PRs right now and they're coming in thick and fast. The theory suggested in the porting meeting was that the mathport output should just be a bunch of #print statements and then the mathlib4 PR, but the reality was that it was full of definitions of instances and protected theorems and huge error messages saying that things weren't aligned.
To give a concrete example, take a look at https://github.com/leanprover-community/mathlib4/pull/1411 matching https://github.com/leanprover-community/mathlib/pull/18086 . That's a very short PR and it was not that hard to verify from the diffs that the two PRs did the same thing (although it wasn't entirely trivial because the diffs differ with variable usage). However now take a look at what mathlib3port is saying: https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Algebra/SmulWithZero.lean . I would far rather be checking the diffs than looking at that.
The other example I alluded to earlier is https://github.com/leanprover-community/mathlib4/pull/1439 , with parallel mathlib3 PR https://github.com/leanprover-community/mathlib/pull/18081, merged, and which changed 12 files, three of which had been ported. Github kindly kept the ordering of the files so comparing the diffs wasn't that bad, but there were a lot of changes in the three ported files. Take a look at the first change in the first (according to github) file which was already ported: that was Algebra.Group.WithOne.Defs . The first change is to add an id $ to a structure field, presumably because something broke in the refactor in mathlib3, but the analogous thing didn't break in mathlib4 so there is no change at all. Note that the instance shows up in the mathlib3port file https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Algebra/Group/WithOne/Defs.lean anyway because every single instance shows up.
I am not sure that we have a good answer for how to review these paired PRs other than by manually trawling through the diffs, and I think that these two case studies firmly prove my point right now.
Kevin Buzzard (Jan 20 2023 at 15:09):
I am definitely tending towards the opinion that mathlib3 PRs which make changes to ported files should simply be banned, or perhaps at least temporarily halted until we actually find a viable solution to this, because I envisage that the mathlib4 queue is simply going to get swamped by these and they're hell to review.
Eric Wieser (Jan 20 2023 at 15:09):
One workflow that could work is to generate the diff in mathlib3port between the version of the file that was ported and the version in mathlib3 master
Eric Wieser (Jan 20 2023 at 15:11):
Which would be a lot easier if mathlib3port didn't update to reflect changes in mathlib4
Eric Wieser (Jan 20 2023 at 15:11):
I completely agree that the automation doesn't exist, but I don't believe that it can't exist
Shreyas Srinivas (Jan 20 2023 at 15:13):
Another issue : It seems the webpage is not list all files to be ported as before. There were a couple of Data.Vector files on the webpage yesterday (including one I am currently wrapping up).
Eric Wieser (Jan 20 2023 at 15:15):
Just to check, are you referring to https://math.commelin.net/files/port_status.html or https://leanprover-community.github.io/mathlib-port-status?
Shreyas Srinivas (Jan 20 2023 at 15:15):
https://math.commelin.net/files/port_status.html
Eric Wieser (Jan 20 2023 at 15:16):
Which files specifically are you claiming are missing?
Shreyas Srinivas (Jan 20 2023 at 15:17):
data.vector.mem and data.vector.zip
Shreyas Srinivas (Jan 20 2023 at 15:17):
data.vector.mem is on mathlib4#1697 (since yesterday evening)
Eric Wieser (Jan 20 2023 at 15:18):
Odd, both appear on the second link
Shreyas Srinivas (Jan 20 2023 at 15:19):
Eric Wieser (Jan 20 2023 at 15:19):
Right, they are indeed missing from the first link
Eric Wieser (Jan 20 2023 at 15:19):
But present at https://leanprover-community.github.io/mathlib-port-status/?q=vector
Shreyas Srinivas (Jan 20 2023 at 15:23):
Ah I see. #port-status takes me to the light-coloured webpage
Eric Wieser (Jan 20 2023 at 15:33):
The other page is "matches-your-docs-theme"-colored
Reid Barton (Jan 20 2023 at 16:13):
Eric Wieser said:
I completely agree that the automation doesn't exist, but I don't believe that it can't exist
Personally I have just been ignoring mathlib4 resynchronization PRs, based on this reasoning.
Reid Barton (Jan 20 2023 at 16:14):
After all, that's not likely to cause any problem until we get around to porting whatever other mathlib file needed the change in question.
Mario Carneiro (Jan 20 2023 at 18:08):
Kevin Buzzard said:
I'm comparing the lean 3 diff. I don't see any other viable way to review these PRs right now and they're coming in thick and fast. The theory suggested in the porting meeting was that the mathport output should just be a bunch of #print statements and then the mathlib4 PR, but the reality was that it was full of definitions of instances and protected theorems and huge error messages saying that things weren't aligned.
By the way, I didn't mention it in the porting meeting but one other thing you will notice in post-port mathport files is these alignment failure error messages. Those are important, it means that something was aligned that should not have been, and the solution is to either put \_x on the align statement to ignore the misalignment, or double check / fix the definition if it is supposed to be defeq. These are basically things that should have been dealt with during the initial file port, but we don't have a good process for that since it requires running mathport on the newly ported file, and mathport only runs regularly on mathlib4 master, not PRs.
Mario Carneiro (Jan 20 2023 at 18:09):
If you can set up oneshot it is fairly easy to iterate on the file to get rid of the messages
Eric Wieser (Jan 20 2023 at 18:10):
It sounds like we need oneshot set up in the gitpod container for mathlib4?
Heather Macbeth (Jan 20 2023 at 19:05):
Eric Wieser said:
It sounds like we need oneshot set up in the gitpod container for mathlib4?
That would be very useful.
Eric Wieser (Feb 20 2023 at 17:24):
https://github.com/leanprover-community/mathport/pull/229 adds some basic gitpod config to allow mathport to be run, I haven't tried it with oneshot
Eric Wieser (Feb 20 2023 at 17:26):
It would be a little more pleasant to use if we had it publish a cache at build time via lake exe cache, as it takes 3-5 minutes to compile everything.
Arthur Paulino (Feb 20 2023 at 17:46):
I'm going to start a thread about an idea that I had that should allow us to expand the caching system to other repos
Last updated: Dec 20 2023 at 11:08 UTC