Importing file from same directory

Stream: lean4

[Tanner Duve]

Hey, I have a project I am working on, trying to configure some file dependencies. I have a file called synt.lean, and am creating a new file semantics.lean, both are in the same folder in the same project. When I write "import synt" at the top, it does not recognize it and says no such package exists, when I try import .synt, I get import failed, trying to import module with anonymous name. This happens anytime I try to import a file from the same directory. Is there an issue with how my project is built?

[Kevin Buzzard]

I'm not an expert but in all the imports in all the projects I've seen, the first word is always the project name, and the files in a project called X are always in a directory called X (possibly within a project directory also called X)

[Henrik Böving]

Tanner Duve said:

Hey, I have a project I am working on, trying to configure some file dependencies. I have a file called synt.lean, and am creating a new file semantics.lean, both are in the same folder in the same project. When I write "import synt" at the top, it does not recognize it and says no such package exists, when I try import .synt, I get import failed, trying to import module with anonymous name. This happens anytime I try to import a file from the same directory. Is there an issue with how my project is built?

there are no relative imports, all imports go directory by directory from the top level of your lake project