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

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

Hi,

I believe I fixed all the issues in the package hol-light.

- I imported a new upstream version, which is distributed now
  with a BSD 2 clause license

- The camlp5 dependencies are right

- hol-light is a binary package with a lintian override for
  arch-dep-package-has-big-usr-share

- One test is performed during package build: This tests loads
  the HOL Light base (in file hol.ml) and the
  arithmetic-geometric mean example (Library/agm.ml).

- The upstream test suite is installed as
  /usr/share/hol-light/holtest, with instruction on howto run it
  in README.Debian.

- A number of external tools that can be used with HOL Light are
  in Suggests.

Bye,

Hendrik