Installing language server on Windows

[FeldrinH]

I am trying to use VsCoq with the new language server and Coq installed using Coq Platform on Windows (not WSL). The readme (https://github.com/coq-community/vscoq?tab=readme-ov-file#installing-the-language-server) recommends installing Coq and the language server with opam, but I don't use or have opam, because I installed Coq using the Coq Platform installer.

What is the intended way to install the language server in this case? Am I forced to use opam? Does opam even work on Windows without WSL (I've found a lot of conflicting info about this online)? Is my setup just unsuported?

[bjartem]

The instructions for compiling from sources using opam on cygwin has this bullet point:

• The resulting Coq installation is opam based and best used from the Cygwin prompt (started via C:<your_coq_platform_Cygwin_path>\Cygwin.bat)

To successfully run that script from Command Prompt I had to set the HOME environment variable to the point to the user created inside the same directory structure as the script:

set HOME=C:\<your_coq_platform_Cygwin_path>\home\<your_username>

Then the script can be run:

C:\<your_coq_platform_Cygwin_path>\Cygwin.bat

The script launches a Bash terminal where the opam and vscoqtop commands are available.
The path that I had to set in the VsCoq settings was this:

"C:\<your_coq_platform_Cygwin_path>\CP.2023.11.0~8.18~2023.11\bin\vscoqtop.exe"

I hope this gets smoother in the future. I don't think the average Window user of Coq can be expected to jump through these hoops.

[FeldrinH]

This does seem fairly convoluted. Also, I noticed this somewhat discouraging note in the build instructions:

The build time is between 1..5 hours, depending on CPU speed and RAM size.

Is this the easiest option to get VsCoq working natively on Windows or is there some better alternative? Is it better to just use WSL and live with the extra layer of virtualization?

[gares]

I think we should ship vscoq in the platform binary installers.

Note that building the entire platform takes time, but you can easily select a smaller portion of it.

[rtetley]

Yes there are plans to ship vscoq in the platform binary installers. It should happen in the not so distant future ! This will make the experience much smoother.