## Stream: maths

### Topic: Splitting topology

#### Patrick Massot (Jan 22 2019 at 13:59):

@Mario Carneiro @Johannes Hölzl @Reid Barton I continued moving on the topology reorganization project. The next step was to split topology.basic and topology.continuity while gathering the basics of continuity and the basics of topological spaces. My current result is at https://github.com/leanprover-community/mathlib/tree/top_split I need comments before moving on. My next step would be to reorganize uniform spaces and topological structures, still following the general scheme discussed in Amsterdam

#### Patrick Massot (Jan 22 2019 at 14:07):

Recall that one goal was to have files with less than 1000 lines, and lighters dependencies for stuff needing only the basics of topological spaces and continuous functions. The current lines counts are

  1927 basic.lean
460 bounded_continuous_function.lean
118 compact_open.lean
1568 continuity.lean
271 stone_cech.lean


my proposal has:

   206 bases.lean
591 basic.lean
460 bounded_continuous_function.lean
118 compact_open.lean
957 constructions.lean
359 maps.lean
132 opens.lean
573 order.lean
280 separation.lean
272 stone_cech.lean
468 subset_properties.lean


you can still see I got tired with constructions.lean (which has products, sum, quotients, pi...). That one could probably be split more

#### Patrick Massot (Jan 22 2019 at 14:10):

Damn, I forgot to move homeomorphisms from constructions to map

#### Patrick Massot (Jan 22 2019 at 14:11):

That will improve the balance for about 100 lines

#### Johannes Hölzl (Jan 22 2019 at 14:13):

Hm the homeomorphisms should be in basic. And I should mention that I don't like to goal of keeping the files less than 1000 lines. This is quiet arbitrary and doesn't tell anybody where to find a specific definition/proof

#### Johannes Hölzl (Jan 22 2019 at 14:13):

But looking through the changeset it looks very sensible

#### Patrick Massot (Jan 22 2019 at 14:20):

We know you don't like reducing line counts. This was very clear from reading the topology part of mathlib, and also from the Amsterdam discussion. But I think this is still a nice goal, especially when we find out there are sensible cutting points. And of course the 1000 number is totally arbitrary, although there is a certain psychological impact above that threshold.

#### Patrick Massot (Jan 22 2019 at 22:03):

So, should I open a PR?

#### Johannes Hölzl (Jan 22 2019 at 22:23):

Yes, I think this is a good PR

#### Reid Barton (Jan 23 2019 at 14:11):

I made this little ASCII art diagram of the proposed import structure (hopefully I caught everything):

basic-------------------
|                      |
order---------         subset_properties
|            |         |
separation   bases     |
|            |  |      |
maps         |  opens  |
|            |         |
constructions-----------


#### Patrick Massot (Jan 23 2019 at 16:13):

This is probably correct. The fact that constructions uses (almost) everything else is probably proving that it was not split enough. There are other files in this directory that import constructions

#### Patrick Massot (Jan 23 2019 at 16:14):

Reid, do you want to work some more on this effort?

Last updated: May 12 2021 at 07:17 UTC