search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
152 stars 31 forks source link

installing coq-lsp on windows #481

Closed ASamSam closed 1 year ago

ASamSam commented 1 year ago

Hello, It is hard to me to setup coq-lsp. First, i did compile cygwin build as suggested in the installation guide for windows. It builds Coq 8.16.1 then i did try to get the main branch as zip - can`t compile it because vendor coq is not included.

then took the tag 0.1.6.1+8.16 with Github desktop. executed make submodules-init and call make. result: Error: Library "ppx_sexp_conv" not found. -> required by _build/default/vendor/coq-serapi/sertop/sercomp.exe -> required by _build/install/default/bin/sercomp.exe -> required by _build/default/vendor/coq-serapi/coq-serapi.install File "controller/dune", line 4, characters 27-42: 4 | (libraries coq fleche lsp dune-build-info)) ^^^^^^^^^^^^^^^ Error: Library "dune-build-info" not found. -> required by library "controller" in _build/default/controller -> required by executable coq_lsp in controller/dune:7 -> required by _build/default/controller/coq_lsp.exe -> required by _build/install/default/bin/coq-lsp.exe -> required by _build/default/coq-lsp.install File "vendor/coq-serapi/sertop/dune", line 12, characters 25-35: 12 | (preprocess (staged_pps ppx_import ppx_sexp_conv)) ^^^^^^^^^^ Error: Library "ppx_import" not found. -> required by _build/default/vendor/coq-serapi/sertop/.merlin-conf/exe-sertop_bin-cea70dd0b7eed1178ac7bb4aff6fbd91 -> required by _build/default/vendor/coq-serapi/sertop/sercomp.exe -> required by _build/install/default/bin/sercomp.exe -> required by _build/default/vendor/coq-serapi/coq-serapi.install File "lang/dune", line 4, characters 12-15: 4 | (libraries uri coq-core.library)) ....

Error: Library "sexplib" not found. -> required by library "coq-serapi.serlib.ltac2" in _build/default/vendor/coq-serapi/serlib/plugins/ltac2 -> required by _build/default/vendor/coq-serapi/META.coq-serapi -> required by _build/install/default/lib/coq-serapi/META -> required by _build/default/vendor/coq-serapi/coq-serapi.install File "vendor/coq-serapi/serlib/plugins/micromega/dune", line 6, characters 46-53: 6 | (libraries coq-core.plugins.micromega serlib sexplib)) ^^^^^^^ +

`Error: Library "ppx_import" not found. -> required by _build/default/vendor/coq-serapi/serlib/plugins/zify/.merlin-conf/lib-coq-serapi.serlib.zify -> required by _build/default/vendor/coq-serapi/serlib/plugins/zify/serlib_zify.a -> required by _build/install/default/lib/coq-serapi/serlib/zify/serlib_zify.a -> required by _build/default/vendor/coq-serapi/coq-serapi.install File "vendor/coq/theories/dune", line 2, characters 0-588: 2 | (coq.theory 3 | (name Coq) 4 | (package coq-stdlib) .... 28 | 29 | coq-core.plugins.ssreflect 30 | coq-core.plugins.derive)) Error: Anomaly "Uncaught exception Failure("Config file not found - neither C:\lib\findlib.conf nor the directory C:\lib\findlib.conf.d")." Please report at http://coq.inria.fr/bugs/.

make: *** [Makefile:19: build] Error 1`

Alizter commented 1 year ago

Hi which branch are you using for coq-lsp? There is a 0.1.6.1 branch for 8.16.

ASamSam commented 1 year ago

i did use tag '0.1.6.1+8.16' now i`m trying to install 8.16 branch.

i see, that I can install missed libraries manually. Maybe I missing some step?

ASamSam commented 1 year ago

ok, after installing libs - this problem remains:

$ make
dune build  vendor/coq/coq-core.install vendor/coq/coq-stdlib.install vendor/coq-serapi/coq-serapi.install coq-lsp.install
File "vendor/coq/theories/dune", line 2, characters 0-588:
 2 | (coq.theory
 3 |  (name Coq)
 4 |  (package coq-stdlib)
....
28 |
29 |    coq-core.plugins.ssreflect
30 |    coq-core.plugins.derive))
Error:
Anomaly
"Uncaught exception Failure("Config file not found - neither C:\\lib\\findlib.conf nor the directory C:\\lib\\findlib.conf.d")."
Please report at http://coq.inria.fr/bugs/.

File "_none_", line 1:
Warning 58 [no-cmx-file]: no cmx file was found in path for module Build_info__Build_info_data, and its interface was not compiled with -opaque
make: *** [Makefile:19: build] Error 1
ASamSam commented 1 year ago

after copying coq lib folder to C:

`dune build vendor/coq/coq-core.install vendor/coq/coq-stdlib.install vendor/coq-serapi/coq-serapi.install coq-lsp.install File "vendor/coq/user-contrib/Ltac2/dune", line 1, characters 0-167: 1 | (coq.theory 2 | (name Ltac2) 3 | (package coq-stdlib) 4 | (synopsis "Ltac2 tactic language") 5 | (flags -w -deprecated-native-compiler-option) 6 | (libraries coq-core.plugins.ltac2)) Error: Can't find file number_string_notation_plugin.cmxs on loadpath.

make: *** [Makefile:19: build] Error 130 `

seems, it uses wrong path somewhere

Alizter commented 1 year ago

That looks like findlib and OCAMLPATH are not set up properly to me. Are you using opam?

ejgallego commented 1 year ago

Hi @ASamSam , indeed it is not easy to get things running in Windows yet, there is a Pull Request that builds the stuff for windows so it could downloaded easily, but there is some trouble.

I'd reproduce the steps I do to get things working on Win:

  1. install the Coq platform, including coq-serapi
  2. checkout the v8.16 branch of coq-lsp, beware that no submodules are needed, also Coq should not be installed
  3. once you do the checkout, make sure the deps for coq-lsp are fine using opam install --deps-only . in coq-lsp sources
  4. then make should work

So indeed it seems to me that something went wront at step 1 , can you provide more details on how did you do it.

Maybe the best way to move forward here is to actually try to use the Coq Platform for 8.17 , which will have coq-lsp working out of the box , I cc @MSoegtropIMC in case he'd like to provide us with the right pointers on the 8.17 Coq Platform branch, so you could try the installer generated from that branch.

ASamSam commented 1 year ago

Thank you very much, i`ll try install 8.17 little bit later, yet it is not officially released yet. for step 1 i did use the link proposed in LSP installation doc. It were building the platform for several hours: https://github.com/coq/platform/blob/main/doc/README_Windows.md#installation-by-compiling-from-sources-using-opam-on-cygwin

ejgallego commented 1 year ago

Thanks, can you try to remove the coq-lsp directory and checkout the v8.16 branch again?

There should be no vendor directory, so maybe the checkout got messed up by the submodules.

ASamSam commented 1 year ago

thank you for help. first of all: got this message - $ opam install --deps-only coq-lsp --> [ERROR] No package named coq-lsp found.

Then i see why i come to failed state before: i did use 'GitHub desktop with the selected tag, expecting that it will download the desired state. But seems it downloads the main brunch instead

ejgallego commented 1 year ago

This is because the opam repository for windows is not updated too often, you can try:

$ git clone -b v8.16 https://github.com/ejgallego/coq-lsp.git
$ cd coq-lsp && opam install --deps-only .
ASamSam commented 1 year ago

i did manage to compile coq-lsp and did install VS code extension (not clear rot me, why I can't install it for VS community.. but it doesn't matter). did setup the path in VS code in coq-lsp section and put the libgmp-10.dll near to exe. now I have this problem: [Error - 11:38:04 PM] Coq LSP Server client: couldn't create connection to server. Launching server using command C:\cygwin64_coq\home\andre\coq-lsp-016-816\_build\install\default\bin failed. Error: spawn C:\cygwin64_coq\home\andre\coq-lsp-016-816\_build\install\default\bin ENOENT

ejgallego commented 1 year ago

Great @ASamSam !!

It seems to me that the path should be : 

C:\cygwin64_coq\home\andre\coq-lsp-016-816\_build\install\default\bin\coq-lsp.exe

The name of the binary seems to be missing.

ASamSam commented 1 year ago

You are right, it helps. i have empty file 'c:/KI/ArkiScripts/arki/utils/FSM/COQ/V/test.v'

Then got this log (I did enable debug):

`[Info - 1:52:51 PM] Server initialized [Trace - 1:52:51 PM] Sending notification 'textDocument/didOpen'. [Trace - 1:52:51 PM] Sending request 'proof/goals - (1)'. [Trace - 1:52:51 PM] Sending request 'textDocument/documentSymbol - (2)'. [Trace - 1:52:51 PM] [workspace]: initialized /c:/KI/ArkiScripts [Trace - 1:52:51 PM] Received notification 'window/logMessage'. [Info - 1:52:51 PM] Configuration loaded from Command-line arguments

ejgallego commented 1 year ago

You are almost there!

You need to pass the --ocamlpath=c:\cygwin64_coq\home\andre\.opam\__coq-platform.2022.09.18.162022.09\lib argument in settings as instructed in the readme.