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, which
       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 they 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>