NAME¶

dh_coq - computes Coq packages provides, and partial dependencies

SYNOPSIS¶

dh_coq [debhelper options]

DESCRIPTION¶

dh_coq is a debhelper program that is responsible for filling the ${coq:Provides} and ${coq:Depends} substitutions and adding them to substvars files.

It only acts on a single type of binary packages: those shipping Coq theories. Those are usually names libcoq-XXXX, but neither libcoq-XXX-ocaml nor libcoq-XXX-ocaml-dev: those are OCaml library packages and managed by dh_ocaml.

On those packages it takes responsibility for, it will look of the Coq compiled files and compute a checksum. This checksum is stored in the registry in /var/lib/coq/md5sums/, and already allows to say the current package provides a checksummed-versioned virtual package. The build-depends are then scanned, and their checksums are retrieved, so the current package depends also on checksummed virtual packages.

The reason for this setup is that without the checksum, with just dependencies on libcoq-XXX, ABI breakage can happen, because a new libcoq-XXX won't be seen as incompatible, be installed and trigger incoherent assumptions errors. With fully checksummed packages, apt-get will not upgrade anything until all packages have migrated to the new ABI.

The dependencies aren't extracted automatically from the compiled project, but from the build-depends of the built package, so it's crucial that those are accurate.

FILES¶

debian/libcoq-XXX.volist

By default, the list of Coq compiled files shipped by your package is automatically computed, but if you need to override this, this files makes it possible to fix the list. Files are considered relative to the package build directory.

SEE ALSO¶

debhelper(7)

This program is a part of debhelper.

AUTHORS¶

Julien Puydt <jpuydt@debian.org>