Lake, libraries, and VSCode (for Mathlib4)

Stream: new members

[Daniel Patterson]

This is probably a noob question, but I searched around and didn't see an answer! I have a project with a pretty bare-bones lakefile.lean -- it installs mathlib4, and that's about it.

I then built a particular part of Mathlib I wanted to try (the linarith tactic); not sure if this was necessary, but seemed to work, with lake build Mathlib.Tactic.Linarith.

I then imported that module into the main file for my project, and I can lake build and it works (and I have a trivial proof that uses it, and I assume that means it is working? I changed it to something garbage, and get output on the commandline that linarith failed).

The problem is that VSCode gives an error on the import. Obviously, something is wrong with the path that it's using. I don't think I set up anything funny in the VSCode extension (use lake is enabled).

Assuming this can be fixed, I'm also wondering, just more generally, how the path is manipulated by lake. Will any .lean file in the same directory as the lakefile.lean pick up the settings (that would be ideal). Subdirectories too?

Thanks in advance.

[Martin Dvořák]

What does lake do?

[Reid Barton]

Are you opening the directory in VS Code?