Stream: Coq devs & plugin devs

Topic: CoqIDE package built with Dune

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 16:32):

Has someone actually tested that the new CoqIDE package contains some binary? When doing tests of building coqide with an installed Coq, I do not get any bin directory.

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 16:33):

I can open a bug report, but again my reproduction case is using Nix, so if the bug is independent of Nix, it might not be useful.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:47):

Theo I suggest you remove the optional field from the dune file

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:47):

the package works fine here, but indeed that kind of optional stuff lead to many problems

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:48):

Tho you should get a warning

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:48):

the optional field is in ide/coqide/dune

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:48):

for the executable

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 17:48):

OK thanks, I'll try.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:50):

so indeed, if I do dune build coqide.install without lablgtk3 installed, I get an almost empty package

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:50):

dune build @check does warn about it

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:50):

so not sure what the rules for this warning are

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:50):

yeah, dune build @all too

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:51):

so I guess the warning is suppresed for the install target as to match the semantics that opam has

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:51):

a bad idea IMHO

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2022 at 17:51):

note that we don't call configure for coqide, but this is something I'd like to solve, to totally separate configure of coqide and of coq

view this post on Zulip Théo Zimmermann (Jul 06 2022 at 18:07):

Your suggestion to remove (optional) was a good one: it helped figure out the problem. It wasn't lablgtk3 but coqide-server that was missing. Probably I didn't register it properly with ocamlfind.

Last updated: Oct 13 2024 at 01:02 UTC