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

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

Mehdi Dogguy <mehdi@debian.org> writes:

   I beleive an intermediate solution would be to compile it on build time
   and not ship it so that we know it works. (I didn't check what tests
   are performed during build time though to see if my proposal makes sense
   in this specific case).

There were no tests performed during package build. The complete
test suite runs for several hours. I am still working on a
version that performs all tests that are possible on a Debian
system. My suggestion would be that the package maintainer runs
these tests once before uploading.

As I said before, compiling hol.ml doesn't make much sense IMHO.
I've added now an override_dh_auto_test entry that performs some
of the tests of the upstream test suite. Each of those tests
loads some file on top of hol.ml. 

Currently I do 4 of the about 110 tests. Each of them takes about
90 seconds on my Core Duo @ 2.80GHz. How much time should I spend
on testing during package build?

Bye,

Hendrik