0

I was following the installation guide from the main github page for installing the vscoq 2 beta release:

https://github.com/coq-community/vscoq

I am running it on WSL 2 Ubuntu on Windows 10.

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⊘ removed   coq.8.18+rc1
⊘ removed   coq-stdlib.8.18+rc1
⊘ removed   coqide-server.8.18+rc1
⊘ removed   coq-core.8.18+rc1
∗ installed coq-core.dev
∗ installed coqide-server.dev
∗ installed coq-stdlib.dev
[ERROR] The compilation of vscoq-language-server failed at "/home/username/.opam/opam-init/hooks/sandbox.sh build dune build -p vscoq-language-server --display=short".

#=== ERROR while compiling vscoq-language-server.dev ==========================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.11.2 | https://coq.inria.fr/opam/extra-dev#2023-09-14 15:00
# path        ~/.opam/4.11.2/.opam-switch/build/vscoq-language-server.dev
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p vscoq-language-server --display=short
# exit-code   1
# env-file    ~/.opam/log/vscoq-language-server-73968-c44b86.env
# output-file ~/.opam/log/vscoq-language-server-73968-c44b86.out
### output ###
# -> required by alias language-server/install
# [...]
#     ocamldep language-server/dm/.dm.objs/dm__RawDocument.impl.d
#     ocamldep language-server/dm/.dm.objs/dm__Scheduler.intf.d
#     ocamldep language-server/dm/.dm.objs/dm__SearchQuery.intf.d
#     ocamldep language-server/dm/.dm.objs/dm__Scheduler.impl.d
#     ocamldep language-server/dm/.dm.objs/dm__SearchQuery.impl.d
#     ocamlopt language-server/language/.language.objs/native/language.{cmx,o}
#     ocamldep language-server/vscoqtop/.vscoqtop.eobjs/dune__exe__LspManager.intf.d
#     ocamldep language-server/vscoqtop/.vscoqtop.eobjs/dune__exe__LspManager.impl.d
#     ocamldep language-server/vscoqtop/.vscoqtop.eobjs/dune__exe__Vscoqtop.intf.d
#       ocamlc language-server/vscoqtop/.vscoqtop.eobjs/byte/dune__exe.{cmi,cmo,cmt}
#     ocamlopt language-server/vscoqtop/.vscoqtop.eobjs/native/dune__exe.{cmx,o}



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build vscoq-language-server dev
└─ 
┌─ The following changes have been performed
│ ⊘ remove  coq           8.18+rc1
│ ↗ upgrade coq-core      8.18+rc1 to dev
│ ↗ upgrade coq-stdlib    8.18+rc1 to dev
│ ↗ upgrade coqide-server 8.18+rc1 to dev
└─ 

I ran the following to get that error:

$ opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
$ opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
$ opam pin add coq 8.18+rc1
$ opam install vscoq-language-server
1

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.