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
- A number of external tools that can be used with HOL Light are