Stream: Coq devs & plugin devs

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


view this post on Zulip Jason Gross (Feb 06 2022 at 17:35):

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

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

What's the fix?

view this post on Zulip Enrico Tassi (Feb 06 2022 at 18:00):

Do you install lib/coq-core/META?

view this post on Zulip Jason Gross (Feb 06 2022 at 19:24):

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

view this post on Zulip Jason Gross (Feb 06 2022 at 19:30):

Is there some issue here with opam vs Ubuntu system layout?

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

view this post on Zulip Jason Gross (Feb 06 2022 at 20:39):

Reported as an issue at https://github.com/coq/coq/issues/15635

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

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

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

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

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

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

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

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

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

view this post on Zulip Enrico Tassi (Feb 07 2022 at 09:24):

Is there an issue where your findings are summarized?

view this post on Zulip Karl Palmskog (Feb 07 2022 at 09:25):

maybe this one? https://github.com/coq/coq/issues/15452

view this post on Zulip Enrico Tassi (Feb 07 2022 at 09:31):

thanks

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

view this post on Zulip Enrico Tassi (Feb 07 2022 at 09:45):

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

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

view this post on Zulip Enrico Tassi (Feb 07 2022 at 09:48):

WDYT @Guillaume Melquiond ?

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

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

view this post on Zulip Jason Gross (Feb 09 2022 at 18:27):

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

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?

view this post on Zulip Jason Gross (Feb 09 2022 at 20:57):

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

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

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

view this post on Zulip Jason Gross (Feb 11 2022 at 06:24):

Hm, seems that I was symlinking the wrong META file, oops

view this post on Zulip Notification Bot (Feb 11 2022 at 06:24):

Jason Gross has marked this topic as resolved.


Last updated: Dec 07 2023 at 18:01 UTC