Stream: Coq devs & plugin devs

Topic: ✔ Where does /usr/bin/coqide come from?

Julien Puydt (Jan 24 2022 at 16:41):

I just tried:

dune build -p coq-core,coq-stdlib,coqide-server,coqide
find _build -name coqide -executable

and got nothing. I have it in my package, but don't know where I get it from...

Emilio Jesús Gallego Arias (Jan 24 2022 at 16:53):

this is because _build/install/default/bin/coqide is a symlink to _build/default/ide.../coqide.exe

Emilio Jesús Gallego Arias (Jan 24 2022 at 16:53):

The thing looks a bit weird but dune has to work on windows so there is a bit of stuff like this to have a more uniform setup in cross-compilation etc...

Julien Puydt (Jan 24 2022 at 21:32):

I'm using coq's 8.15.0 tarball from github, dune 2.9.1 and my command line to compile is: dune build -p coq-core,coq-stdlib,coqide-server,coqide.

I get:

$ find _build/ -name "coqide*" -type f
_build/default/coqide-server.install
_build/default/coqide-server.opam
_build/default/coqide.opam
_build/default/coqide-server.dune-package
_build/default/coqide.dune-package
_build/default/man/coqide.1
_build/default/tools/configure/coqide.ml
_build/default/tools/configure/.conf.objs/coqide.ml.d
_build/default/tools/configure/.conf.objs/coqide.mli.d
_build/default/tools/configure/coqide.mli
_build/default/coqide.install

I do see ide/coqide/dune declaring an executable with public_name coqide, but I don't see it anywhere... I do have a /usr/bin/coqide in my Debian package, but trying to build by hand, I don't know where it comes from. In fact, I was precisely trying to understand things better to rework the Debian packaging to follow upstream packages. For the moment, let's say learning dune starts with a cliff rather than a steep slope ;-)

Emilio Jesús Gallego Arias (Jan 24 2022 at 21:44):

The executable is optional

Emilio Jesús Gallego Arias (Jan 24 2022 at 21:44):

are you sure you have the deps installed?

Emilio Jesús Gallego Arias (Jan 24 2022 at 21:44):

The location is _build/default/ide/coqide/coqide_main.exe

Julien Puydt (Jan 25 2022 at 06:02):

Oh dear, indeed with the current OCaml 4.13.1 transition in Debian, I had lost lablgtk... thanks!

Notification Bot (Jan 25 2022 at 16:19):

Julien Puydt has marked this topic as resolved.

Last updated: Apr 18 2024 at 15:01 UTC