purpose of Mathlib.lean file?

Stream: mathlib4

[Scott Morrison]

In the mathlib4 repository ci, we run

find Mathlib -not -type d | sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

[Scott Morrison]

and require that this doesn't change Mathlib.lean. Why are we doing this?

[Scott Morrison]

It just seems an unnecessary hurdle for someone adding a new file. (e.g. I had added Test/Split.lean, and amongst other reasons this check broke the build).

[Mario Carneiro]

As the CI says, it's checking that every file is imported from Mathlib.lean. @Gabriel Ebner might have more to say about this, but my guess is that this is needed so that we actually compile everything rather than getting a spurious green checkmark for an incorrect file that is not imported anywhere

[Daniel Selsam]

@Scott Morrison Leanpkg expects there to be a <package-name>.lean in the same directory as the leanpkg.toml file, and for all files in the package to be (recursively) imported from this file. FWIW I think it is an unfortunate design that currently, all ancestor files in Mathlib4 are imported together at the top-level like this. I would a priori suggest creating a file for each subdirectory that imports the .lean files in that subdirectory.

[Mario Carneiro]

lean 3 doesn't need this because lean --make will automatically compile all .lean files in the directory

[Daniel Selsam]

Daniel Selsam said:

FWIW I think it is an unfortunate design that currently, all ancestor files in Mathlib4 are imported together at the top-level like this. I would a priori suggest creating a file for each subdirectory that imports the .lean files in that subdirectory.

This is what is done in Lean4. For example, the Lean/Meta/ directory has a corresponding Lean/Meta.lean that imports the lean files in Lean/Meta/: https://github.com/leanprover/lean4/blob/master/src/Lean/Meta.lean

[Mario Carneiro]

Regarding test files specifically, I think we need an exemption, together with a separate CI job for tests

[Mario Carneiro]

@Daniel Selsam the CI script for that sounds more complicated. Does lean 4 have a CI script checking that all those files are exhaustive?

[Scott Morrison]

Couldn't we just have CI prepare this file? Having the build fail because you forgot to generate an automatically generated file yourself seems annoying. :-)

[Mario Carneiro]

I was thinking about that, but it won't work locally either without the file, and having people learn how to run the CI scripts locally also sounds error prone

[Scott Morrison]

Sounds like we want lean --make again. :-)

[Scott Morrison]

In any case, very often it wouldn't even occur to me to want to compile everything locally before feeding things to CI, so it's not even clear that the local file is needed.

[Mario Carneiro]

we want leanpkg build or whatever the nextgen version of that is to just work after someone clones mathlib4

[Mario Carneiro]

Using Default.lean files like daniel describes would be better, although it is also more constraining compared to lean 3 default.lean files, which often but not always import everything in the directory

[Mario Carneiro]

with lean 4 we would have to ensure (via a similar CI script) that default files always import everything in the directory

[Mario Carneiro]

then again I think the added flexibility isn't particularly critical

[Scott Morrison]

I really don't like the burden being on the user to modify Mathlib.lean (or a bunch of Default.lean files) when they add a new file. I'd even prefer CI adding a commit itself if necessary.

[David Renshaw]

I've been using leanmake -j, and it seems to build everything, regardless of what's in Mathlib.lean.

[Gabriel Ebner]

Scott Morrison said:

and require that this doesn't change Mathlib.lean. Why are we doing this?

At some point Sebastian changed leanpkg build so that it only builds files that are (transitively) imported from the Mathlib.lean file. This check makes sure that everything is imported. I don't care if this is "unfortunate" or if "one file per directory would be more beautiful". It would be worse if we had files that silently break and CI doesn't notice it because we forgot to import them.

[Gabriel Ebner]

OTOH, it looks like leanpkg build now builds everything under Mathlib (since it found the Test/Split.lean file even though it wasn't imported). So maybe we can just remove that CI step altogether.

[Mac]

Gabriel Ebner The specific behavior of leanpkg currently, I believe, is as follows. If you run leanpkg build (i.e. perform an in-Lean build), it builds all transitive imports of the root .lean. However, f you run leanpkg build bin/lib (i.e., invoke leanmake and use its Makefile) it builds a .lean files in the package directory (ex. the one with the same name as root .lean).

[Mac]

Specifically, see this line of the leanmake Makefile which states: "We compile all source files in $PKG/ as well as $PKG.lean. $PKG is also used for naming binary files." This line of Leanpkg.lean set the PKG variable (to the name of the root .lean).

[Mac]

Conversely, in Build.lean (where the in-Lean build of the bareleanpkg build is defined) these lines use the imports to determine what to build.