How to add more files to build?

Stream: new members

[Jakub Nowak]

I've created new project with lake new project exe. It created files Main.lean, project.lean, and project/Basic.lean. I've tried adding import project to Main.lean, but I got this error on lake build:

❯ lake build
✖ [2/4] Building Main
trace: .> LEAN_PATH=/home/nix/tmp/lean/project/.lake/build/lib/lean /home/nix/.elan/toolchains/leanprover--lean4---v4.26.0/bin/lean /home/nix/tmp/lean/project/Main.lean -o /home/nix/tmp/lean/project/.lake/build/lib/lean/Main.olean -i /home/nix/tmp/lean/project/.lake/build/lib/lean/Main.ilean -c /home/nix/tmp/lean/project/.lake/build/ir/Main.c --setup /home/nix/tmp/lean/project/.lake/build/ir/Main.setup.json --json
error: Main.lean:1:0: unknown module prefix 'project'

No directory 'project' or file 'project.olean' in the search path entries:
/home/nix/tmp/lean/project/.lake/build/lib/lean
/home/nix/.elan/toolchains/leanprover--lean4---v4.26.0/lib/lean
error: Lean exited with code 1
Some required targets logged failures:
- Main
error: build failed

What do I have to do, to make lean find the files?

[Jakub Nowak]

It works fine with lake new project. (it creates Project.lean and Project/Basic.lean instead) Is exe template broken?

[Jakub Nowak]

I've tried reading https://github.com/leanprover/lean4/blob/master/src/lake/README.md#binary-executables to understand what to do, but I have no idea what exactly is "local import" or "fellow module".

[Jakub Nowak]

From what I understand, the documentation says, that the build system should recursively build local imports. But this doesn't seem to be the case. Unless local import is not the same as import statement of local file in the same directory?

[Jakub Nowak]

Or do I have to declare local imports somewhere? But I couldn't find any documentation on it.