Julien Puydt (Dec 25 2021 at 18:15): Julien Puydt (Dec 25 2021 at 18:15):I discovered a new problem with the current Debian coq package: ocamlfind doesn't see the coq-core libraries because they're in /usr/lib/coq-core which isn't in the search path. But if I tell dune install --libdir=/usr/lib/ocaml, then ocamlfind finds the coq libraries... but coq itself doesn't find its stdlib anymore! So I would need a way to tell dune that ocaml libs go to /usr/lib/ocaml, but that coq libs go to /usr/lib/coq... if that's even possible...
Emilio Jesús Gallego Arias (Dec 25 2021 at 23:25):That's weird, Debian dune should be patched already to install stuff in the right location, and coq libs are looked by Prelude.vo which is set at configure time
Julien Puydt (Dec 26 2021 at 00:50):There is no configure time with dune, is it?
Gaëtan Gilbert (Dec 26 2021 at 08:46):there's implicit configure
Emilio Jesús Gallego Arias (Dec 26 2021 at 12:27):I mean dune itself, for distros, dune has its own configure thing so it can install ocaml libs in the right place
Emilio Jesús Gallego Arias (Dec 26 2021 at 12:27):So Debian's dune should do already the right thing (TM) otherwise there is a bug
Emilio Jesús Gallego Arias (Dec 26 2021 at 12:28):Indeed, see https://salsa.debian.org/ocaml-team/ocaml-dune/-/blob/master/debian/rules#L21
Emilio Jesús Gallego Arias (Dec 26 2021 at 12:28):so it is strange you see that
Julien Puydt (Dec 26 2021 at 21:24):I don't get the point... this configure line says where Debian's dune gets installed, not where it will install things when used.
The problem I have is that if I tell coq's dune invocation to install libs in /usr/lib/ocaml, then it also installs non-libs (coq's stdlib isn't an OCaml lib) in /usr/lib/ocaml, and that is wrong. And if I don't add --libdir to coq's dune invocation, then the libs get into /usr/lib/ directly and ocamlfind won't find them.
Emilio Jesús Gallego Arias (Dec 26 2021 at 22:34):Julien Puydt said:
I don't get the point... this configure line says where Debian's dune gets installed, not where it will install things when used.
That's not correct.
Guillaume Melquiond (Dec 27 2021 at 08:55):Emilio Jesús Gallego Arias said:
That's not correct.
Actually, it is mostly correct. Indeed, ifocamlfind is present, dune ignores the value that was passed to --libdir at configure time. It uses instead the result of ocamlfind printconf destdir. As documented, "If ocamlfind is present, it has precedence over everything else."
Emilio Jesús Gallego Arias (Dec 27 2021 at 15:02):Oh indeed, but I guess Debian's ocamlfind should also output the correct directory?
Emilio Jesús Gallego Arias (Dec 27 2021 at 15:03):But my comment stand, the flag doesn't tell dune where it is installed itself, as @Julien Puydt mentioned, but where to install the ocaml libs using dune install, that is to say, the mapping of lib to files.
Emilio Jesús Gallego Arias (Dec 27 2021 at 15:04):There could be a problem with the way we install .vo files tho.
Emilio Jesús Gallego Arias (Dec 27 2021 at 15:04):but for OCaml libs (that is to say, coq-core), should work fine
Julien Puydt (Dec 30 2021 at 13:20):I don't get it: the problem I have is that dune installs ocaml & coq libs in the same directory, so one of them is always wrong
Karl Palmskog (Dec 30 2021 at 13:56):things like coq-core are OCaml libraries. A "Coq library" is nearly always used to refer to compiled .vo files that are installed into a subdirectory of coq/user-contrib (where coq might be /usr/lib/coq)
Julien Puydt (Dec 30 2021 at 15:41):Karl Palmskog said:
things like
coq-coreare OCaml libraries. A "Coq library" is nearly always used to refer to compiled.vofiles that are installed into a subdirectory ofcoq/user-contrib(wherecoqmight be/usr/lib/coq)
As I said, there should be two library directories: 1. /usr/lib/ocaml for the ocaml part so ocamlfind works 2. and /usr/lib/coq for the theories -- and I haven't found how to tell dune about the difference
Karl Palmskog (Dec 30 2021 at 15:47):so it seems that what you want is to remap user-contrib to some arbitrary location. I'm not sure that's currently possible (without patching the source).
Julien Puydt (Dec 30 2021 at 22:56):Karl Palmskog said:
so it seems that what you want is to remap
user-contribto some arbitrary location. I'm not sure that's currently possible (without patching the source).
The current situation is:
so I'm a bit upset either way.
Gaëtan Gilbert (Dec 30 2021 at 23:24):you probably need to tell something to coq's configure
how did it work before?
Julien Puydt (Dec 31 2021 at 08:09):Gaëtan Gilbert said:
you probably need to tell something to coq's configure
how did it work before?
Coq's configure? I thought that didn't exist with dune anymore?
Gaëtan Gilbert (Dec 31 2021 at 10:32):it still exists, but you don't need to use it if you don't install, or if you just want -prefix you can replace it with setting COQ_CONFIGURE_PREFIX
if your configure is more complicated than -prefix you still need it
Julien Puydt (Jan 03 2022 at 16:24):Gaëtan Gilbert said:
it still exists, but you don't need to use it if you don't install, or if you just want -prefix you can replace it with setting COQ_CONFIGURE_PREFIX
if your configure is more complicated than -prefix you still need it
I tried to configure with:
./configure -bindir /usr/bin -libdir /usr/lib/coq -configdir /etc/xdg/coq -datadir /usr/share/coq -mandir /usr/share/man -docdir /usr/share/doc/coq -coqdocdir /usr/share/texmf/tex/latex/misc
and got, while building (no install tried):
Command [2821] exited with code 1:
$ (cd _build/default/doc/stdlib && /usr/bin/bash -e -u -o pipefail -c '../../../install/default/bin/coqdoc -q -d html --with-header ../common/styles/html/coqremote/header.html --with-footer ../common/styles/html/coqremote/footer.html --multi-index --html -g -R ../../theories Coq -Q ../../user-contrib/Ltac2 Ltac2 $(find ../../theories ../../user-contrib -name *.v)')
coqdoc: cannot find coqdoc style files in coqlib: /home/jpuydt/Debian/build/coq-8.14.1+dfsg/_build/default/tools / coqdoc.css
what build command?
Julien Puydt (Jan 03 2022 at 16:29):(there is a /home/jpuydt/Debian/build/coq-8.14.1+dfsg/_build/default/tools/coqdoc/coqdoc.css)
I have two build commands and I don't know yet which failed:
dune build -p coq-core,coq-stdlib,coqide-server,coqide --display=verbose
dune build @stdlib-html --display=verbose
(I'll retry with complete logs)
Julien Puydt (Jan 03 2022 at 16:43):It's happening at the second step of the build.
Julien Puydt (Jan 04 2022 at 15:06):Can you reproduce the issue?
Gaëtan Gilbert (Jan 04 2022 at 16:06):it seems we need to add -coqlib_path %{project_root} to the invocation at https://github.com/coq/coq/blob/4d78b1fbf6a76dfd48c2fffa3cccf5a1d030fdf2/doc/stdlib/dune#L30
Karl Palmskog (Jan 04 2022 at 16:12):this might be considered a regression introduced between 8.13 and 8.14, right?
Julien Puydt (Jan 04 2022 at 16:14):I'll give it a try
Gaëtan Gilbert (Jan 04 2022 at 16:21):Karl Palmskog said:
this might be considered a regression introduced between 8.13 and 8.14, right?
no, it's unchanged I think
Gaëtan Gilbert (Jan 04 2022 at 16:21):@Julien Puydt is just using dune targets that where undertested
Karl Palmskog (Jan 04 2022 at 16:23):but didn't the -coqlib_path configure variable work also for stdlib-doc, etc., before Dune was introduced?
Karl Palmskog (Jan 04 2022 at 16:24):I briefly recall using it a couple of years ago...
Gaëtan Gilbert (Jan 04 2022 at 16:26):this is a dune problem so if you use legacy build there's no problem
Julien Puydt (Jan 05 2022 at 18:41):I get things to compile, I get ocamlfind to see the coq libs... but coqide insists on searching the libs in /usr/lib/ocaml/theories, while of course they have been installed in /usr/lib/ocaml/coq/theories...
Karl Palmskog (Jan 05 2022 at 19:10):is it only CoqIDE, or can you reproduce with CLI builds of Coq projects? Try for example make after cloning this: https://github.com/coq-community/huffman
Julien Puydt (Jan 06 2022 at 07:51):Coqide, configured with the same configure line as coq, built with the same build line as coq, installed with the same install line as coq... doesn't find coq.
huffman's make also doesn't find coq.
Karl Palmskog (Jan 06 2022 at 07:57):OK, then the problem is in compilation/installation of Coq itself rather than CoqIDE
Karl Palmskog (Jan 06 2022 at 07:58):CLI compilation is a good first smoke test, CoqIDE has many moving parts
Julien Puydt (Jan 06 2022 at 09:42):So there's something wrong at the configure stage, probably?
Karl Palmskog (Jan 06 2022 at 11:15):maybe, but you say you can't find the coqc executable? Or what's the error message from trying to compile Huffman?
Karl Palmskog (Jan 06 2022 at 11:15):this could even be some PATH problem
Julien Puydt (Jan 06 2022 at 12:33):No, I mean the coq lib isn't found:
Error:
cannot guess a path for Coq libraries; please use -coqlib option or ensure you have installed the package containing Coq's stdlib (coq-stdlib in OPAM) If you intend to use Coq without a standard library, the -boot -noinit options must be used.
Let me again quote the configure line:
./configure -bindir /usr/bin -libdir /usr/lib/ocaml -configdir /etc/xdg/coq -datadir /usr/share/coq -mandir /usr/share/man -docdir /usr/share/doc/coq -coqdocdir /usr/share/texmf/tex/latex/misc
the build lines:
dune build -p coq-core,coq-stdlib,coqide-server,coqide --display=verbose
dune build @stdlib-html --display=verbose
and the install line:
dune install coq-core coq-stdlib coqide-server coqide --destdir=$(CURDIR)/debian/tmp --prefix=/usr --mandir=/usr/share/man --libdir=/usr/lib/ocaml
hum, what about find /usr/lib/ocaml -name Prelude.vo?
Julien Puydt (Jan 06 2022 at 13:05):Well, of course Prelude.vo is in /usr/lib/ocaml/coq/theories/Init/Prelude.vo ; but the problem (and using "strace coqidetop.opt | grep Prelude" definitely proves this is it) is that it's only looked as /usr/lib/ocaml/theories/Init/Prelude.vo.
Julien Puydt (Jan 06 2022 at 13:08):My initial assessment of the issue was that coq libs and ocaml libs shouldn't be mistaken one for the other ; I stand by it.
There should be libdir to install the ocaml libs for coq, and a coqlibdir to install the coq libs for coq (ie: stdlib).
Julien Puydt (Jan 09 2022 at 14:23):This is now: https://github.com/coq/coq/issues/15452
Last updated: Nov 29 2023 at 22:01 UTC