Importing local files help

Stream: new members

[Andy Jiang]

sorry for the basic question but I couldn't figure this out. I have a folder with a main file which lake build can compile. I want to write some auxillary things in another file called Template.lean, but I can't import it in the main file by "import Template". When I call lake build it says it says unknown package. How can I allow lean to import this local file?

[Yaël Dillies]

Importing local files is currently not supported. You have to create a properly formatted project to import files from it.

[Yaël Dillies]

You should follow https://leanprover-community.github.io/install/project.html