Following up on https://github.com/coq/coq/issues/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
What's the fix?
Do you install lib/coq-core/META?
The build log says
So it looks like it gets installed to
Is there some issue here with opam vs Ubuntu system layout?
It should be installed to
/usr/lib/ocaml/coq-core/META. You can double-check by looking at the paths given by
ocamlfind printconf. I don't think this is specific to Ubuntu. It should be the same for any standard installation of OCaml.
Reported as an issue at https://github.com/coq/coq/issues/15635
@Jason Gross did you see the long discussions about the placement of coq-core and similar with the Debian packager? For example, this one
@Karl Palmskog thanks, I left a comment on that issue. It seems to be related, but I think the findlib PR made the situation worse somehow?
I guess it made the situation worse in the following sense. Before the pull request, plugin paths were hardcoded, so even if they were installed in the wrong place, they were still found by findlib (assuming the hardcoded paths were consistent). Now, this is no longer the case. Thus, if the plugins are not installed in one of the search paths looked up by findlib, they cannot be found anymore.
I suggest you add a line symlinking coq-core in the right place in you dh_override_auto_install.
I'm not sure the other discussions about the install paths of dune in Debian were conclusive.
(I mean, they should not have happened here, but rather on Debian channels, and they are going to require to update dune's package, so not something you can do in your corner)
If dune and coq install files don't distinguish the various types of files, Debian can do little to fix matters on its end...
I don't know about all the other problems (I don't have the energy to follow all discussions), but for META files (and the corresponding .cmxs), Debian's findlib, Debian's dune and Debian's coq should agree, and use the same paths. Which is the right one, is up to Debian to decide. And Debian can patch upstream software as she please.
I mean, it would not be the first time that a debian package does
make install; mv debian/tmp/foo debian/tmp/bar because the makefiles are buggy..
@Enrico Tassi Debian can move files around all it wants (and indeed, it does), if the software keeps computing its paths left and right without consideration for the type of information, it cannot do much...
(and coq also provides a Makefile system, so if said system also doesn't cope with file types correctly, that means other packages too get ugly)
Is there an issue where your findings are summarized?
maybe this one? https://github.com/coq/coq/issues/15452
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.
Maybe the quickest fix is to initialize
ocamlfind so that
$COQLIB/.. is a root like here https://github.com/coq/coq/blob/7c608fe3e9a3054c6809ae8556bea404256369c7/sysinit/coqinit.ml#L125
Well, and if I want to put ocaml libs in /usr/lib/ocaml and coq libs in /usr/lib/coq (which makes sense: it's not the same thing!), then having just a "libdir" is definitely too little. Since my last rework, everything is in /usr/lib/ocaml.
WDYT @Guillaume Melquiond ?
If I understood correctly, that will not solve the issue Jason is encountering. Because it is not Coq that is not finding the plugins at runtime, it is OCaml that does not find them at compile time.
--libdir for that, so you can use prefix but override
@Julien Puydt I tried using your debian folder from https://github.com/coq/coq/issues/15452#issuecomment-1031679711, but that fails at https://launchpadlibrarian.net/585071937/buildlog.txt.gz with
Traceback (most recent call last): File "/usr/lib/python3/dist-packages/gitbuildrecipe/main.py", line 164, in main package_version.upstream_version, working_basedir) File "/usr/lib/python3/dist-packages/gitbuildrecipe/deb_util.py", line 86, in extract_upstream_tarball raise NoSuchTag(tag_names) gitbuildrecipe.deb_util.NoSuchTag During handling of the above exception, another exception occurred: Traceback (most recent call last): File "/usr/lib/python3/dist-packages/gitbuildrecipe/deb_util.py", line 215, in convert_3_0_quilt_to_native ["quilt", "push", "-a", "-v"], cwd=path, env=env) File "/usr/lib/python3.6/subprocess.py", line 311, in check_call raise CalledProcessError(retcode, cmd) subprocess.CalledProcessError: Command '['quilt', 'push', '-a', '-v']' returned non-zero exit status 1. During handling of the above exception, another exception occurred: Traceback (most recent call last): File "/usr/bin/git-build-recipe", line 11, in <module> load_entry_point('git-build-recipe==0.1', 'console_scripts', 'git-build-recipe')() File "/usr/lib/python3/dist-packages/gitbuildrecipe/main.py", line 172, in main force_native_format(working_directory, current_format) File "/usr/lib/python3/dist-packages/gitbuildrecipe/deb_util.py", line 236, in force_native_format convert_3_0_quilt_to_native(working_tree_path) File "/usr/lib/python3/dist-packages/gitbuildrecipe/deb_util.py", line 223, in convert_3_0_quilt_to_native raise Exception("Failed to apply quilt patches") Exception: Failed to apply quilt patches RUN: /usr/share/launchpad-buildd/bin/in-target scan-for-processes --backend=chroot --series=impish --arch=amd64 RECIPEBRANCHBUILD-2952857 Scanning for processes to kill in build RECIPEBRANCHBUILD-2952857
For reference, the previous successful build log is at https://launchpadlibrarian.net/584903443/buildlog_ubuntu-impish-amd64.coq_8.master~git~202202072017+23038-0~daily367-d76cff3874~ubuntu21.10.1_BUILDING.txt.gz
Any ideas what's going wrong?
configure does not impact where
META files are installed.
@Jason Gross Your backtrace looks strange: it's Python and it speaks about git. Please start with just the unpacked sources, the debian dir and dpkg-buildpackage -- once that simpler setup works we can try to figure out what goes wrong with your complete setup.
$ ocamlfind printconf path /home/jgross/.local64/lib /home/jgross/.opam/4.11.2+fp/lib $ find -L /home/jgross/.local64/lib -name '*META*' /home/jgross/.local64/lib/ocaml/coq/coq-core/META
So why does ocamlfind give the error ocamlfind: Package `coq-core.plugins.ltac' not found?
Hm, seems that I was symlinking the wrong META file, oops
Jason Gross has marked this topic as resolved.
Last updated: Feb 06 2023 at 00:03 UTC