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?
Why are you calling coqdep on user-contrib?
You should be calling coqdep
on the .v file.
Don't worry about -boot
that just adds deps on files from the stdlib which you don't need.
coqdep is pretty dumb so it is not clever enough to understand you fed it a load of nonsense.
If you try
$ coqdep /usr/lib/ocaml/coq/user-contrib/HB/structures.v
You ought to get a better output.
But coqdep is really an internal tool used by coq_makeifle (and dune). Is there another issue that you need help understanding?
-boot prevents putting user-contrib in scope, hence the failures
coqdep can't really be called on .v files in user-contrib
it is supposed to be used in local files with the corresponding -R -Q flags if that applies
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?
We use it for that.
But what are you trying to use it for?
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
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.
You can "parse vo files" programmatically with horrible combos of expect and votour. Not recommended, but might work.
The question then is whether votour lets you extract the right info... the checksums about assumptions?
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.
How is this handled in OCaml?
As far as I can see that's the same problem
FWIW, bumping everything at each rebuild seems the easy way out, and anything else is an enhancement on top
I am not sure why you talk about "blocking"
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.
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.
Just play safe and shasum all .vo in a package.
I'll see what I can hack up. And I'm wonder if I really need to use Perl...
Only .vo files? elpi has .a, .cma, .cmi, .cmo, .cmx, .cmxa and .cmxs too...
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).
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.
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.
I said .vo because the other files should be in a caml package hence covered by the other tool
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
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: Oct 13 2024 at 01:02 UTC