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