Stream: Coq devs & plugin devs

Topic: Confusing results with coqdep


view this post on Zulip Julien Puydt (Jun 02 2022 at 13:01):

I have pretty big issues with coq-related Debian packages that I want to iron out. As a first step, that requires understanding coqdep (pun intended).

And I find things a bit confusing:

$ coqdep /usr/lib/ocaml/coq/user-contrib/HB
/usr/lib/ocaml/coq/user-contrib/HB/structures.vo /usr/lib/ocaml/coq/user-contrib/HB/structures.glob /usr/lib/ocaml/coq/user-contrib/HB/structures.v.beautified /usr/lib/ocaml/coq/user-contrib/HB/structures.required_vo: /usr/lib/ocaml/coq/user-contrib/HB/structures.v
/usr/lib/ocaml/coq/user-contrib/HB/structures.vio: /usr/lib/ocaml/coq/user-contrib/HB/structures.v

That is already a bit surprising, because there's an explicit From elpi Require Import elpi!

So I'm trying my luck adding -boot to see if I can make sense of it:

$ coqdep -boot /usr/lib/ocaml/coq/user-contrib/HB
*** Warning: in file /usr/lib/ocaml/coq/user-contrib/HB/structures.v, library String is required from root Coq and has not been found in the loadpath!
*** Warning: in file /usr/lib/ocaml/coq/user-contrib/HB/structures.v, library ssreflect is required from root Coq and has not been found in the loadpath!
*** Warning: in file /usr/lib/ocaml/coq/user-contrib/HB/structures.v, library ssrfun is required from root Coq and has not been found in the loadpath!
*** Warning: in file /usr/lib/ocaml/coq/user-contrib/HB/structures.v, library elpi is required from root elpi and has not been found in the loadpath!
/usr/lib/ocaml/coq/user-contrib/HB/structures.vo /usr/lib/ocaml/coq/user-contrib/HB/structures.glob /usr/lib/ocaml/coq/user-contrib/HB/structures.v.beautified /usr/lib/ocaml/coq/user-contrib/HB/structures.required_vo: /usr/lib/ocaml/coq/user-contrib/HB/structures.v
/usr/lib/ocaml/coq/user-contrib/HB/structures.vio: /usr/lib/ocaml/coq/user-contrib/HB/structures.v

and I end up even more confused: it tells me it doesn't find elpi, and in fact, it doesn't find any of the stdlib chunks!

But:

$ coqtop
Welcome to Coq 8.15.2

Coq < From HB Require Import structures.
[Loading ML file ring_plugin.cmxs ... done]
[Loading ML file ssrmatching_plugin.cmxs ... done]
[Loading ML file ssreflect_plugin.cmxs ... done]
[Loading ML file elpi_plugin.cmxs ... done]

Coq <

So, clearly Coq does find everything... from the same codebase, I get two tools not agreeing on what they see!

Can someone shed a light on the matter?

view this post on Zulip Gaëtan Gilbert (Jun 02 2022 at 13:03):

Why are you calling coqdep on user-contrib?

view this post on Zulip Ali Caglayan (Jun 02 2022 at 13:06):

You should be calling coqdep on the .v file.

view this post on Zulip Ali Caglayan (Jun 02 2022 at 13:09):

Don't worry about -boot that just adds deps on files from the stdlib which you don't need.

view this post on Zulip Ali Caglayan (Jun 02 2022 at 13:10):

coqdep is pretty dumb so it is not clever enough to understand you fed it a load of nonsense.

view this post on Zulip Ali Caglayan (Jun 02 2022 at 13:10):

If you try

$ coqdep /usr/lib/ocaml/coq/user-contrib/HB/structures.v

You ought to get a better output.

view this post on Zulip Ali Caglayan (Jun 02 2022 at 13:11):

But coqdep is really an internal tool used by coq_makeifle (and dune). Is there another issue that you need help understanding?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2022 at 13:19):

-boot prevents putting user-contrib in scope, hence the failures

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2022 at 13:20):

coqdep can't really be called on .v files in user-contrib

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2022 at 13:20):

it is supposed to be used in local files with the corresponding -R -Q flags if that applies

view this post on Zulip Julien Puydt (Jun 02 2022 at 15:03):

I thought coqdep was the right path to the solution, but I now have doubts about it: it's more about finding deps inside a project, isn't it?

view this post on Zulip Enrico Tassi (Jun 02 2022 at 15:03):

We use it for that.
But what are you trying to use it for?

view this post on Zulip Enrico Tassi (Jun 02 2022 at 15:04):

If your files are already compiled, then the dependencies are written inside the .vo, but I don't think we have a tool to extract them

view this post on Zulip Julien Puydt (Jun 02 2022 at 15:11):

The problem I have is that Coq gets compiled, the Debian package declares it provides coq-{coq-version}+{ocaml-version}. So when a new ocaml/coq gets out, the libcoq-* packages either block the upgrade or get removed: that marks them as incompatible. That's not so bad.

But if I compile the same Coq with the same OCaml but other changes, the packaging doesn't see the problem, but trying to actually do anything triggers errors about incoherent assumptions (or something like this).

So I would like something smarter, so things don't break.

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 15:25):

You can "parse vo files" programmatically with horrible combos of expect and votour. Not recommended, but might work.

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 15:26):

The question then is whether votour lets you extract the right info... the checksums about assumptions?

view this post on Zulip Julien Puydt (Jun 02 2022 at 15:33):

I could also brutally store libcoq-foo depends on libcoq-bar-3.14-2, so when libcoq-bar version 3.14-3 is out, nothing will happen until libcoq-foo gets recompiled against it... but that might block more often that actually needed.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2022 at 15:53):

How is this handled in OCaml?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2022 at 15:53):

As far as I can see that's the same problem

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 15:55):

FWIW, bumping everything at each rebuild seems the easy way out, and anything else is an enhancement on top

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 15:55):

I am not sure why you talk about "blocking"

view this post on Zulip Paolo Giarrusso (Jun 02 2022 at 15:57):

either the rebuild is guaranteed to succeed (so nothing is blocked, the only annoyance is longer package build times and more stuff to download), or the packages might fail building because there were substantial changes — but then the hashes would not match anyway.

view this post on Zulip Julien Puydt (Jun 02 2022 at 19:48):

For OCaml packages, there's a dh_ocaml tool which comes with an ocaml-md5sums helper. The second computes and store codes (say: 9ec98) which the first uses to make libfoo-ocaml provide a libfoo-ocaml-9ec98. And when a package should depend on libfoo-ocaml, dh_ocaml replaces it with a dep on libfoo-ocaml-9ec98.

I think dh_ocaml can probably be adapted as a dh_coq pretty easily (well, it's Perl so I'll probably need to find a perverted but kind soul to lend a hand).

But ocaml-md5sums uses ocamlobjinfo, and that part looks more difficult -- that's why I was interested in coqdep in the first place.

view this post on Zulip Enrico Tassi (Jun 02 2022 at 19:51):

Just play safe and shasum all .vo in a package.

view this post on Zulip Julien Puydt (Jun 02 2022 at 20:03):

I'll see what I can hack up. And I'm wonder if I really need to use Perl...

view this post on Zulip Julien Puydt (Jun 02 2022 at 20:28):

Only .vo files? elpi has .a, .cma, .cmi, .cmo, .cmx, .cmxa and .cmxs too...

view this post on Zulip Julien Puydt (Jun 02 2022 at 20:30):

I have few trivial lines of Python to compute something... that's only a small part of what ocaml-md5sums does (it stores and retrieves the values too).

view this post on Zulip Julien Puydt (Jun 03 2022 at 05:14):

The Debian package libcoq-core-ocaml-dev ships a /var/lib/ocaml/md5sums/libcoq-core-ocaml-dev.md5sums, which looks like this:

0ef2c1d74d0241e078526d7514660bb6 Inductive libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
0f8a06f68e9b73352fba40564febf484 Micromega_plugin__Simplex libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
0f9c13ed18bf622b84f16a2b3d465df9 Ltac_plugin__G_auto libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
1022a6ec2d547d2252dc45c83f4d3766 Nativecode libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
10457b5a56992b84ea5549a54c6a64fb Firstorder_plugin libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
106857d3847cd6657e1e9fedc3c50b21 Vernac libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
1083b848254a9f98a6288ee3374c1e51 Option libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
109909db5f5c1bf546ddf43dc1b67cda Feedback libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
10cb83625bbbfa1e8f30d2f7d002f28a ComDefinition libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
111841eb8594957005bbf57d24f8e17d CObj libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34
1119eca0a3d45671f3ec78603e07f9d3 UnivNames libcoq-core-ocaml-dev libcoq-core-ocaml 8.15.2+dfsg-1 0hk34

and OCaml packages built using libcoq-core-ocaml-dev really declare a dep on libcoq-core-ocaml-0hk34.

view this post on Zulip Julien Puydt (Jun 03 2022 at 05:20):

I found the place in the code where that file is read ; the fields are: md5sum, symbol name, dev package name, runtime package name, version and checksum.

view this post on Zulip Enrico Tassi (Jun 03 2022 at 05:49):

I said .vo because the other files should be in a caml package hence covered by the other tool

view this post on Zulip Julien Puydt (Jun 03 2022 at 06:25):

Ah, the separation libcoq-foo (with .v, .vo, .glob) and libcoq-foo-ocaml (with .cm* .o) is indeed the norm -- only paramcoq strays from this, and I'm going to fix that

view this post on Zulip Julien Puydt (Jun 03 2022 at 19:06):

I have a dh-coq up in Debian's NEW queue. It's not perfect but it should improve matters.

The main issue is that it relies on explicitly declared dependencies, not on detecting them.


Last updated: Feb 06 2023 at 19:03 UTC