lake new setup issue

Stream: general

[Greg Shuflin]

Hello, I'm new to lean and playing around with lake.

If I run lake new program exe, this creates a scaffold that looks like:

Main.lean
program.lean
program/
    Basic.lean

(with some other files omitted). This doesn't have an example of Main.lean importing code from program like it would if I had omitted the exe when running the lake command. And indeed, if I try to add import program to Main.lean in the exe-case, lake build fails with an error about program being an unknown module prefix.

I'm not sure why I can't import another lean file in the same directory in the exe configuration.

[Kim Morrison]

Looks like a bug in the exe template, indeed! @Mac Malone?

[Mac Malone]

(The bug here is that Lae should not be generated program.lean / program/ at all. The exe template is just supposed to generate a single Main.lean. The standard template is used to produce both a library an an executable.)