Zulip Chat Archive
Stream: new members
Topic: Issue with imports
Siva Gollapalli (Aug 01 2024 at 01:49):
image.png
Here I have a theorem and it's proof. Now in the right side the VS Code extension of LEAN isn't showing any errors, but when I try to run the command lean <filename> it says import error.
Can someone help me with this
Ira Fesefeldt (Aug 01 2024 at 07:36):
Prefer using lake to build your project via lake build <projectname>
, not lean directly.
I believe, the error comes from executing lean from the wrong folder (you are in a subfolder, while vscode executes it from the root folder). But even if you didn't, there may appear import problems from not properly building your project.
Sebastian Ullrich (Aug 01 2024 at 07:41):
If you do want to run Lean on a single file of a project, use lake lean
Last updated: May 02 2025 at 03:31 UTC