Right now if you want to build a specific module, you need to use the syntax lake build Foo.Bar, which does not play well with shell completion which is file-oriented. Can we make the syntax Foo/Bar.lean work there as well? I'm sure this is ambiguous with other things but the presence of .lean at the end should help disambiguate it. It should probably not be the default option in the case of an ambiguity, and an alternative lake build --file Foo/Bar.lean Foo/Baz.lean can be used for e.g. CI scripts that want the file-based resolution without ambiguity.

Also, it would be good if this works even for files outside the module tree, such as lake build test/ring.lean for mathlib4. I am not sure there is any current option which this is equivalent to, but what it should do is build all the dependencies of the file (as specified in the import lines) and then call the equivalent of lake env lean test/ring.lean.