Stream: Coq users

Topic: Install Coq-LSP on Windows


view this post on Zulip NB (Sep 26 2023 at 08:45):

Hello, I'm new to coq and would like to ask for advices. If I understand correctly, opam is only available on Linux, so Windows users can't install the lsp? How could I overcome this, should I downgrade coq and install vscoq legacy?

view this post on Zulip Karl Palmskog (Sep 26 2023 at 08:51):

VsCoq legacy works on 8.18 (and earlier). Some people use opam inside WSL2 and then use a VS Code remote extension to get Coq+opam into VS Code that runs on Windows.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 26 2023 at 10:18):

Hi @NB , coq-lsp install on windows is indeed not the easiest , tho with the new Coq platform for 8.17 having been released things are easier now, tho it is unfortunate we didn't manage to add coq-lsp to that release. If you are feeling bold, you can try the instructions in the README , use the v8.17 branch and Coq platform 2023.03.0 .

The upside is that once you have done that process, it has been reported to work pretty well and can be run from the explorer shell which is very convenient!

We hope to provide better installers soon tho.

view this post on Zulip Théo Zimmermann (Sep 26 2023 at 12:45):

Something to clarify is that coq-lsp and VsCoq are two separate projects. From the initial question, it appears that there is a confusion as the VsCoq extension does not require the coq-lsp server, but its own LSP server (when using VsCoq >= 2.0).

view this post on Zulip Patrick Nicodemus (Oct 20 2023 at 22:48):

i use wsl2 and I'm mostly happy with it. you can ask me if you have questions but I'm not an expert, just a casual user

view this post on Zulip Karl Palmskog (Oct 20 2023 at 22:53):

main WSL2 gotcha these days is arguably that MathComp2 barely builds with 8GB physical memory on a Windows machine (then WSL2 gets maybe 4GB, which may not be enough). But on a 16GB machine I didn't hit any issues yet with WSL2

view this post on Zulip Pierre Roux (Oct 21 2023 at 07:27):

Karl Palmskog said:

main WSL2 gotcha these days is arguably that MathComp2 barely builds with 8GB physical memory on a Windows machine (then WSL2 gets maybe 4GB, which may not be enough). But on a 16GB machine I didn't hit any issues yet with WSL2

That's no longer true, with latest coq-elpi and HB, mathcomp master (and 2.1 to be released soon) is way below 1.5 GB (in make -j1 at least). (I'm myself using WSL2 (I mean, other that it's quite unstable) without issue and frequently use make -j5 though)

view this post on Zulip Pierre Roux (Oct 21 2023 at 07:28):

You just need to avoid Coq 8.17.0 (8.17.1 is fine)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2023 at 14:22):

I do wonder how these numbers look for the native Coq Windows version, out of curiosity of course!

view this post on Zulip Pierre Roux (Oct 23 2023 at 14:29):

No idea, I would expect the memory consumption to be similar but I could be wrong.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2023 at 14:39):

We'll soon have the infra to actually measure that, let's see!


Last updated: Jun 23 2024 at 04:03 UTC