Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover

[Hendrik Tews <tews@os.inf.tu-dresden.de>]

Stéphane Glondu <glondu@debian.org> writes:

   camlp5's provides). The question is: why dh_ocaml doesn't put it in
   hol-light? I'll have a deeper look at this (but feel free to beat me on
   this)

I believe the problem is that in
/var/lib/ocaml/md5sums/camlp5.md5sums the runtime field is "-".

This is caused by using "--runtime-map camlp5" in the rules file
of camlp5, which sets only the development package name.

If I build camlp5 with --runtime-map camlp5:camlp5 then
camlp5.md5sums has "camlp5" as runtime field and then hol-light
gets the expected dependencies:

    Depends: camlp5, ocaml-base-nox-3.12.1, camlp5-q9ic5


Bye,

Hendrik