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

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.)