Mathematics in Lean / unknown package 'Mathlib'

Stream: new members

[Alexander Hicks]

Hi,

I've been meaning to play aroud with Lean (I've previously worked with Isabelle) and thought I would start by looking at the examples from the Mathematics in Lean book. I've followed the instructions (https://github.com/leanprover-community/mathematics_in_lean) to set up vscode and the book's repository, but unfortunately I keep getting "unkown package" errors for Mathlib as well as MIL packages. I also get a warning that the opened folder if not a valid Lean 4 project because it does not contain a lean-toolchain file, but the MIL repository obviously does contain a lean-toolchain file. Any ideas what might be causing this and how to resolve the issue? Thanks!
Screenshot-from-2024-03-08-14-50-15.png

[Ruben Van de Velde]

Did you open the root folder of the project in vs code?

[Ruben Van de Velde]

And are there local changes to lean-toolchain and lake-manifest.json? If so, you might want to revert those

[Alexander Hicks]

I believe I've opened the root folder in vs code (i.e., ran code .. from the mathematics_in_lean folder). I did make some changes to lean-toolchain, trying both leanprover/lean4:v4.6.0 and leanprover/lean4:v4.6.1-rc (iirc) as it was suggested when I ran lake exe cache get (the issues existed in both cases).

[Ruben Van de Velde]

You should run code . with just the one dot

[Alexander Hicks]

That works, thank you! I hadn't realised the second . in the docs was just a regular end of sentence . .

[Ruben Van de Velde]

Do you remember where you saw that sentence? That sounds like something we could rephrase

[Alexander Hicks]

Here: https://leanprover-community.github.io/install/project.html#working-on-an-existing-project. The line is "Launch VS Code, either through your application menu or by typing code .. (MacOS users need to take a one-off extra step to be able to launch VS Code from the command line.)"

[Ruben Van de Velde]

https://github.com/leanprover-community/leanprover-community.github.io/pull/450

[Alexander Hicks]

Definitely looks clearer. Thanks!