[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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


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

- 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.



Reply to: