Coq seems to install META files in the wrong location

Question

Coq seems to install META files in the wrong location

Closed this issue 8 months ago · 24 comments

Following up on #15610, the Ubuntu packages I maintain now generate a Coq which is incapable of building plugins, failing with things like

CAMLC -c src/Rewriter/Util/plugins/strategy_tactic.mli
ocamlfind: Package `coq-core.plugins.ltac' not found

(cf https://github.com/mit-plv/fiat-crypto/runs/5084108808?check_suite_focus=true#step:6:487)

The build log says

Installing /<<BUILDDIR>>/coq-8.master~git~202202051948+23033-0~daily356/debian/tmp/usr/lib/coq-core/META

So it looks like it gets installed to /usr/lib/coq-core/META

@silene said on zulip that it should be installed to /usr/lib/ocaml/coq-core/META.
The configure options I'm building with are set at https://github.com/JasonGross/coq-packaging/blob/f6a69cce7f82d0fbcb47578433af744198b7dedd/debian/rules#L26-L30: -arch Linux -prefix /usr -mandir /usr/share/man -configdir /etc/xdg/coq -docdir /usr/doc -browser "/usr/bin/x-www-browser %s &" -with-doc no.

cc @gares @ejgallego ?

Answer 1 · 2022-02-07T09:36:06.000Z

This seems a duplicate of #15452

Answer 2 · 2022-02-08T10:35:22.000Z

I think this is different, for some reason the --libdir=/usr/lib/ocaml that is needed in Debian is not passed to Dune, it uses $prefix/lib instead which is the default.

Answer 3 · 2022-02-08T10:50:18.000Z

So it is a bug in "configure.ml"?

Answer 4 · 2022-02-08T10:55:27.000Z

For the record, here is what I wrote in Zulip:

I think the main issue is as follows. Dune says "If --prefix is specified the default is $prefix/lib, otherwise it is the output of ocamlfind printconf destdir." Since Coq uses --prefix, Dune installs the files in a location that Findlib never heard about.

Answer 5 · 2022-02-08T11:02:46.000Z

So it is a bug in configure.ml?

I would rather say that it is a bug in Makefile.install. But there is presumably a missing feature in configure.ml that prevents from fixing the bug adequately, I guess.

Answer 6 · 2022-02-08T13:49:39.000Z

I think we had this sorted in configure/Makefile.install but is very possible that I messed up.

Answer 7 · 2022-02-08T13:50:05.000Z

For the record, here is what I wrote in Zulip:

I think the main issue is as follows. Dune says "If --prefix is specified the default is $prefix/lib, otherwise it is the output of ocamlfind printconf destdir." Since Coq uses --prefix, Dune installs the files in a location that Findlib never heard about.

Yup, dune allows to override this tho with --libdir

Answer 8 · 2022-02-09T20:14:10.000Z

I think this is different, for some reason the --libdir=/usr/lib/ocaml that is needed in Debian is not passed to Dune, it uses $prefix/lib instead which is the default.

Even if I pass -libdir to ./configure explicitly, make install ignores it and installs the META files to, e.g., usr/lib/coq-core/META (see this log)

Answer 9 · 2022-05-16T09:08:37.000Z

@JasonGross is this still relevant?

Answer 10 · 2022-05-16T21:32:11.000Z

I think it's not? I'm not sure, though; I found a workaround a while back, I think, and haven't touched the code since

Answer 11 · 2022-05-17T06:19:04.000Z

Unsetting the blocker tag in any case.

Answer 12 · 2022-05-17T08:19:03.000Z

I suspect this is broken in the non-standard layout we are discussing in #15663 .

Answer 13 · 2022-05-17T14:25:42.000Z

Should be solved by #15560

Answer 14 · 2023-12-20T23:08:56.000Z

@ejgallego any idea what's going on in mit-plv/fiat-crypto#1558 and mit-plv/fiat-crypto#1787 ?

Answer 15 · 2023-12-20T23:14:14.000Z

ocamlfind cannot find the coq-core.plugins.ltac library. This is indeed can happen due to many reasons, wrong findlib config, wrong OCaml config, wrong dune config, packages not following the install instructions.

I guess on Arch, I'd try to see if other OCaml packages are correctly installed (by means of ocamlfind query $pkg returning the right path. If so, I'd try to see if oterh OCaml packages using dune do work, otherwise, Arch's dune is misconfigured as to where it should install libs.

If all of the above is correct, likely the problem is wrong install instruction for coq-core itself.

Answer 16 · 2023-12-21T18:04:49.000Z

I guess the issue in Arch is a missing configure at https://gitlab.archlinux.org/archlinux/packaging/packages/coq/-/blob/main/PKGBUILD?ref_type=heads#L49 as in #15663 (comment)

Answer 17 · 2023-12-24T01:34:41.000Z

Hm, but this does not fix the problem for Alpine, which even with the updated ./configure installs

usr/lib/coq-core/META
usr/lib/coq-stdlib/META
usr/lib/coq/META

It seems that dune is configured fine, as ocamlfind query dune says /usr/lib/ocaml/dune. I am using the Alpine Coq package from https://gitlab.alpinelinux.org/alpine/aports/-/merge_requests/57766, btw.

The build log says

You have OCaml 4.14.1. Good!
You have OCamlfind 1.9.6. Good!
You have native-code compilation. Good!
You have the Zarith library 1.12 installed. Good!
  Architecture                : Linux
  Sys.os_type                 : Unix
  OCaml version               : 4.14.1
  OCaml binaries in           : /usr/bin/
  OCaml library in            : /usr/lib/ocaml
  Web browser                 : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
  Coq web site                : http://coq.inria.fr/
  Bytecode VM enabled         : true
  Native Compiler enabled     : no
  Paths where installation is expected by Coq Makefile:
  - Coq is expected in /usr
  - the Coq library is expected in /usr/lib/coq
  - the Coqide configuration files is expected in /usr/etc/xdg/coq
  - the Coqide data files is expected in /usr/share/coq
  - the Coq man pages is expected in /usr/share/man
  - documentation prefix path for all Coq packages is expected in /usr/share/doc
If anything is wrong above, please restart './configure'.
*Warning* To compile the system for a new architecture
          don't forget to do a 'make clean' before './configure'.
dune build  --root . theories_dune ltac2_dune
touch .dune-stamp
cp -a _build/default/theories_dune theories/dune && chmod +w theories/dune
cp -a _build/default/ltac2_dune user-contrib/Ltac2/dune && chmod +w user-contrib/Ltac2/dune
(cd _build/default && /bin/bash -e -u -o pipefail -c dev/tools/make_git_revision.sh) > _build/default/revision

I am building with

build() {
	./configure \
		-prefix /usr \
		-mandir /usr/share/man \
		-docdir /usr/share/doc
	make dunestrap
	dune build -p coq,coq-core,coq-stdlib
}

package() {
	dune install coq coq-core coq-stdlib \
		--prefix=/usr \
		--destdir="$pkgdir" \
		--mandir=/usr/share/man \
		--docdir=/usr/share/doc

	mkdir -vp "$pkgdir"/usr/lib/ocaml
	mv -v "$pkgdir"/usr/lib/stublibs "$pkgdir"/usr/lib/ocaml/
}

Picking a package at ~random, ocaml-ppxlib seems to both use dune and install correctly to usr/lib/ocaml/ppxlib/META.

So the issue seems to be on Coq's side? (Note that this is Coq 8.18.0)

Do you see anything wrong with this @ejgallego ? What should we do to debug?

Answer 18 · 2023-12-24T07:19:59.000Z

@ejgallego If I skip ./configure and remove --prefix, then it seems to work fine. I guess --prefix is not supported with dune install?

Answer 19 · 2023-12-24T16:15:05.000Z

@ejgallego If I skip ./configure and remove --prefix, then it seems to work fine. I guess --prefix is not supported with dune install?

I don't see what the error is from your messages; but indeed --prefix is supported by dune install.

Skipping configure is not allowed unless you are in a "local", dev build.

Answer 20 · 2023-12-24T16:17:23.000Z

Seems like dropping --prefix in your case will be a no-op as dune is likely configured to default to /usr.

Note that for distros like Alpine, you can setup all the dirs for dune at Dune's build time, so packages need only to do dune install (or export DESTDIR=foo dune install)

Answer 21 · 2023-12-24T16:20:48.000Z

Note that -libdir in Coq's configure is used to locate Coq's stdlib, not for any OCaml libs.

Answer 22 · 2023-12-24T22:05:14.000Z

Seems like dropping --prefix in your case will be a no-op as dune is likely configured to default to /usr.

@ejgallego It seems we are again hit by

For the record, here is what I wrote in Zulip:

I think the main issue is as follows. Dune says "If --prefix is specified the default is $prefix/lib, otherwise it is the output of ocamlfind printconf destdir." Since Coq uses --prefix, Dune installs the files in a location that Findlib never heard about.

Originally posted by @silene in #15635 (comment)

However, I cannot find this on the dune docs now, I see for example

if an explicit --lib <path> argument is passed, use this path

if an explicit --prefix <path> argument is passed, use <path>/lib

if --lib <path> argument is passed before during dune compilation to ./configure, use this paths

if OPAM_SWITCH_PREFIX is present in the environment use $OPAM_SWITCH_PREFIX/lib

otherwise, fail

without any mention of ocamlfind printconf destdir. @ejgallego How does -prefix and -libdir in ./configure interact with --prefix and --libdir in dune install? Is there a way to tell dune install to install Coq files as per the -prefix given to ./configure but install OCaml files as per the configuration of ocamlfind?

I see that dune is configured in Alpine with

./configure --libdir="$(ocamlc -where)" \
                --bindir="/usr/bin" --sbindir="/usr/sbin" --etcdir="/etc" \
                --mandir="/usr/share/man" --docdir="/usr/share/doc" \
                --datadir="/usr/share"

and I'm trying to understand

if it is incorrect to pass $(ocamlc -where) to dune's ./configure and we should instead be passing ocamlfind printconf destdir (except I guess the package doesn't depend on ocamlfind so I guess we can't use ocamlfind printconf destdir?)
if I should invoke Coq's ./configure with -prefix /usr in Alpine
if I should invoke Coq's dune install with --prefix=/usr in Alpine
whether I should avoid passing -libdir to Coq's ./configure, or if I should pass -libdir /usr/lib or -libdir "$(ocamlc -where)" or -libdir "$(ocamlfind printconf destdir)"
whether I should avoid passing --libdir to Coq's dune install, or if I should pass --libdir="$(ocamlc -where)" or --libdir="$(ocamlfind printconf destdir)"

Answer 23 · 2023-12-24T22:07:35.000Z

I guess this is #15452

Answer 24 · 2023-12-24T23:01:06.000Z

Duplicate of #15452