Zulip Chat Archive

Stream: new members

Topic: Organization of Mathlib


view this post on Zulip Brent A Ritterbeck (Oct 20 2020 at 01:10):

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.

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:33):

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

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:33):

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

view this post on Zulip Brent A Ritterbeck (Oct 20 2020 at 01:51):

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?

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:52):

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

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:53):

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

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:54):

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

view this post on Zulip Mario Carneiro (Oct 20 2020 at 01:55):

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


Last updated: May 13 2021 at 04:21 UTC