NB (Sep 26 2023 at 08:45): 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?
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.
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.
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).
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
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
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)
Pierre Roux (Oct 21 2023 at 07:28):You just need to avoid Coq 8.17.0 (8.17.1 is fine)
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!
Pierre Roux (Oct 23 2023 at 14:29):No idea, I would expect the memory consumption to be similar but I could be wrong.
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: Oct 13 2024 at 01:02 UTC