Zulip Chat Archive

Stream: general

Topic: mathlib files


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 18 2018 at 13:20):

Do you know what you want to do specifically?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Dec 18 2018 at 14:03):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:05):

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

view this post on Zulip Patrick Massot (Dec 18 2018 at 14:05):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip Scott Morrison (Dec 20 2018 at 21:14):

This looks appealing!

view this post on Zulip Mario Carneiro (Dec 20 2018 at 21:23):

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

view this post on Zulip Reid Barton (Dec 20 2018 at 21:24):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Dec 20 2018 at 21:24):

(it's already there)

view this post on Zulip Patrick Massot (Dec 20 2018 at 21:25):

Basic topology is in topological_space/default.lean

view this post on Zulip 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

view this post on Zulip Patrick Massot (Dec 20 2018 at 21:25):

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

view this post on Zulip Patrick Massot (Dec 20 2018 at 21:26):

Then will come split and merge

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 20 2018 at 21:27):

because import folder.default = import folder

view this post on Zulip Patrick Massot (Dec 20 2018 at 21:27):

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

view this post on Zulip Mario Carneiro (Dec 20 2018 at 21:27):

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

view this post on Zulip Patrick Massot (Dec 20 2018 at 21:28):

this would be very easy to do

view this post on Zulip 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

view this post on Zulip Jan-David Salchow (Dec 21 2018 at 19:07):

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

view this post on Zulip 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...

view this post on Zulip Jan-David Salchow (Dec 21 2018 at 21:37):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 15 2019 at 19:50):

and the instances folder doesn't know where to go

view this post on Zulip Patrick Massot (Jan 15 2019 at 19:50):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:06):

But then where is analysis starting?

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Jan 15 2019 at 20:08):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:08):

aha, deriv is definitely analysis

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:08):

so it's nonempty

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:08):

I PR'ed

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:09):

unless deriv is calculus...

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:09):

It is indeed calculus

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:09):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:11):

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

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:11):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:12):

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

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:12):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:15):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:16):

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

view this post on Zulip Reid Barton (Jan 15 2019 at 20:21):

Or topology.topology or even topology.topological_space

view this post on Zulip Reid Barton (Jan 15 2019 at 20:25):

or general_topology.topology

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:47):

what do you mean "everything in analysis"?

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:48):

Travis seems to be confused by old oleans...

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:57):

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

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:57):

I can also rename analysis to topology

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:57):

I think topology and analysis should be separate folders

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:58):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 20:58):

depends on the file...

view this post on Zulip Patrick Massot (Jan 15 2019 at 20:59):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:00):

I think metric_space and normed_space can go in analysis

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:00):

I realize it's a border case

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:01):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:01):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:04):

Great!

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:05):

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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:05):

not yet

view this post on Zulip Reid Barton (Jan 15 2019 at 21:05):

(My plan is just to follow the MSC)

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:05):

Leo has to act to make that happen

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:06):

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

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:11):

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

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:12):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:17):

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

view this post on Zulip Reid Barton (Jan 15 2019 at 21:18):

Let me check

view this post on Zulip 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!)

view this post on Zulip 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).

view this post on Zulip Reid Barton (Jan 15 2019 at 21:20):

Oh, except for the instances directory

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:21):

Where would you put those?

view this post on Zulip Reid Barton (Jan 15 2019 at 21:21):

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

view this post on Zulip Patrick Massot (Jan 15 2019 at 21:21):

yes, that's where I started doubting again

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:28):

I like keeping analysis.real etc where they are

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:29):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:31):

I'm okay with that

view this post on Zulip Reid Barton (Jan 15 2019 at 21:32):

The question will be when we define LpL^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.

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:32):

I agree, that sounds like analysis to me

view this post on Zulip Mario Carneiro (Jan 15 2019 at 21:32):

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

view this post on Zulip 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.

view this post on Zulip 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