Zulip Chat Archive

Stream: mathlib4

Topic: splitting order.bounded_order

Kevin Buzzard (Nov 27 2022 at 14:46):

I'd like to port a part of order.bounded_order but we're not ready for all of it yet I don't think, so I made a Lean 3 PR splitting the file #17730 from one 2000 line file into four smaller files. I then noticed that @Ruben Van de Velde had actually made a mathlib4 PR mathlib4#697 about this file so I thought that it was best not to add to the confusion andI closed the mathlib3 PR. But now I realise that actually there is plenty of work to be done on the mathlib4 PR, and I'm not even sure that we're going to be able to port all of it (this was the reason I wanted to split the file in mathlib3, well, that and the fact that I've never liked files with > 1000 lines and this file has 2000 lines). Right now the work put into the mathlib4 PR would not be wasted because only the first part of the file compiles (about the first 500 lines) and I left all these lines in order.bounded_order in the mathlib3 PR; in fact I split the file precisely at the point where the mathlib4 version stops compiling. So I am currently minded to get the mathlib3 PR pushed through and then this will make the mathlib4 port easier. Does anyone have any comments on this plan?

Ruben Van de Velde (Nov 27 2022 at 14:54):

I was very confused that github claimed you linked to this zulip message 14 hours ago :)

I'm looking how far I got in the port, but I certainly wouldn't mind if you made it easier

Jireh Loreaux (Nov 27 2022 at 14:55):

I concur, splitting would be good.

Ruben Van de Velde (Nov 27 2022 at 14:57):

Scratch that, I need to step out and won't have time to look further for a few hours at least. Do whatever makes sense and feel free to take over the mathlib4 pr or not, as you prefer

Kevin Buzzard (Nov 27 2022 at 14:59):

Well right now the mathlib4 file is clean up to the bit where it starts going on about PropCat and then it's just a copy of the mathlib3port version and full of errors, so let's maybe go for the split.

Ruben Van de Velde (Nov 27 2022 at 19:53):

Updated mathlib4#697 to match

Kevin Buzzard (Nov 27 2022 at 19:57):

oh how have you done that? Just manually deleted the stuff I moved?

Ruben Van de Velde (Nov 27 2022 at 19:58):

Yeah

Last updated: Dec 20 2023 at 11:08 UTC