Zulip Chat Archive

Stream: lean4

Topic: nix setup for lean4


Joachim Breitner (Nov 16 2022 at 14:48):

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 (Nov 16 2022 at 14:51):

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 (Nov 16 2022 at 14:53):

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 (Nov 16 2022 at 14:56):

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

Sebastian Ullrich (Nov 16 2022 at 15:08):

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.


Last updated: Dec 20 2023 at 11:08 UTC