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

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

   There is already an automatically computed camlp5 ABI (have a look at
   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)
   
Maybe because there is no executable and the only cmo is
installed in /usr/share/hol-light?

   By the way, if one manages to use this automatic ABI, care should be
   taken w.r.t. #549679. Basically, until this bug is fixed, the package
   should be arch:any (because the ABI depends on the architecture, at
   least theoretically).

Can the package still install sources and the cmo in
/usr/share/hol-light in the arch:any case?

   > This does of course not work, because there is no package
   > camlp5-6.04. Can we change the camlp5 package to provide
   > camlp5-${F:Camlp5ABI} ?
   
   Before doing that, I'd like to understand why dh_ocaml is not suitable.
   
I wasn't really aware of these ABI hashes. 

Bye,

Hendrik