Zulip Chat Archive
Stream: mathlib4
Topic: topology.algebra.order.basic
Yaël Dillies (Dec 08 2022 at 10:28):
I'm taking a stab at splitting file#topology/algebra/order/basic.
Heather Macbeth (Dec 08 2022 at 12:02):
Great! FWIW, I looked at that file a few days ago and concluded that an important feature of a split should be to reduce the imports of docs#order_topology_of_nhds_abs, since that is used in topology/metric_space/basic.
Yaël Dillies (Dec 08 2022 at 12:33):
The main part of my split was to move out of algebra. the parts that actually didn't have any algebra in them (5/6th of the file :rofl:), but I can certainly incorporate your thoughts.
Eric Wieser (Dec 08 2022 at 12:47):
If there's a clear "there's no algebra here" line, then Heather's thoughts might be best to a follow-up PR just to keep things reviewable
Yaël Dillies (Dec 08 2022 at 12:47):
Yes, absolutely.
Yaël Dillies (Dec 08 2022 at 12:47):
In fact, my PR already touches 24 files (most are just renames).
Yaël Dillies (Dec 08 2022 at 14:55):
#17859 for my move/split.
Eric Wieser (Dec 08 2022 at 15:37):
I put this in a PR comment, but I'll repeat it here; since it seems that 90% of the file is not about algebra, can you start by just renaming it to lose the algebra path segment?
Eric Wieser (Dec 08 2022 at 15:38):
That way we have a 10% move diff to review rather than a 90% move
Yaël Dillies (Dec 08 2022 at 15:38):
Sure, that makes sense.
Yaël Dillies (Dec 08 2022 at 15:43):
Last updated: Dec 20 2023 at 11:08 UTC