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

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

   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)
   
The --with ocaml was missing. Now I see 

    hol-light depends on camlp5 v6.04-1 through Eprinter
    hol-light depends on ocaml-nox/ocaml-base-nox v3.12.1-2 through Format

during package build. The dependencies are however still

    Depends: camlp5, ocaml-base-nox-3.12.1

Running ocaml-md5sums alone gives

    hol-light depends on camlp5 v6.04-1 through Eprinter
    hol-light depends on ocaml-nox/ocaml-base-nox v3.12.1-2 through Format
    camlp5 - 6.04-1 q9ic5
    ocaml-nox ocaml-base-nox 3.12.1-2 3.12.1
    W: hol-light doesn't resolve dependency on unit Asttypes
    W: hol-light doesn't resolve dependency on unit Parsetree


Bye,

Hendrik