Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover
Le 16/03/2012 11:36, Hendrik Tews a écrit :
> a first version of the hol-light package is available at
> git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git
Even though I've pushed (cosmetic) stuff there, I've not yet fully
looked at everything.
> I believe the compiled syntax extension will only work with the
> camlp5 version it was compiled. Therefore I would like to have a
> dependency
>
> camlp5-${F:Camlp5ABI},
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)
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).
> 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.
Cheers,
--
Stéphane
Reply to: