build all my code

Stream: lean4

[Kevin Buzzard]

Mathlib seems to ensure that lake build means "build the entire project" by maintaining this ludicrous Mathlib.lean file. I want MyProjectName.lean to be a fun file, not a boring one. Can I have this and also get automation to ensure thatlake build means "build all the lean files in the MyProjectName directory"?

I find it a bit weird that I call my project name Foo and then we're supposed to put all the code in another directory also called Foo. Can I go back to calling it src or is this now out of fashion?

[Kim Morrison]

This is now out of fashion. :-) It's doable in your lakefile, but probably you'll find few examples because it's the sort of thing where it's easier for everyone the more standardised the layout is. Also, lake doesn't expose much API, and the lakefile is not parseable by anyone but lake, and so it's hard for external programs to discover where you've put your sources!

[Adam Topaz]

1. In my projects I have many top-level folders and just add lean_lib declarations in the lake file (with default_target if I want them to build with lake build). Is something like that good enough for you Kevin?

[Kim Morrison]

I'm on my phone and struggling to post a link, but if you search for "globs" on zulip you will find messages explaining how to have lake builds everything.

[Adam Topaz]

@Kevin Buzzard we had this globs trick that Scott mentioned in our copenhagen repo: https://github.com/adamtopaz/CopenhagenMasterclass2023/blob/master/lakefile.lean

[Kevin Buzzard]

So

lean_lib «Condensed» where
  roots := #[`Condensed]

in a lakefile means "make lake build Condensed build the current contents on disc of all the files in the Condensed directory"?

[Mario Carneiro]

no, that will build only Condensed and its transitive dependencies, which is also the default behavior

[Mario Carneiro]

you want globs := #[.andSubmodules `Condensed] to say "build Condensed.* to make this target"

[Kevin Buzzard]

Is it better to override the default behaviour by globbing with .andSubmodules or to have some hook or something which makes the stupid files automatically when I try to compile?

With my UG course I'm constantly addding small files and then I want to check everything builds with mathlib and everything else. I have a habit of not editing user-facing files once they've appeared in main in case the students who don't know git have edited them; I don't want to break git pull in any way (and I never update mathlib either) so the argument for andSubmodules is "one less thing to break".

[Mario Carneiro]

The main advantage of a mathlib-style CI process for Mathlib.lean over using .andSubmodules is that downstream users can use import Mathlib. If you use .andSubmodules then import MyProject will still only load the transitive dependencies of MyProject, and you can also use .submodules and then you don't even need a root file and import MyProject won't work at all.

In other words, unless your project is designed to be a dependency of another project there isn't much downside to using .andSubmodules or .submodules to compile all the lean files in a folder, and this seems like a good choice for bag-o-files "libraries" used as collections of exercises or lecture notes. (Another "advantage" of .submodules is that it allows you to have a library which is mutually incompatible with itself, e.g. if there are multiple variations on a definition in different files, because such projects have no root that imports everything. This doesn't seem like a good idea in general though, I think it confuses some server features that take a global view of the project.)

[Martin Dvořák]

I hate maintaining the "sink file", so most of my projects contains something like:
https://github.com/madvorak/vcsp/blob/095a6c422e204bd75994f31c5bbcfe1a4f5416b6/lakefile.lean#L13