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

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

Stéphane Glondu writes:

   >   I: hol-light: arch-dep-package-has-big-usr-share 17934kB 100%
   
   It's not an error, it's an info :-) Please override it with a useful
   comment, and don't split the package.
   
Done.

   It should be possible to compile stuff so that your:
   
     #use "hol.ml";;
   
   could be replaced by a much faster:
   
     #load "hol.cma";;
   
   Besides, the package would also be of better quality, because it would
   not be available if the compilation of hol.ml failed.
   
I already thought about this, but

1. I believe upstream deliberately decided to not compile hol.ml.
   The Debian package should follow this. Note that upstream
   advises users to type ``#use "hol.ml";;'' into ocaml in order
   to use HOL Light.

2. With compiling hol.ml you would gain very little, because (I
   believe) most of its material are theorems and proofs. That
   is, most of hol.ml are constants, which are rather computation
   intensive. So even if you compile it, loading would take about
   2 minutes, and, if one of the proofs is wrong, loading would
   fail, although the compilation succeeded. (HOL Light is
   different from Coq, there is no hol-lightc!)

To ensure quality I want to run the test suite (file holtest).
But running this takes several hours. Some of those tests require
external tools (eg prover9, zchaff). I first have to find out
which of those test should work on a Debian installation.

Bye,

Hendrik