Changing the default behavior of `lake build`

Stream: general

[Eric Wieser]

Eric Wieser said:

Annoyingly these users often claim their code does compile, and then you have to explain "no, lake build didn't build your files because you didn't tell it about them"

@Mac Malone, what would your thoughts be on having lake new default to MyProject.+ as the glob, to avoid this class of mistake?

[Mac Malone]

@Eric Wieser The goal is generally to encourage users to think about what imports they include in their top-level modules. As with Python libraries, not every import should necessarily be part of the default import <lib-name>, but such a module should usually exist. The new module system will hopefully also encourage more consideration about what imports (and what kind of imports) to include. Globs are often used to do the opposite, hence I would be wary using them in the default template.

[Mac Malone]

(Though, technically, it is possible to have well-designed top-level modules and use globs.)

[Eric Wieser]

Mac Malone said:

not every import should necessarily be part of the default import <lib-name>

I agree with this, but I think I claim that lake build should still build all the submodules. Maybe I should have said MyProject.*?

[Mac Malone]

If this path were to be taken -- building everything in the directory as the library by default -- I would lean towrards changing the lean_lib default for globs to <lib-name>.* rather than changing the default template.

[Notification Bot]

5 messages were moved here from #general > Alleged Collatz Conjecture proof by Eric Wieser.

[suhr]

Maybe there should be lake check in addition to lake build, like there's cargo check in Rust.

[Pim Otte]

This particular case could also be solved by having lake build output something like "Built x files" (a little bit like the ephemeral output that is already there when you're actually building something)

[Shreyas Srinivas]

Pim Otte said:

This particular case could also be solved by having lake build output something like "Built x files" (a little bit like the ephemeral output that is already there when you're actually building something)

The output would be too large for even a self-contained formalisation project

[Pim Otte]

To clarify, I don't mean doing printing all of 1/1337 to 1337/1337, but just one final line at the end, reporting the final number, 1337 in this case.

[Weiyi Wang]

or could it do the other way: output the name of .lean files that it didn't build?

[Eric Wieser]

What's the situation where you don't want it to build every lean file?