Coq seems to install META files in the wrong location
Closed this issue · 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 ?
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.
So it is a bug in "configure.ml"?
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 ofocamlfind printconf destdir
." Since Coq uses--prefix
, Dune installs the files in a location that Findlib never heard about.
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.
I think we had this sorted in configure/Makefile.install but is very possible that I messed up.
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 ofocamlfind 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
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)
@JasonGross is this still relevant?
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
Unsetting the blocker tag in any case.
@ejgallego any idea what's going on in mit-plv/fiat-crypto#1558 and mit-plv/fiat-crypto#1787 ?
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.
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)
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?
@ejgallego If I skip ./configure
and remove --prefix
, then it seems to work fine. I guess --prefix
is not supported with dune install
?
@ejgallego If I skip
./configure
and remove--prefix
, then it seems to work fine. I guess--prefix
is not supported withdune 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.
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
)
Note that -libdir
in Coq's configure is used to locate Coq's stdlib, not for any OCaml libs.
Seems like dropping
--prefix
in your case will be a no-op asdune
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 ofocamlfind 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)
todune
's./configure
and we should instead be passingocamlfind printconf destdir
(except I guess the package doesn't depend onocamlfind
so I guess we can't useocamlfind 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'sdune install
, or if I should pass--libdir="$(ocamlc -where)"
or--libdir="$(ocamlfind printconf destdir)"
I guess this is #15452
Duplicate of #15452