mathlib file organization

Stream: general

[Sean Leather]

For those interested in the file organization of mathlib, I've written up a proposal for a small change that, I think, will improve things a bit. Feedback welcome!

[Johan Commelin]

Interesting proposal. I have also noticed myself getting lost in the long files...

[Johan Commelin]

I would also like to separate the "interface lemma's" from the "real beef", although maybe there is not always a clear line between them.

[Sean Leather]

I have also noticed myself getting lost in the long files...

I'm glad I'm not the only one. I think this is a first logical step to reducing the size of files. There are other steps that can be taken later, of course.

[Johan Commelin]

Also, I have never read what the purpose of default.lean is. But if I inferred it correctly, then I think we should make more use of it.

[Johan Commelin]

And then using more files will not increase the length of import lines.

[Mario Carneiro]

I've been deliberately avoiding the use of default.lean within mathlib, and I think it's good practice without as well

[Sean Leather]

AFAIK, the file data/list/default.lean allows you to write import data.list instead of import data.list.default. So, the default.lean file generally imports everything in the directory.

[Johan Commelin]

exactly

[Mario Carneiro]

right

[Mario Carneiro]

and that's exactly what I don't want

[Johan Commelin]

Why not?

[Mario Carneiro]

that adds a bunch of spurious dependencies in an already delicate graph

[Mario Carneiro]

remember that circular dependencies are bad but there isn't an obvious linear order of files

[Johan Commelin]

Sure, but there is a partial order, right?

[Johannes Hölzl]

It should be a DAG

[Johan Commelin]

Do we already have a script that generates a graphviz visualisation?

[Mario Carneiro]

mathlib.gif

[Johan Commelin]

Right, I had a similar graph on the level of theorems and proofs for my thesis.

[Johan Commelin]

But why are you scared that the graph becomes to delicate for Lean?

[Sean Leather]

I don't quite see the problem with default.lean. Nonetheless, I see it as just an extra and there's no actual need to have one.

[Johan Commelin]

Well, we need it to keep imports manageable.

[Johan Commelin]

Already it is common to have files with >8 imports

[Johan Commelin]

If you want to split a 3000-line file into 5 files

[Mario Carneiro]

Currently, folders are organized by topic, and files are organized by dependency units

[Mario Carneiro]

so if there is no dependency issue and the topic is still the same, it all goes in one file

[Sean Leather]

At least with my proposal, once you split a file into one for definitions and one for theorems, the theorems file imports the definitions file, and you just import the theorems file. The default.lean just allows you to leave off one part of the hierarchy.

[Johan Commelin]

What is a "dependency issue"?

[Mario Carneiro]

A is used by B, which is used by A'

[Mario Carneiro]

and A' wants to be in the same file as A

[Johan Commelin]

Ok, and there is a reason (I guess the topic) that B should not be in that file as well.

[Mario Carneiro]

I've thought many times about separating out definitions. But I'm not sure it's as easy as that

[Mario Carneiro]

in lean, definitions and theorems are all mixed up thanks to curry howard

[Sean Leather]

As I said, there may be exceptions, but I think there are many obvious easy examples.

[Sean Leather]

And I'm happy to give it a try myself.

[Mario Carneiro]

If you are using list as your test bed it's not representative

[Sean Leather]

If other people think this is a good thing.

[Mario Carneiro]

programming stuff in general tends to be less dependent

[Sean Leather]

Perhaps. But there is a lot of programming stuff in mathlib. :simple_smile:

[Sean Leather]

And what's the harm with doing it there?

[Mario Carneiro]

also, how is theorem organization handled? What to do if a definition depends on a theorem?

[Sean Leather]

It probably depends on the example.

[Mario Carneiro]

What about instances? are they definitions or theorems?

[Sean Leather]

To keep the proposal minimal, I don't say anything about that.

[Sean Leather]

This is where concrete examples help.

[Mario Carneiro]

rat is a field

[Sean Leather]

What I really want to know is whether people are, in general, in favor of having definitions separated from theorems. From my experience using mathlib, I believe I am. There are certainly wrinkles to be ironed out.

[Mario Carneiro]

I am worried about losing topicality

[Mario Carneiro]

particularly for smaller definitions that are more auxiliary or only used in a few theorems

[Sean Leather]

Isn't rat a structure?

[Mario Carneiro]

I mean a mathematical field

[Mario Carneiro]

That's an instance

[Mario Carneiro]

in rat.lean

[Sean Leather]

You mean instance field_rat : discrete_field ℚ?

[Mario Carneiro]

yeah

[Mario Carneiro]

@Jeremy Avigad may want to chip in on this topic

[Sean Leather]

It seems to me that data/rat.lean would also benefit from extracting the defs.

$ grep '^def' data/rat.lean | wc -l
       7
$ grep '^theorem' data/rat.lean | wc -l
      44
$ grep '^instance' data/rat.lean | wc -l
      16

Whether you put instances in with theorems or not is a secondary question. Since I'm not familiar with it, I don't have the answer for you.

[Mario Carneiro]

You can't just count them, theorems will almost always outnumber defs by a large margin

[Sean Leather]

That's kind of the point. :wink:

[Mario Carneiro]

But there is often def -> theorem -> def -> theorem dependencies that will be messed up with such a reorganization

[Sean Leather]

Indeed! So it needs a concrete attempt.

[Johannes Hölzl]

and the instances and theorems are very interdependent

[Mario Carneiro]

By the way, one downside of the partial order structure of files is that it's not exactly a lattice, so it's not clear where to put cross cutting theorems

[Johan Commelin]

With my current PR on algebraic topology, I split it up in 3 files... in this example, would you have rather had 1 file? (Question is for mathlib maintainers.)

[Mario Carneiro]

like if you have incomparable files A and B and you have a theorem about AB which is used by C

[Sean Leather]

By the way, one downside of the partial order structure of files is that it's not exactly a lattice, so it's not clear where to put cross cutting theorems

Which is one of the reasons I left that concern out of the proposal.

[Johan Commelin]

(Mario, in my thesis I had one theorem/def per file -- this is all LaTeX --, and it worked quite nicely. I had some LaTeX macros that hyperlinked all references to theorems and definitions. And then with a bit of bash-fu I got PDF's for every theorem/def. I wanted an HTML realisation, but it never became nice enough...)

[Johan Commelin]

So... that was the other end of the spectrum (-;

[Johan Commelin]

And it was on a smaller scale, and not formalised.

[Sean Leather]

Yeah, that could make sense for a thesis, but it's probably too far for a library. :wink:

[Mario Carneiro]

By the way, metamath is organized as set.mm, a single 20MB text file with lots of ascii headers of various levels to give it a book-like structure

[Mario Carneiro]

so I guess that's the extreme opposite

[Sean Leather]

OMG :bomb:

[Mario Carneiro]

One thing that I like about that is it enforces a linear dependency structure, which makes the dependency question trivial

[Mario Carneiro]

the downside is that it (apparently) adds a lot of spurious dependencies, more than are truly needed by the theorems

[Mario Carneiro]

But that's less of a problem when the entire file can be verified in less than 10 seconds

[Mario Carneiro]

Also metamath has a separate html view so you aren't completely reliant on text navigation, you can look at abridged views and high level views of the theorems so that you can skip over the boring stuff... Maybe something like this in lean could be helpful for you

[Sean Leather]

It's still useful to browse code, and I still think good code organization is a worthy goal.

[Jeremy Avigad]

I think it generally makes it easier to read theory files when the definitions are an integral part of theory. The definitions are needed to understand the theorems and the theorems illustrate the intended usage of the definitions. It would be annoying to have to flip back and forth between files.

[Chris Hughes]

How about just listing all the definitions in a comment at the top of the file?

[Kevin Buzzard]

And while we're at it how about listing what goes on in the file in another comment at the top of the file?

[Kevin Buzzard]

@Mario Carneiro what would you make of such PRs? Someone adding definitions and comments explaining what is going in various files in mathlib?

[Mario Carneiro]

Absolutely go ahead

[Mario Carneiro]

I do my best but I also have a lot of theorems I want to prove

[Kevin Buzzard]

theorems are overrated

[Scott Morrison]

@Kevin Buzzard

[Kevin Buzzard]

I'm into definitions

[Johan Commelin]

theorems are overrated — @Kevin Buzzard

I just read the following blogpost of M. Harris: https://mathematicswithoutapologies.wordpress.com/2018/06/02/is-the-tone-appropriate-is-the-mathematics-at-the-right-level/
It contains the following quote of Scholze:

“What I care most about are definitions. For one thing, humans describe mathematics through language, and, as always, we need sharp words in order to articulate our ideas clearly. (For example, for a long time, I had some idea of the concept of diamonds. But only when I came up with a good name could I really start to think about it, let alone communicate it to others. Finding the name took several months (or even a year?). Then it took another two or three years to finally write down the correct definition (among many close variants). The essential difficulty in writing “Etale cohomology of diamonds” was (by far) not giving the proofs, but finding the definitions.) But even beyond mere language, we perceive mathematical nature through the lenses given by definitions, and it is critical that the definitions put the essential points into focus.

Unfortunately, it is impossible to find the right definitions by pure thought; one needs to detect the correct problems where progress will require the isolation of a new key concept.”

[Mario Carneiro]

I think this is an over-mature view though; it is only in the context where theorems are commonplace that you can advocate a return to focus on definitions

[Mario Carneiro]

it's too easy to abuse this view to focus only on definitions at the expense of theorems

[Kevin Buzzard]

On the other hand there are some definitions which are much more important than theorems.

[Mario Carneiro]

I don't argue that definitions aren't important, essential even. They are the core of the theory, the things that theorems relate

[Mario Carneiro]

but to take one without the other is to see only half the picture

[Johan Commelin]

Maybe I like the fact that DTT muddles the distinction between the two.

[Kevin Buzzard]

That's right, so we should take the most important of both :-)

[Kevin Buzzard]

and there is surely ample evidence out there now in blogland and mathoverflow and whatever

[Kevin Buzzard]

that perfectoid spaces are a supremely important definition

[Sean Leather]

I think it generally makes it easier to read theory files when the definitions are an integral part of theory. The definitions are needed to understand the theorems and the theorems illustrate the intended usage of the definitions. It would be annoying to have to flip back and forth between files.

@Jeremy Avigad Thanks for your thoughts.

I agree with you that it is useful to see definitions and theorems together, but I find that most theorems beyond the simplest rfl involve more than one definition. Thus, when the definitions are interleaved with large chunks of theorems, I'm either flipping back and forth or viewing different parts of the same file in a split screen. Whereas with all (or as many as is reasonable) of the definitions in one file, I can view two files side-by-side, one with definitions and one with theorems involving those definitions.

To summarize, while I think it would be nice to have a definition with a nearby associated group of theorems, I think that that is already problematic in mathlib in a very practical sense because the number of theorems generally surpasses the number of definitions and makes it difficult to find them. In addition to that, I think definition discovery is a useful part of learning a theory topic and would be aided by putting the definitions in one place.

[Sean Leather]

How about just listing all the definitions in a comment at the top of the file?

@Chris Hughes: By “definition,” are you referring to either (a) the entire declaration (i.e. def name := term) or (b) only the name?

(a) While I grant you that we are not engaging in (“full-blown”) software engineering when writing mathlib, this is one of those big no-no's in practice. Duplication in comments is notorious for getting out of sync with code. I would strongly recommend against doing this.

(b) Listing the names may provide a minor benefit for reference. But, since theorems generally use the unfolded definition in some form, this won't be helpful when trying to understand a theorem that uses multiple definitions, because you will end up trying to find the declarations themselves. It won't solve the problem I'm trying to solve.

[Andrew Ashworth]

I think what you really want to do is write a doxygen extension for lean :)

[Andrew Ashworth]

not like other programming files don't have the same problem with separation of data structures / classes and methods...

[Sean Leather]

not like other programming files don't have the same problem with separation of data structures / classes and methods...

Certainly! My proposal is actually similar to a common pattern in Haskell package development: putting types in a file of their own.

[Andrew Ashworth]

that's a big pain in lean though since circular dependencies are hard to handle

[Johan Commelin]

https://www.stack.nl/~dimitri/doxygen/manual/faq.html#faq_pgm_X
Seems like Lean falls in the 3rd category...

[Andrew Ashworth]

it wouldn't be so bad if you wanted something quick and dirty - you just want to grab things in between def | definition, lemma, theorem, :, :=, and a newline

[Andrew Ashworth]

but I am not volunteering to do this :) however it seems more likely to happen than changing how mathlib is organized

[Andrew Ashworth]

it seems straightfoward - famous last words of every project I've ever estimated ever

[Patrick Massot]

I know I'm always writing the same thing, but I think we shouldn't forget that some people already developed huge libraries in a language very close to Lean, and have a look at how they handle this. For the comments at top of files see https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/vector.v (this is random file from math-comp, they all look the same)

[Patrick Massot]

It also seems they keep the definitions and lemmas in the same file

[Patrick Massot]

@Assia Mahboubi will probably tell us much more

[Assia Mahboubi]

Hi @Patrick Massot . I read the thread briefly, so I might have missed the point of the debate. I do not see the advantage of having definitions and theorems in separated files. Sometimes, the difference between a definition and a theorem is quite thin. Also, what makes me believe that an object in the library is what I am looking for is not only its name (and not even only its definition) but also the companion lemmas, examples, etc. So it would not ease my inspection. Last, the definition of a list in Lean is probably no going to change, but for more complex objects, definitions often evolve during the course of the development. "Testing" the subsequent impact of the changes on notations, lemmas, theorem, etc. is easier if this content is not too far I would say. However, part of the answer might be of a technological nature. Even if I am flatted that people like @Patrick Massot want to hear from my experience, you Lean people might benefit from tools that change the game.

[Sebastian Ullrich]

One more argument in favor of not separating definitions and lemmas: You can make uninteresting helper definitions privateand still prove things about them

[Sean Leather]

That's really only an argument for not separating those definitions. :wink: (But it is a fine argument in any case.)