NixOS and Lean

Stream: general

[Johan Commelin]

I'm trying out NixOS. What is the recommended way to install VSCode + lean extension (these things try to auto-update, not sure if that plays nice with the nix philosophy)
Similar question for elan. Please share your observations / derivations.

cc: @Gabriel Ebner @Yury G. Kudryashov

[Yury G. Kudryashov]

I don't use vscode. I installed elan from nixpkgs; it downloads lean binaries.

[Adam Topaz]

If you do end up using emacs, the nixos guide is pretty good about explaining the "Nix" way to install emacs packages. (Disclaimer: I haven't used nixos in about 6 months.)

[Chris B]

I think @Sebastian Ullrich is also a nix guy, so he might have some sage advice.

[Gabriel Ebner]

We have elan and vscode packages in nixpkgs. Check the leanproject readme for how to install it mutably. (Now that leanproject development has settled, we should probably add a package to nixpkgs. But quickly the 20.09 freeze is coming..)

[Gabriel Ebner]

I believe we have a declarative way to install vscode extensions using vscode-with-extensions, but I've never used it: https://nixos.wiki/wiki/Vscode
I just use the extension manager in vscode.

[Iocta]

I'm curious if anybody's been able to compile mathlib.

[Mario Carneiro]

CI has

[Mario Carneiro]

I haven't compiled mathlib in a long time

[Jannis Limperg]

As soon as you have elan, compiling mathlib should be just leanpkg build. I do this regularly (not on Nix, but if Nix can install elan, you should be good).

[Johan Commelin]

Thanks for all the responses. I'm going to try this soon!

[Johan Commelin]

I've got elan and VScode running. Thanks for the help!

[Johan Commelin]

It seems that installing python packages is quite messy on NixOS. @Gabriel Ebner @Yury G. Kudryashov do you have a recommended way of installing leanproject?

[Gabriel Ebner]

What is the official name for the leanproject package these days? leanproject, mathlib-tools, mathlibtools?
cc @Patrick Massot

[Patrick Massot]

mathlibtools

[Patrick Massot]

pip won't allow a dash in a package name.

[Gabriel Ebner]

This is what I've been using:

nix-env -if https://github.com/leanprover-community/mathlib-tools/archive/master.tar.gz

[Johan Commelin]

https://pypi.org/project/mathlibtools/

[Gabriel Ebner]

But we might want to get it into nixpkgs.

[Johan Commelin]

Sounds good

[Patrick Massot]

I don't insist on any name here, they are all historical accidents.

[Patrick Massot]

And I'm sorry the current names are confusing.

[Gabriel Ebner]

https://github.com/NixOS/nixpkgs/pull/96608

[Johan Commelin]

Cool! You already merged it :grinning_face_with_smiling_eyes:
Thanks @Gabriel Ebner