✔ ocamlfind: Package `coq-core.plugins.ltac' not found · Coq devs & plugin devs

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

Enrico Tassi (Feb 06 2022 at 18:00):

Jason Gross (Feb 06 2022 at 19:24):

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

Jason Gross (Feb 06 2022 at 19:30):

Guillaume Melquiond (Feb 06 2022 at 19:43):

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.

Jason Gross (Feb 06 2022 at 20:39):

Karl Palmskog (Feb 06 2022 at 22:38):

@Jason Gross did you see the long discussions about the placement of coq-core and similar with the Debian packager? For example, this one

Jason Gross (Feb 06 2022 at 22:45):

@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?

Guillaume Melquiond (Feb 07 2022 at 07:57):

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.

Enrico Tassi (Feb 07 2022 at 08:42):

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)

Julien Puydt (Feb 07 2022 at 08:53):

If dune and coq install files don't distinguish the various types of files, Debian can do little to fix matters on its end...

Enrico Tassi (Feb 07 2022 at 09:00):

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.

Enrico Tassi (Feb 07 2022 at 09:02):

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

Julien Puydt (Feb 07 2022 at 09:09):

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

Julien Puydt (Feb 07 2022 at 09:11):

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

Enrico Tassi (Feb 07 2022 at 09:24):

Karl Palmskog (Feb 07 2022 at 09:25):

Enrico Tassi (Feb 07 2022 at 09:31):

Guillaume Melquiond (Feb 07 2022 at 09:43):

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.

Enrico Tassi (Feb 07 2022 at 09:45):

Julien Puydt (Feb 07 2022 at 09:45):

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.

Enrico Tassi (Feb 07 2022 at 09:48):

Guillaume Melquiond (Feb 07 2022 at 09:51):

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.

Emilio Jesús Gallego Arias (Feb 07 2022 at 21:28):

Dune has --libdir for that, so you can use prefix but override --libdir=/usr/bin/ocaml

Jason Gross (Feb 09 2022 at 18:27):

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[0])
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

Jason Gross (Feb 09 2022 at 20:57):

Also, using -libdir on configure does not impact where META files are installed.

Julien Puydt (Feb 09 2022 at 21:18):

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

Jason Gross (Feb 11 2022 at 06:21):

$ 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?

Stream: Coq devs & plugin devs

Topic: ✔ ocamlfind: Package `coq-core.plugins.ltac' not found

Jason Gross (Feb 06 2022 at 17:35):