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

[Stéphane Glondu <glondu@debian.org>]

Le 18/03/2012 21:54, Hendrik Tews a écrit :
> 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

camlp5 is a development package, not a runtime one. From your
description, hol-light would also be a development package. Did you try
to run dh_ocaml with --runtime-map (the same way as camlp5 does) in
hol-light instead?


Cheers,

-- 
Stéphane