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
--
To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org
Archive:
http://lists.debian.org/20330.18151.956788.248...@blau.inf.tu-dresden.de
