Hjalte Sorgenfrei Mac Dalland (Feb 02 2023 at 15:09): Hjalte Sorgenfrei Mac Dalland (Feb 02 2023 at 15:09):Hi, i am trying to build and run VSCoq2, but the server crashes when trying to run "textDocumentDidOpen".
The backtrace from vscoqtop is the following:
=========================================================
(Dynlink.Cannot_open_dll "Failure(\"/home/hjadal/.opam/default/lib/coq-core/plugins/ltac/ltac_plugin.cmxs: undefined symbol: camlLocusops__10\")")
Raised at Dynlink_common.Make.load in file "otherlibs/dynlink/dynlink_common.ml", line 330, characters 23-73
Called from Dynlink_common.Make.loadfile in file "otherlibs/dynlink/dynlink_common.ml" (inlined), line 347, characters 26-45
Called from Mltop.PluginSpec.load in file "coq/vernac/mltop.ml", line 168, characters 6-28
Called from Mltop.load_ml_object in file "coq/vernac/mltop.ml", line 318, characters 2-15
Called from Mltop.trigger_ml_object in file "coq/vernac/mltop.ml", line 370, characters 10-77
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Declaremods.StagedMod.do_module in file "coq/vernac/declaremods.ml", line 375, characters 4-34
Called from Library.register_library_syntax in file "coq/vernac/library.ml", line 344, characters 2-81
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Lib.add_leaf in file "coq/library/lib.ml", line 526, characters 2-39
Called from Synterp.vernac_require_syntax in file "coq/vernac/synterp.ml", line 390, characters 2-67
Called from Flags.with_modified_ref in file "coq/lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "coq/clib/exninfo.ml", line 81, characters 4-38
Called from Coqinit.require_file in file "coq/sysinit/coqinit.ml", line 176, characters 2-84
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dm__DocumentManager.init in file "dm/documentManager.ml", line 105, characters 2-33
Called from Dune__exe__LspManager.textDocumentDidOpen in file "vscoqtop/lspManager.ml", line 156, characters 19-63
Called from Dune__exe__LspManager.dispatch_method in file "vscoqtop/lspManager.ml", line 294, characters 30-56
Called from Dune__exe__LspManager.handle_lsp_event in file "vscoqtop/lspManager.ml", line 315, characters 24-62
Called from CList.map in file "coq/clib/cList.ml", line 298, characters 21-24
Called from CList.map_append in file "coq/clib/cList.ml", line 391, characters 29-38
Called from Dune__exe__Vscoqtop.loop.loop in file "vscoqtop/vscoqtop.ml", line 33, characters 22-68
Called from Dune__exe__Vscoqtop.loop in file "vscoqtop/vscoqtop.ml", line 35, characters 6-27
Any idea what I am doing wrong?
Enrico Tassi (Feb 02 2023 at 16:03):Right now we use a submodule for Coq, since some code is not yet integrated in the mainline. My guess is that it is loading a coq plugin installed in yor opam root, in which you also have a mainline coq.
Maxime Dénès (Feb 03 2023 at 08:56):@Hjalte Sorgenfrei Mac Dalland Do you manage to fix your problem? We will provide better build instructions very soon, I hope it will help.
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 09:46):I am using the submodule checkouted at hash c649b8c83d and I don't have anything else related to Coq installed.
So far i have not found anyway to fix it.
I tried to follow ci.yml to build the language server without using Nix.
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 09:48):$ opam list | grep coq
coq dev pinned to version dev at git+file:///home/hjadal/code/vscoq/language-server/coq#HEAD
coq-core dev pinned to version dev at git+file:///home/hjadal/code/vscoq/language-server/coq#HEAD
coq-stdlib dev pinned to version dev at git+file:///home/hjadal/code/vscoq/language-server/coq#HEAD
coqide dev pinned to version dev at git+file:///home/hjadal/code/vscoq/language-server/coq#HEAD
coqide-server dev pinned to version dev at git+file:///home/hjadal/code/vscoq/language-server/coq#HEAD
vscoq-language-server ~dev pinned to version ~dev at file:///home/hjadal/code/vscoq/language-server
What commands did you run after cloning the VsCoq repo?
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 10:21):I installed the packages from default.nix with opam / pacman.
The commands after that was:
$ opam install ./language-server/coq/coq-core.opam ./language-server/coq/coq-stdlib.opam
$ opam install ./language-server/vscoq-language-server.opam
$ (cd client && yarn compile)
Then i used the "Run Extension" task in ./client to start the client after which it crashes because of the error i posted yesterday
Enrico Tassi (Feb 03 2023 at 13:06):can you do coqtop -v and echo Quit. | coqtop ?
Enrico Tassi (Feb 03 2023 at 13:08):The commands you write look good to me, but the ltac plugin fails to load because the coq binary which loads it misses a symbol it expects, which means they are not "in sync". Maybe some attempt resulted in another coq being installed, or maybe another compilation attempt (it can even be the same sources but compiled with different options).
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 13:08):$ coqtop -v
The Coq Proof Assistant, version 8.18+alpha
compiled with OCaml 4.14.0
$ vscoqtop -v
The Coq Proof Assistant, version 8.18+alpha
compiled with OCaml 4.14.0
$ echo Quit. | coqtop
Welcome to Coq :/home/hjadal/.opam/default/.opam-switch/build/coq-core.dev/_build/default,master (c649b8c83d07151f5c7aeeb060cf952367aeb338)
Coq < %
$ echo Quit. | vscoqtop -bt
No output from the last one, which I assume is expected.
Enrico Tassi (Feb 03 2023 at 13:10):Hum, it looks good. Hence my guessing was wrong.
Maxime Dénès (Feb 03 2023 at 13:23):I'll try to reproduce on a fresh VM.
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 13:46):I don't know it has any impact but I am using Arch, kernel 6.1.9-arch1-1. I don't know if the error also occurs on Ubuntu.
Enrico Tassi (Feb 03 2023 at 14:18):The error seems OCaml specific. environment variables could affect it, but not the kernel. I guess you don't have coq or ocaml installed outside the opam root
Maxime Dénès (Feb 03 2023 at 15:41):@Hjalte Sorgenfrei Mac Dalland I forgot to ask the value of vscoq.path in your vscode settings
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 15:50):/home/hjadal/.opam/default/bin/vscoqtop
Which i got from which vscoqtop
Maxime Dénès (Feb 03 2023 at 15:51):is your current switch really default?
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 15:51):yes
Maxime Dénès (Feb 03 2023 at 15:53):what do you pass as arguments?
Maxime Dénès (Feb 03 2023 at 15:53):(i.e. vscoqtop.args)
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 15:54):The default of -bt
Maxime Dénès (Feb 03 2023 at 15:54):I am surprised that it manages to find the stdlib, then
Maxime Dénès (Feb 03 2023 at 15:55):(I'm trying to reproduce as I don't use opam myself, but I hit slightly different issues, I'll continue investigating next week)
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 15:56):So would you suggest I try without Opam?
Maxime Dénès (Feb 03 2023 at 15:57):I build with nix without trouble. But I believe @Enrico Tassi does it with opam.
Maxime Dénès (Feb 03 2023 at 15:59):One more thing: you get the backtrace in the "Coq Language Server" output window?
Maxime Dénès (Feb 03 2023 at 15:59):Did you do anything more to have it displayed?
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 16:01):No, I add logging to a text file in vscoqtop.ml. As it was the fastest way to see what was going wrong i could think of
Maxime Dénès (Feb 03 2023 at 16:02):Ah! So actually I may have managed to reproduce the pb. Just I wasn't seeing the backtrace.
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 16:02):Yeah without it just crashes 5 times and does not restart, without giving any feedback
Maxime Dénès (Feb 03 2023 at 16:03):I saw something fishy in the process: opam built Coq twice (once as part of the coq-core package, the other as part of vscoq-language-server).
Maxime Dénès (Feb 03 2023 at 16:03):So thanks for the report, I'll investigate more next week, but I believe I can reproduce.
Enrico Tassi (Feb 03 2023 at 16:09):oh, then my CI job is bad too
Hjalte Sorgenfrei Mac Dalland (Feb 03 2023 at 16:13):Super, thanks a lot for your help :)
I think the issue I have with Nix is some sort of library missing.
Running nix-shell --run "cd language-server/coq && make -j2 world"
Gives a bunch of linking errors for gtk, gdk and gtksourceview like this:
/nix/store/r2b9k28c6aghczpqfvh71y9xavm7rr68-binutils-2.39/bin/ld: warning: libxml2.so.2, needed by /nix/store/vn56q9iw31fs5kbarl1yhxryhyj3ldh2-gtksourceview-3.24.11/lib/libgtksourceview-3.0.so, not found (try using -rpath or -rpath-link)
Through I might be doing something wrong here as i am a total noob at Nix.
Maxime Dénès (Feb 08 2023 at 07:25):@Hjalte Sorgenfrei Mac Dalland I fixed the Nix build issues by porting it to Flakes. Once you activate flakes for your nix install, you can do:
nix develop, then make world in language server.
Maxime Dénès (Feb 08 2023 at 07:26):To activate flakes you can run something like:
mkdir -p ~/.config/nix
echo "experimental-features = nix-command flakes" >> ~/.config/nix/nix.conf
(see https://nixos.wiki/wiki/Flakes for more)
Maxime Dénès (Feb 08 2023 at 07:27):Once you built the language server, you can build and execute the extension. You can launch it from VsCode. You will probably have to customize the vscoq settings: putting the full vscoqtop path in vscoq.path (including the file name).
Maxime Dénès (Feb 08 2023 at 07:30):And in vscoq.args, you'll need to add ["-coqlib", "path/to/vscoq2/language-server/_build/install/default/lib/coq"]
Maxime Dénès (Feb 08 2023 at 07:31):Sorry for the current complexity, all this will go away once we can switch to a regular Coq version instead of our custom one.
Simon Green Kristensen (Feb 08 2023 at 13:09):Following your instructions, we have been able to build and run the extension on very simple files (define boolean inductive type, prove 0+n=n)! Thanks for the help.
Simon Green Kristensen (Feb 08 2023 at 13:09):However, running it on Basics.v from the book Software foundations vol. 1 makes the server raise an exception, which we suppose is due to not having async proofs enabled by default:
Anomaly
"in safe_typing: True Future.t were created for opaque constants even if -async-proofs is off"
Please report at http://coq.inria.fr/bugs/.
Raised at Exninfo.iraise in file "coq/clib/exninfo.ml", line 79, characters 4-11
Called from Safe_typing.propagate_senv in file "coq/kernel/safe_typing.ml", line 1161, characters 4-134
Called from Safe_typing.end_module in file "coq/kernel/safe_typing.ml", line 1192, characters 2-66
Called from Global.globalize_with_summary in file "coq/library/global.ml", line 66, characters 16-31
Called from Declaremods.RawModOps.Interp.end_module_core in file "coq/vernac/declaremods.ml", line 1008, characters 26-64
Called from Declaremods.RawModOps.Interp.end_module in file "coq/vernac/declaremods.ml", line 1033, characters 19-55
Called from Vernacentries.vernac_end_module in file "coq/vernac/vernacentries.ml", line 1229, characters 11-43
Called from Vernacentries.vernac_end_segment.(fun) in file "coq/vernac/vernacentries.ml", line 1310, characters 17-50
Called from Vernacinterp.interp_typed_vernac in file "coq/vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "coq/vernac/vernacinterp.ml", line 213, characters 24-69
Called from Flags.with_modified_ref in file "coq/lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "coq/clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "coq/vernac/vernacinterp.ml", line 263, characters 18-43
Called from Vernacinterp.interp_gen in file "coq/vernac/vernacinterp.ml", line 261, characters 6-286
Re-raised at Exninfo.iraise in file "coq/clib/exninfo.ml", line 81, characters 4-38
Called from Dm__ExecutionManager.interp_ast in file "dm/executionManager.ml", line 97, characters 13-46
Called from Dm__ExecutionManager.execute in file "dm/executionManager.ml", line 261, characters 26-68
Called from Dm__DocumentManager.handle_event in file "dm/documentManager.ml", line 230, characters 6-93
Called from Dune__exe__LspManager.handle_event in file "vscoqtop/lspManager.ml", line 334, characters 26-62
Called from CList.map_loop in file "coq/clib/cList.ml", line 291, characters 21-24
Called from CList.map in file "coq/clib/cList.ml", line 299, characters 4-18
Called from CList.map_append in file "coq/clib/cList.ml", line 391, characters 29-38
Called from Dune__exe__Vscoqtop.loop.loop in file "vscoqtop/vscoqtop.ml", line 27, characters 22-68
Called from Dune__exe__Vscoqtop.loop in file "vscoqtop/vscoqtop.ml", line 29, characters 6-27
I also got it working and I am working on a bugfix to fix the issue that occurs for @Simon Green Kristensen .
A minimal repro example is the following:
Theorem plus_0_n : forall n : nat, 0 + n = n.
Proof. apply plus_O_n. Qed.
Module ModuleTest.
End ModuleTest.
Thank for the help getting the extension running :)
Maxime Dénès (Feb 08 2023 at 14:05):Interesting! We're gonna look at it with Enrico
Enrico Tassi (Feb 08 2023 at 14:57):https://github.com/coq-community/vscoq/pull/366
Enrico Tassi (Feb 08 2023 at 15:00):Thanks for testing on a real example, the fix was easy. The whole SF file now passes.
Enrico Tassi (Feb 08 2023 at 15:01):If you happen to hit more issues, feel free to open an issue on github.
Maxime Dénès (Feb 08 2023 at 16:10):And the fixes have been merged in the vscoq2 branch.
Last updated: Jun 04 2023 at 23:30 UTC