Organization of Mathlib

Stream: new members

[Brent A Ritterbeck]

While working through the bounded_lattice file, I noticed that there are a lot of different classes in the file. Is it standard practice to put a whole bunch of classes related together into one file, or have the various classes in that file not yet been split out into their own files? Maybe a better example would be splitting lattice into a file for distributive_lattice, join_semilattice, and meet_semilattice? I'm not giving any suggestions or criticism. I'm simply trying to understand the organizational choices being made.

[Mario Carneiro]

It can be done either way. If there are lots of files importing can become more annoying/pedantic, this way you just say "I want lattices" and you get all the stuff

[Mario Carneiro]

Note that not all the classes are actually in there, in particular I think complete lattices and boolean lattices are in another file

[Brent A Ritterbeck]

Mario Carneiro said:

It can be done either way. If there are lots of files importing can become more annoying/pedantic, this way you just say "I want lattices" and you get all the stuff

Couldn't that be solved in a manner similar to https://github.com/lballabio/QuantLib/blob/master/ql/processes/all.hpp, which is pulling a lot of the stochastic process machinery into one header file for inclusion?

[Mario Carneiro]

Yeah, we do that too, with default.lean files scattered about

[Mario Carneiro]

not so much inside mathlib itself because we want to keep the dependency graph as decoupled as is reasonable

[Mario Carneiro]

but all these lattice theorems have low/similar dependencies so they don't hurt the dependency graph situation too much

[Mario Carneiro]

That said, mathlib has seen many authors with different views on this subject, so some of the judgment calls here are made differently in different parts of the library

[Pieter Cuijpers]

But there seems to be a naming convention for definitions and theorems, right? Just not for files, then? (And where can I find anything regarding such conventions?)

[Moritz Doll]

https://leanprover-community.github.io/contribute/naming.html