## Stream: general

### Topic: mathlib files

#### Patrick Massot (Dec 18 2018 at 13:19):

@Mario Carneiro and @Johannes Hölzl Would you be open to a PR reorganizing files in the analysis part of mathlib? There are huge files with a strange import graph. I would like to create new sub-folders an move stuff around so that it get easier to guess what is in what file

#### Mario Carneiro (Dec 18 2018 at 13:20):

Do you know what you want to do specifically?

#### Patrick Massot (Dec 18 2018 at 13:25):

I'd like to have a list of folders inside analysis that looks like topological_space, uniform_spaces, metric_spaces, topological_structures, normed_spaces. In particular moving topological_structures down in the import graph (ie I don't want it to be imported by so many files)

#### Patrick Massot (Dec 18 2018 at 13:27):

The current graph looks approximately like https://www.yworks.com/yed-live/?file=https://gist.githubusercontent.com/PatrickMassot/05234c6c375bfd588c346f0dab9b626a/raw/topology

#### Patrick Massot (Dec 18 2018 at 13:27):

(I removed a couple of redundant edges, and created the thing by hand, so there may be mistakes)

#### Patrick Massot (Dec 18 2018 at 13:29):

Of course it would be much easier to reorganize stuff after merging Sébastien's topology PRs

#### Johannes Hölzl (Dec 18 2018 at 14:01):

It looks to me that most of theses files depend on topological structures?! Is there no edge from topological structures to metric space (or maybe complex...)
I don't know if splitting up these files into multiple files will help. Some of this stuff is interdependent, forcing it into a hierarchy may be hard.

#### Patrick Massot (Dec 18 2018 at 14:02):

For instance, completion depends on topological structures because we complete groups and rings, but we could have the dependency the other way around, it would make more mathematical sense

#### Johannes Hölzl (Dec 18 2018 at 14:03):

How would topological structures depend on completion of groups and rings?

#### Patrick Massot (Dec 18 2018 at 14:05):

We could have a folder topological_structures with files topological_groups, topological_rings, normed_spaces. Each file would contain the relevant completed structures

#### Patrick Massot (Dec 18 2018 at 14:05):

Mathematically, the construction of the completion of a uniform space doesn't need anything from algebra

#### Patrick Massot (Dec 18 2018 at 14:05):

It is a fundamental construction that is then applied to topological structures

#### Johannes Hölzl (Dec 18 2018 at 14:12):

topological_structures are used everywhere. The completion operation is a special one. I don't see why we should have the completion at a lower place than topological structures

#### Patrick Massot (Dec 18 2018 at 14:13):

If you are worried that completions get imported everywhere then we can have files topological_group_completion etc inside the topological_structure folder

#### Patrick Massot (Dec 20 2018 at 21:01):

I just tried to move files around in the analysis folder, without splitting or joining any file. I get:

analysis
├── complex.lean
├── ennreal.lean
├── exponential.lean
├── limits.lean
├── measure_theory
│   ├── borel_space.lean
│   ├── integration.lean
│   ├── lebesgue_measure.lean
│   ├── measurable_space.lean
│   ├── measure_space.lean
│   └── outer_measure.lean
├── metric_space
│   ├── default.lean
│   └── emetric_space.lean
├── nnreal.lean
├── normed_space
│   ├── bounded_linear_maps.lean
│   └── default.lean
├── polynomial.lean
├── probability_mass_function.lean
├── real.lean
├── topological_algebra
│   ├── default.lean
│   ├── infinite_sum.lean
│   ├── quotient_topological_structures.lean
│   └── topological_groups.lean
├── topological_space
│   ├── continuity.lean
│   ├── continuous_map.lean
│   ├── default.lean
│   └── stone_cech.lean
└── uniform_space
├── completion.lean
└── default.lean


Note that I didn't increase the depth, only gathered stuff. My next move would be to split topological algebra into group and ring, and then group_completion and ring_completion, as well as splitting uniform_space/completion into manageable files. Is there any hope to get something like this merged?

#### Patrick Massot (Dec 20 2018 at 21:02):

Note also that Lean inserts default automatically, so importing the definition of topological space is done by import analysis.topological_space

#### Patrick Massot (Dec 20 2018 at 21:04):

There are still some mess at the root of analysis above, but it's still a start

#### Patrick Massot (Dec 20 2018 at 21:07):

I should say I'm ready to redo this work after PRs with Sébastien and Jeremy get merged (it's very easy to change imports using VScode "replace in files")

#### Patrick Massot (Dec 20 2018 at 21:10):

I would also update the documentation of course. I think it would be really nice to have a general cleanup and documentation effort before the Amsterdam workshop

#### Scott Morrison (Dec 20 2018 at 21:14):

This looks appealing!

#### Mario Carneiro (Dec 20 2018 at 21:23):

what's the difference between continuity and continuous_map? Also where's basic topology gone

#### Reid Barton (Dec 20 2018 at 21:24):

continuous_map is what Johannes renamed my file on the compact-open topology on mapping spaces

#### Patrick Massot (Dec 20 2018 at 21:25):

Basic topology is in topological_space/default.lean

#### Mario Carneiro (Dec 20 2018 at 21:25):

I'm not sure that's a good answer... just because it's what's there doesn't mean it's good, especially in a thread on reorganization

#### Patrick Massot (Dec 20 2018 at 21:25):

Oh sure, the above is the first step, moving files around

#### Patrick Massot (Dec 20 2018 at 21:26):

Then will come split and merge

#### Mario Carneiro (Dec 20 2018 at 21:26):

I don't like the idea of putting basic stuff in a default.lean, these files are usually the supremum of their folders' contents

#### Mario Carneiro (Dec 20 2018 at 21:27):

because import folder.default = import folder

#### Patrick Massot (Dec 20 2018 at 21:27):

I think both semantics make sense, and it avoids long names

#### Mario Carneiro (Dec 20 2018 at 21:27):

the convention is to put basic stuff in a basic.lean

#### Patrick Massot (Dec 20 2018 at 21:28):

this would be very easy to do

#### Patrick Massot (Dec 20 2018 at 21:57):

It seems a reorganization could be merged, so I'll wait for the big topology merges and then try something

#### Jan-David Salchow (Dec 21 2018 at 19:07):

I like it! Have you considered moving topology out of analysis though?

#### Patrick Massot (Dec 21 2018 at 19:53):

:slight_smile: of course this was my first reaction. But I don't want to fight here...

#### Jan-David Salchow (Dec 21 2018 at 21:37):

Interesting. Is there a rationale for keeping it in there?

#### Patrick Massot (Jan 15 2019 at 19:50):

I'm doing the file reorganization for analysis. In the end I think that the separation between topology and analysis doesn't look good. The split is pretty much arbitrary, and files about specialized topics like the compact-open topology end up at the same level as folders like uniform_space and metric_space. It looks a bit weird

#### Patrick Massot (Jan 15 2019 at 19:50):

and the instances folder doesn't know where to go

#### Patrick Massot (Jan 15 2019 at 19:50):

I think I'll PR something a bit closer to my original proposal

#### Mario Carneiro (Jan 15 2019 at 19:54):

there is no rule that a folder must have only files or only folders in it; in fact I would expect that specialized topics end up in loose files alongside folders where the theory is more developed. data is like that

#### Mario Carneiro (Jan 15 2019 at 19:54):

so I don't see a problem with topology/uniform_space/ being sibling to topology/compact_open.lean

#### Patrick Massot (Jan 15 2019 at 19:55):

I have a commit strictly implementing (the move only part) of the proposal. Now I'm trying something slightly different. We'll see what looks best

#### Kevin Buzzard (Jan 15 2019 at 20:04):

Let me remark again that for 25 years I had no idea that topology was a subset of analysis.

#### Patrick Massot (Jan 15 2019 at 20:06):

But then where is analysis starting?

#### Patrick Massot (Jan 15 2019 at 20:07):

Of course I can also rename analysis to topology. But soon we'll have derivative, and it's not really topology either (unless you include differential topology in the same folder)

#### Kevin Buzzard (Jan 15 2019 at 20:08):

Maybe I should leave these questions to the topologist :-)

#### Mario Carneiro (Jan 15 2019 at 20:08):

aha, deriv is definitely analysis

so it's nonempty

I PR'ed

#### Mario Carneiro (Jan 15 2019 at 20:09):

unless deriv is calculus...

#### Patrick Massot (Jan 15 2019 at 20:09):

It is indeed calculus

#### Patrick Massot (Jan 15 2019 at 20:09):

This is the name of that file in my differential topology repository

#### Mario Carneiro (Jan 15 2019 at 20:10):

but integrals are also calculus and I don't know where to draw the line from measure theory

#### Patrick Massot (Jan 15 2019 at 20:11):

in French we have "calcul différentiel" including derivatives and "calcul intégral"

#### Patrick Massot (Jan 15 2019 at 20:11):

but elementary courses are about "real analysis", and involve both

#### Reid Barton (Jan 15 2019 at 20:11):

files about specialized topics like the compact-open topology end up at the same level as folders like uniform_space and metric_space.

I guess this is because we have TOPOLOGY, the top-level classification, and topology as opposed to metric spaces

#### Patrick Massot (Jan 15 2019 at 20:12):

We could also follow Johannes, and have only one mathlib file

#### Patrick Massot (Jan 15 2019 at 20:12):

https://github.com/leanprover/mathlib/pull/598

#### Mario Carneiro (Jan 15 2019 at 20:15):

wait, so this PR is still putting everything in analysis/?

#### Mario Carneiro (Jan 15 2019 at 20:16):

we could have topology/basic/ for separating topology and TOPOLOGY

#### Reid Barton (Jan 15 2019 at 20:21):

Or topology.topology or even topology.topological_space

#### Reid Barton (Jan 15 2019 at 20:25):

or general_topology.topology

#### Patrick Massot (Jan 15 2019 at 20:47):

what do you mean "everything in analysis"?

#### Patrick Massot (Jan 15 2019 at 20:48):

Travis seems to be confused by old oleans...

#### Patrick Massot (Jan 15 2019 at 20:57):

I'm sorry I don't understand what Reid and you suggest

#### Patrick Massot (Jan 15 2019 at 20:57):

I can also rename analysis to topology

#### Mario Carneiro (Jan 15 2019 at 20:57):

I think topology and analysis should be separate folders

#### Mario Carneiro (Jan 15 2019 at 20:58):

I'm not sure why this is in any way strange

#### Patrick Massot (Jan 15 2019 at 20:58):

That's not the question. The question is how do you choose which files go into which folder

#### Mario Carneiro (Jan 15 2019 at 20:58):

depends on the file...

#### Mario Carneiro (Jan 15 2019 at 21:00):

I think metric_space and normed_space can go in analysis

#### Mario Carneiro (Jan 15 2019 at 21:00):

I realize it's a border case

#### Mario Carneiro (Jan 15 2019 at 21:01):

I prefer the name topology to general_topology for the top level folder

#### Mario Carneiro (Jan 15 2019 at 21:01):

unless there are any plans for specific_topology folders at the top level, it's a meaningless distinction which just makes names longer

#### Patrick Massot (Jan 15 2019 at 21:01):

It's much easier to exclude metric spaces if we call it general topology

#### Mario Carneiro (Jan 15 2019 at 21:03):

well it can still mean general topology, I am just objecting to the extra letters

#### Mario Carneiro (Jan 15 2019 at 21:04):

In lean 2 there were package .md files for all the subfolders, we could bring that back

#### Reid Barton (Jan 15 2019 at 21:04):

As a maintainer for the topology section of mathlib I volunteer to decide which things are or are not topology

Great!

not yet

#### Reid Barton (Jan 15 2019 at 21:05):

(My plan is just to follow the MSC)

#### Mario Carneiro (Jan 15 2019 at 21:05):

Leo has to act to make that happen

#### Patrick Massot (Jan 15 2019 at 21:06):

I thought I was elected the documentation dictator, will I get push access?

#### Patrick Massot (Jan 15 2019 at 21:11):

Reid, could you tell us what the file organization would look like then?

#### Patrick Massot (Jan 15 2019 at 21:12):

I can confirm I can build from scratch here, and Travis is confused

#### Reid Barton (Jan 15 2019 at 21:16):

As a first approximation, I would suggest moving all of analysis to topology except for exponential.lean, normed_space and specific_limits.lean, leaving the directory structure intact

#### Reid Barton (Jan 15 2019 at 21:16):

That doesn't leave much in analysis but I think it's just because we don't have much analysis yet.

#### Patrick Massot (Jan 15 2019 at 21:17):

Isn't this what I had in my first commit?

Let me check

#### Reid Barton (Jan 15 2019 at 21:19):

As far as the analysis/topology split is concerned, it's exactly the same. (I didn't peek first!)

#### Reid Barton (Jan 15 2019 at 21:20):

So I would just suggest bringing back the topological_space subdirectory and renaming the top-level directory to topology (with the understanding that it really means general topology).

#### Reid Barton (Jan 15 2019 at 21:20):

Oh, except for the instances directory

#### Patrick Massot (Jan 15 2019 at 21:21):

Where would you put those?

#### Reid Barton (Jan 15 2019 at 21:21):

I guess this is a bit awkward, because some of these are also normed spaces. Hmm

#### Patrick Massot (Jan 15 2019 at 21:21):

yes, that's where I started doubting again

#### Mario Carneiro (Jan 15 2019 at 21:28):

I like keeping analysis.real etc where they are

#### Mario Carneiro (Jan 15 2019 at 21:29):

unless there is a reason to split the file up into topology and analysis stuff

#### Reid Barton (Jan 15 2019 at 21:30):

Actually it turns out there are no instances related to normed spaces in any of those files. So the whole directory could move to topology

#### Mario Carneiro (Jan 15 2019 at 21:31):

I'm okay with that

#### Reid Barton (Jan 15 2019 at 21:32):

The question will be when we define $L^p$ spaces and so on which are normed spaces and therefore also have a topology, what do we do. I think we can just stick everything related to those in the analysis directory though.

#### Mario Carneiro (Jan 15 2019 at 21:32):

I agree, that sounds like analysis to me

#### Mario Carneiro (Jan 15 2019 at 21:32):

the whole construction of the space will be an analysis thing anyway

#### Jeremy Avigad (Jan 16 2019 at 02:41):

All this sounds good to me. I agree with Mario that topology is better than general_topology.

#### Patrick Massot (Jan 16 2019 at 08:34):

I just renamed general_topology to topology, and moved instances there. Is everybody happy?

Last updated: May 13 2021 at 22:15 UTC