lean4 vscode setup?

Stream: lean4

[Daniel Fabian]

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?

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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.

[Sebastian Ullrich]

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

[Daniel Fabian]

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.

[Daniel Fabian]

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

[Miguel Raz Guzmán Macedo]

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

[Julian Berman]

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

[Julian Berman]

(Which appears to work for me)

[Julian Berman]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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.

[Miguel Raz Guzmán Macedo]

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.

[Sebastian Ullrich]

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.

[Sebastian Ullrich]

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

[Miguel Raz Guzmán Macedo]

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!