Zulip Chat Archive

Stream: lean4

Topic: lean4 vscode setup?


view this post on Zulip Daniel Fabian (Mar 13 2021 at 12:41):

I was hoping to play around with lean4 a little but I'm hitting some stumbling blocks. First of all, I don't use linux as my desktop, but windows. So, I necessarily need vscode remote. My options are WSL2 or a linux container running on a linux server both of which I ssh into with vscode running on my desktop. So far, I've managed to set it up with Ubuntu and remoting into that.

I can get nix working in it, but don't quite understand how that would interact with nix-shell. Given that the correct setup would only be available from within the nix-shell but then I don't think I can remote into that?

Has anyone managed to get vscode remote working with the nix setup? My server is a NixOS server where I created an Ubuntu container, just because it's easiest to get vscode remote working that way. Which means for now, I only managed to get the "basic setup" working.

Which leads me to the 2nd issue I have. Even though I've managed to get lean4 nightly builds to work, the lean4 info view seems to be empty very often when I put the cursor into any one function. When should we see the proof state?

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 12:53):

To answer your second question first: the proof state is only available on tactics at the moment

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 13:00):

Note that it is definitely possible to run the basic setup on Windows directly (our CI does so for every commit), though leanpkg requires sh, git, and make in the PATH. I think people had success using msys2 for that.

view this post on Zulip Sebastian Ullrich (Mar 13 2021 at 13:04):

There is a VS Code extension for entering nix-shells, apparently compatible with WSL, but I haven't tried it yet. https://marketplace.visualstudio.com/items?itemName=arrterian.nix-env-selector

view this post on Zulip Daniel Fabian (Mar 13 2021 at 13:05):

Oh I believe that it's possible. Just that I prefer a real linux environment for linux-y projects. And lean definitely qualifies. Also, I have the server on a more powerful machine in a different room, so linux is fine. Just that my desktop is windows. I quite like using linux for development.

view this post on Zulip Daniel Fabian (Mar 13 2021 at 13:05):

oh cool, thanks, I'll play around with it.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 11 2021 at 19:13):

I'm getting this error after following the manual step by step on Manjaro:

[nix-shell:~/projects/mypkg]$ nix run .#vscode-dev MyPackage.lean
error: builder for '/nix/store/pmhj1v7jz7vkr8iccsq352w57gfhsc3c-VSCode_1.52.1_linux-x64.tar.gz.drv' failed with exit code 1;
       last 7 log lines:
       >
       > trying https://vscode-update.azurewebsites.net/1.52.1/linux-x64/stable
       >   % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
       >                                  Dload  Upload   Total   Spent    Left  Speed
       >   0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
       > curl: (22) The requested URL returned error: 404 Not Found
       > error: cannot download VSCode_1.52.1_linux-x64.tar.gz from any mirror
       For full logs, run 'nix log /nix/store/pmhj1v7jz7vkr8iccsq352w57gfhsc3c-VSCode_1.52.1_linux-x64.tar.gz.drv'.
error: 1 dependencies of derivation '/nix/store/8mbgdq37xd1h758hxx0blbfdgwayibas-vscode-1.52.1.drv' failed to build
error: 1 dependencies of derivation '/nix/store/2imyr3wwb4hxmik1z0k8p7haqn9hlimd-vscode-with-extensions-1.52.1.drv' failed to build
error: 1 dependencies of derivation '/nix/store/w6bif8i5b2s011lmyj7i280qk3akjfiy-vscode-dev.drv' failed to build

view this post on Zulip Julian Berman (Apr 11 2021 at 19:46):

I don't know anything about the setup but google finds https://github.com/microsoft/vscode/issues/120171 -- tl;dr that looks like it needs to be changed to link instead to https://update.code.visualstudio.com/1.52.1/linux-x64/stable

view this post on Zulip Julian Berman (Apr 11 2021 at 19:46):

(Which appears to work for me)

view this post on Zulip Julian Berman (Apr 11 2021 at 19:50):

And which looks like is fixed in nixpkgs I think -- https://github.com/NixOS/nixpkgs/pull/117479/files not sure what needs running to get that change

view this post on Zulip Sebastian Ullrich (Apr 11 2021 at 20:57):

(see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Lean.20should.20update.20flake.2Elock.20file)

view this post on Zulip Sebastian Ullrich (Apr 11 2021 at 21:04):

I added a separate, newer nixpkgs just for vscode to get things working again for now

view this post on Zulip Sebastian Ullrich (Apr 11 2021 at 21:09):

To be honest, I'm not sure whether we should keep the pinned VS Code. The fact that you cannot install any further extensions into it makes it much less useful than emacs-dev. But being able to launch a fully set up instance with a single command is still pretty cool, I have to admit.

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 11 2021 at 22:15):

Thanks Sebastian. I don't mind switching to emacs - is that plugin much more polished?
I'm using Doom Emacs and would appreciate any pointers for Lean4 with Dook Emacs.

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 07:13):

Oh, I didn't mean to imply that anyone should give up on VS Code. It is definitely possible to use a separate VS Code installation with the Nix setup, see the middle part of https://leanprover.github.io/lean4/doc/setup.html#basic-commands. The Emacs and VS Code extensions are roughly equal at the moment.

view this post on Zulip Sebastian Ullrich (Apr 12 2021 at 07:18):

For Doom Emacs I use something equivalent to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Doom.20Emacs.20setup/near/224678160 - though I don't think you should need any but the last package! declaration

view this post on Zulip Miguel Raz Guzmán Macedo (Apr 12 2021 at 16:50):

FWIW with the latest nix build, I get the following error in the goal view in VSCode when placing my cursor in teh first line of a theorem:

Error updating: {"code":-32601}.Try again.
No info found.

#eval 2+2 works though!


Last updated: May 07 2021 at 12:15 UTC