mathlib4 in vscode

Stream: lean4

[Connor Gordon]

I've been attempting to learn Lean 4 lately, and one step I'm having trouble with is getting Mathlib to work. I followed the instructions here and lake build is successfully running, but if I put import Mathlib into a file I get the error unknown package 'Mathlib'.

For more information, my lakefile.lean looks like

import Lake
open Lake DSL

package testing {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib Testing {
  -- add any library configuration options here
}

Any ideas what I'm doing wrong?

[Kevin Buzzard]

I have a working Lean 4 project which depends on mathlib and my lakefile looks lite this:

import Lake
open Lake DSL

package «iISc-experiments» {
  -- add any package configuration options here
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «IIScExperiments» {
  -- add any library configuration options here
}

I have no idea whether the funny French quotes make any difference, but everything else looks the same. Are you opening the root directory of the project in VS Code using its "open folder" functionality? That's what seems to trip a lot of people up.

[Connor Gordon]

Ack, I had the folder containing the project rather than the project folder itself. Opening the correct folder fixed it; thanks!