Using Lake to import std

Stream: new members

[Philip Zucker]

Hi, I'm having difficulty getting the lean4 standard lib to import successfully using lake (or any other method). The repo is here https://github.com/philzook58/philzook58.github.io/tree/master/_notes/Languages/lean/myproject vscode keeps saying unknown package 'Std' . I did add the require to the lakefile.lean I think. Ran lake update and lake build, not sure what else to do

[Kevin Buzzard]

I can't answer your question but you could compare and contrast with mathlib4, which imports std. If you don't get an answer here you could try the lean 4 stream.

[Bolton Bailey]

I am having the same issue. I run lake new Foo, I open the new project in VSCode and I put import Std.Data.Nat.Lemmas at the top of Foo.lean, and I get the error "unknown package Std".

[Bolton Bailey]

The mathlib4 lakefile is totally different from the one I get by default. Should I just replace all of it?

[Bolton Bailey]

Ok I got it working by "restarting the server" by closing and reopening the window.

[Bolton Bailey]

Word to the wise, when lean 4 tells you to restart the server, the VSCode command named "Lean: Restart" doesn't do it, I think it only works for Lean 3 or something.

[Adam Topaz]

FYI: you need “Lean4: Restart server”

[Adam Topaz]

To use Std, just copy and paste the line from mathlib4’s lakefile into the lakefile for your project.

[Adam Topaz]

Specifically the “require std from git …” line

[Bolton Bailey]

Screenshot-2023-05-10-at-10.26.27-AM.png

Why don't I see the command here?

[Bolton Bailey]

I feel like this happens periodically - I search for Lean 4: Restart Server and get no results

[Bolton Bailey]

The command has reappeared now. Seems more likely to be a problem with VSCode than with the Lean extension in particular.