Lean 4 VS Code extension help requestered squigly on im...

Stream: lean4

[Alex Kassil]

Hello! I am able to build a lean 4 project locally with lake build, but the lean 4 vs code extension is giving me trouble. I can't get imports to work with the vs code extension.

Here is a simple repro of what doesn't work for me:

lake new test
Open up the generated Main.lean file
red squigly over import example.png

Any tips/insights?

[Alex Kassil]

In case it's relevant, I am on ubuntu 18.04 LTS. The lean4 extension works totally fine when I keep to a single file

[Notification Bot]

Alex Kassil has marked this topic as resolved.

[Notification Bot]

Alex Kassil has marked this topic as unresolved.

[Alex Kassil]

I also get this error Error updating: Error fetching goals: Rpc error: InvalidParams: Incorrect position 'file:///home/alex/Desktop/Stuffs/programming/lean4/test/Main.lean:4:0' in RPC call. Try again. when I follow Error updating: Error fetching goals: Rpc error: InvalidParams: Incorrect position 'file:///home/alex/Desktop/Stuffs/programming/lean4/test/Main.lean:4:0' in RPC call. Try again. when I https://github.com/leanprover/vscode-lean4#lean-editing-features follow this and use the Lean 4: Refresh File Dependencies command in vs code

[Kevin Buzzard]

You need to open the folder corresponding to your project using VS Code's "open folder" functionality. Looks to me like you used this functionality to open the directory containing all your lean projects.

[Arthur Paulino]

Tô follow Kevin's advice on your terminal:

lake new test
cd test
code .

That will create the new Lake project, enter the project directory and then open VS Code on that directory