Forgetting to add new files to the project’s root file

Stream: new members

[Isak Colboubrani]

Whenever I add a new file, NewFile.lean, to the project ProjectName using VS Code’s “New File…” command, I also need to remember to manually add import ProjectName.NewFile in the root file ProjectName.lean to have NewFile.lean built by lake build.

This generally works, but it’s easy to forget that second manual step. When that happens, NewFile.lean may appear to work fine in VS Code, yet remain omitted from the lake build.

As a result, lake build won’t flag issues such as the presence of sorry in NewFile.lean, which can falsely suggest that the project is in better shape than it really is.

Am I the only one who sometimes forgets to add new files to the project’s root file?

Is there an effective way to prevent this issue? Something like import ProjectName.* isn’t currently possible?

[Eric Wieser]

You can skip the top level file entirely and tell lake to build all subfiles

[Eric Wieser]

The syntax for doing so depends on if you have a lean or toml lakefile

[Isak Colboubrani]

That's great news!

I'm using the standard lakefile.toml provided by lake new project-name math.

[Eric Wieser]

I believe the syntax is globs = ["MyProject.+"] in the lean_lib target, but I don't remember how to find the docs

[Isak Colboubrani]

I found this: https://github.com/leanprover/lean4/blob/master/src/lake/README.md#defining-build-targets

[Isak Colboubrani]

• globs: An Array of module Glob(s) to build for the library. The term glob comes from file globs (e.g., foo/*) on Unix. A submodule glob builds every Lean source file within the module's directory (i.e., Glob.submodules `Foo is essentially equivalent to a theoretical import Foo.*). Local imports of glob'ed files (i.e., fellow modules of the workspace) are also recursively built. Defaults to a Glob.one of each of the library's roots.

[Eric Wieser]

That's the .lean docs, the .toml ones might not yet exist

[Kevin Buzzard]

The FLT toml looks like https://github.com/ImperialCollegeLondon/FLT/blob/main/lakefile.toml and that builds everything in FLT whether or not it's in that crazy FLT.lean file (which I autogenerate with lake exe mk_all BTW)