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

[JJ]

hi, reusing this thread: why is this? i am still understanding the module system and am a little confused why typing import Foo in a Main.lean file with a Foo.lean next to it does not work. my understanding is that the module system is supposed to reflect the filesystem structure...

[Eric Wieser]

The file being imported has to be referenced in a lean_lib from the lakefile for this to work