Zulip Chat Archive

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:24):

First question: compare https://github.com/leanprover/mathlib/blob/master/analysis/topology/continuity.lean and https://github.com/leanprover/mathlib/blob/master/analysis/topology/continuous_map.lean

Patrick Massot (Dec 20 2018 at 21:24):

(it's already there)

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

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

so it's nonempty

Patrick Massot (Jan 15 2019 at 20:08):

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...

Patrick Massot (Jan 15 2019 at 20:59):

Do you like https://github.com/leanprover/mathlib/tree/ede7943feb0c5a8fa6ea481c8d08adf49104d55e/src ?

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

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

Great!

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

I wanted to ask about this new maintainer list: does it mean you have push access?

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

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?

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

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: Dec 20 2023 at 11:08 UTC