Trouble installing coq-core on Windows

Using Coq
1

I am trying to install coq-lsp on Windows, and because of that I need to install coq-core. I have successfully installed opam using Cygwin, but now I am trying to install coq-core and am getting this error message:

image
image2815Ă—1317 251 KB

I have successfully installed zarith though, and can find dllzarith.so. Do I need to copy it to a certain directory? What should I do to fix this? Let me know of any more details that are needed.

2

Are you installing Windows native or Windows WSL? They are very different environments. Your output (the “WSL”) suggests the latter but “dllzarith.so” suggests Windows native.

Installing Coq through Coq platform (the recommended way to install) should install coq-core IIUC.

3

I am installing it on native Windows. If coq-core is installed then opam is not finding it when I try to install coq-lsp.

4

It may be easier to debug opam. The windows version of opam was somewhat broken a year or two ago. It may be better now. And if not, maybe worth submitting an issue.

Alternatively, you might want to consider using WSL, which I’ve been using for a couple years now. I’ve found it’s a more stable and predictable environment. Since it’s Linux, it’s very similar to what the majority of Coq developers use. AFAIK none of them use native Windows as their development platform, so few people who can help you debug native Windows issues.

5

Hi @kalyani.tt ,

we are trying to provide a better install system for coq-lsp + windows soon, for now I think the easiest is to use the Coq Platform, as stated in the README.

Thus:

  • install the Coq Platform with OPAM as outlined here
  • then try compile coq-lsp

Don’t hesitate to stop by our Zulip to ask for help.

6

Thank you, I will try that out.

1 Like