Stream: Coq devs & plugin devs

Topic: Dune install: ocaml libs vs coq libs


view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Julien Puydt (Dec 26 2021 at 00:50):

There is no configure time with dune, is it?

view this post on Zulip Gaëtan Gilbert (Dec 26 2021 at 08:46):

there's implicit configure

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 26 2021 at 12:28):

so it is strange you see that

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 27 2021 at 15:04):

There could be a problem with the way we install .vo files tho.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 27 2021 at 15:04):

but for OCaml libs (that is to say, coq-core), should work fine

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Julien Puydt (Dec 30 2021 at 15:41):

Karl Palmskog said:

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)

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

view this post on Zulip 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).

view this post on Zulip Julien Puydt (Dec 30 2021 at 22:56):

Karl Palmskog said:

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).

The current situation is:

  1. don't set --libdir, get the coq ocaml libs in /usr/lib/coq where ocamlfind doesn't see them ; the coq theories are found by coq tools ;
  2. set --libdir=/usr/lib/ocaml, get the coq ocaml libs in /usr/lib/ocaml/coq where ocamlfind sees them ; but the coq theories don't get found by coq tools.

so I'm a bit upset either way.

view this post on Zulip Gaëtan Gilbert (Dec 30 2021 at 23:24):

you probably need to tell something to coq's configure
how did it work before?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jan 03 2022 at 16:28):

what build command?

view this post on Zulip 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)

view this post on Zulip Julien Puydt (Jan 03 2022 at 16:43):

It's happening at the second step of the build.

view this post on Zulip Julien Puydt (Jan 04 2022 at 15:06):

Can you reproduce the issue?

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jan 04 2022 at 16:12):

this might be considered a regression introduced between 8.13 and 8.14, right?

view this post on Zulip Julien Puydt (Jan 04 2022 at 16:14):

I'll give it a try

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Jan 04 2022 at 16:21):

@Julien Puydt is just using dune targets that where undertested

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 04 2022 at 16:24):

I briefly recall using it a couple of years ago...

view this post on Zulip Gaëtan Gilbert (Jan 04 2022 at 16:26):

this is a dune problem so if you use legacy build there's no problem

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jan 06 2022 at 07:57):

OK, then the problem is in compilation/installation of Coq itself rather than CoqIDE

view this post on Zulip Karl Palmskog (Jan 06 2022 at 07:58):

CLI compilation is a good first smoke test, CoqIDE has many moving parts

view this post on Zulip Julien Puydt (Jan 06 2022 at 09:42):

So there's something wrong at the configure stage, probably?

view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Jan 06 2022 at 11:15):

this could even be some PATH problem

view this post on Zulip 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.

view this post on Zulip Julien Puydt (Jan 06 2022 at 12:36):

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

view this post on Zulip Enrico Tassi (Jan 06 2022 at 12:42):

hum, what about find /usr/lib/ocaml -name Prelude.vo?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Julien Puydt (Jan 09 2022 at 14:23):

This is now: https://github.com/coq/coq/issues/15452


Last updated: Feb 02 2023 at 15:04 UTC