Zulip Chat Archive
Stream: general
Topic: Splitting file#measure_theory/function/lp_space
Eric Wieser (May 26 2023 at 15:15):
According to port-status#measure_theory/function/lp_space, this is the longest file that remains to port.
An obvious split to my eyes would be everything in the ### ℒp seminorm section (1650 lines) moving to a new measure_theory/function/lp_seminorm.lean file, leaving the remaining ~1500 lines in the current file.
Does this seem sensible?
Eric Wieser (May 26 2023 at 15:17):
(Note that #19083 is on the bors queue, so we shouldn't attempt to split until that's in master)
Mauricio Collares (May 26 2023 at 15:45):
There's an open mathlib4 PR for LpSpace which passes CI. Can't the split be done after the port?
Mauricio Collares (May 26 2023 at 15:46):
(I noticed you commented on the PR, but the CI results weren't available at the time)
Mauricio Collares (May 26 2023 at 15:47):
I know about #19083 and that it will need to be integrated into the LpSpace PR, I am just talking about the splitting suggestion, which was added to the wiki after the PR was already green
Eric Wieser (May 26 2023 at 16:18):
I know about #19083 and that it will need to be integrated into the LpSpace PR
My claim is that it will be easier to do this by porting the file from scratch; the file will be is more than 600 lines out of sync once staging lands.
Eric Wieser (May 26 2023 at 16:18):
At which point we may as well split it too
Eric Wieser (May 26 2023 at 16:21):
which was added to the wiki after the PR was already green
I've updated the wiki to point to this Zulip thread to make that timing clear; you're indeed correct. Note that the original message () predates the first commit in !4#4341 though.
Mauricio Collares (May 26 2023 at 17:58):
cc @Pol'tta / Miyahara Kō
Pol'tta / Miyahara Kō (May 27 2023 at 02:49):
OK, I'will wait for this thread.
Mauricio Collares (May 27 2023 at 05:02):
I am not really involved with the porting, but my naïve impression was that the fastest option for the porting, given that the PRs are already done, would be to land the mathlib4 PRs as is and then replace the appropriate files by re-ports later. Is there a downside to this?
Pol'tta / Miyahara Kō (May 27 2023 at 05:13):
There are many files which doesn't depends on this file.
The scale of these PRs is large, so it's more efficient to port the others and forward-port all diffs at once later.
Mauricio Collares (May 27 2023 at 05:15):
I was mostly worried about wasting your efforts, but if you're okay with waiting and re-porting that's perfect :)
Eric Wieser (May 27 2023 at 08:12):
#19112 splits the file
Patrick Massot (May 27 2023 at 08:13):
It doesn't lint.
Eric Wieser (May 27 2023 at 08:15):
Whoops, forgot to push my import tweaks. Fixed.
Ruben Van de Velde (May 27 2023 at 08:20):
That leaves us with a nice and short (checks) 1,629 line file :sweat_smile:
Eric Wieser (May 27 2023 at 08:21):
Two of them! (1692 for the original)
Patrick Massot (May 27 2023 at 08:23):
I checked the module docstrings.
Patrick Massot (May 27 2023 at 08:23):
and delegated
Eric Wieser (May 27 2023 at 08:23):
Was my guess as to ℒp space (mem_ℒp) vs Lp space (Lp) correct?
Patrick Massot (May 27 2023 at 08:24):
what guess?
Eric Wieser (May 27 2023 at 08:24):
I changed the title of the files such that each only claims to be about one of the two
Eric Wieser (May 27 2023 at 08:25):
Ah, it seems Sebastien Gouezel has left a review anyway. Thanks!
Ruben Van de Velde (May 27 2023 at 10:00):
@Eric Wieser and it's all green
Scott Morrison (May 27 2023 at 16:44):
#19083 has been merged, but the port comments wiki page also says to wait "on this thread". Can someone confirm that the wait is now over?
Eric Wieser (May 27 2023 at 18:07):
The wait is now over, but the open porting PR (that was made despite the wait) should be discarded, as it's extremely out of sync
Eric Wieser (May 27 2023 at 18:08):
Oh: but we should still wait for mathport to run overnight
Last updated: Dec 20 2023 at 11:08 UTC