nix setup for lean4

Stream: lean4

[Joachim Breitner]

Greetings from the Freiburg Lean Hackathon!

I’m following the nix setup instructions for lean4 according to https://leanprover.github.io/lean4/doc/setup.html#nix-setup, but when I run

nix run .#vscode-dev MyPackage.lean

the lean4 extension complains with

You have no default "lean-toolchain" in this folder or any parent folder.

What did I do wrong, and how do I fix it?

[Sebastian Ullrich]

Mmh, I haven't tested vscode-dev in a long time! If you want to use your own VS Code with your own extensions, nix shell .#lean-dev -c code . might be more successful.

[Sebastian Ullrich]

But also mandatory disclaimer that the Nix setup is used (and thus tested) by very few people. I'm always surprised when it's not just me.

[Joachim Breitner]

Ok, that works, it seems, although I have shove vscode hard to use the lean4 extensions, and not the lean extension.

[Sebastian Ullrich]

Interesting, I thought the extensions defaulted to Lean 4 if the current Lean is not definitely Lean 3. Not sure how the Nix setup could interfere there.