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.
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.
Theo I suggest you remove the optional field from the dune file
the package works fine here, but indeed that kind of optional stuff lead to many problems
Tho you should get a warning
the optional field is in ide/coqide/dune
for the executable
OK thanks, I'll try.
so indeed, if I do
dune build coqide.install without lablgtk3 installed, I get an almost empty package
dune build @check does warn about it
so not sure what the rules for this warning are
yeah, dune build @all too
so I guess the warning is suppresed for the install target as to match the semantics that opam has
a bad idea IMHO
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
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: Feb 05 2023 at 19:29 UTC