Zulip Chat Archive

Stream: new members

Topic: Importing local files help

Andy Jiang (Dec 18 2023 at 14:56):

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 (Dec 18 2023 at 14:57):

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

Yaël Dillies (Dec 18 2023 at 14:58):

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

Last updated: Dec 20 2023 at 11:08 UTC