search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
347 stars 70 forks source link

Installing language server on Windows #889

Open FeldrinH opened 2 months ago

FeldrinH commented 2 months ago

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 commented 2 months ago

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

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 commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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.