`lake` should give a warning when it looks like nothing is imported, by accident

[semorrison]

A pretty common user error in a project Foo is to neither modify Foo.lean to import their "interesting" files e.g. Foo/XYZ.lean nor to use globs := #[.submodules `Foo] in their lean_lib (which, as far as I'm aware, is only discoverable by asking on zulip).

They just leave Foo.lean with its default contents, and get to work in the Foo directory, relying on VSCode to show them errors when they open files.

This has the effect that lake build is essentially a no-op.

This is sufficiently common that I think we need to do something about it. It's good that the default template now has a

-- Import modules here that should be built as part of the library.
import «Foo».Basic

but I think this isn't enough.

Possible solutions:

1. We switch the default lakefile.lean to use globs, e.g. something like:

lean_lib «Foo» where
  -- This setting causes `lake build Foo` to build all `.lean` files in the `Foo/` directory.
  -- You can remove this and instead import only the files you want to build in `Foo.lean`.
  globs := #[.submodules `Foo]

2. We try to detect if the user is confused (e.g. Foo.lean only contains import Foo.Basic, there is no globs setting, but there are other lean files under Foo/), and if so give them explanatory text or a warning.
3. We ship something that automatically updates Foo.lean (lake update-imports??), and warns when it is out of sync, with an option to silence the warning for experts.

(I prefer 1. over 2. over 3.)

[tydeu]

I think one confounding issue here is that, like Python it is not necessarily ideal to have users importing their whole package into a top-level module. Ideally, downstream users are expected to import parts of packages piecemeal as needed, not just import a catch-all root.

[nomeata]

It seems only option 1 comes without extra code and complexity?

I find it a natural default, more sophisticated libraries can change that.

[semorrison]

@tydeu, I think you're making the mistake of optimizing for expert users / complicated projects, rather than for beginners / small projects here. The confounding issue you point out is real, but I don't think warrants not improving life for everyone else.

[tydeu]

@semorrison While I do agree that I (probably mistakenly) lean towards experts, my concern here was one focused on beginners. We do not want to habituate them into catch-all roots. However, the globs idea should work for both here.