Re: Bug#663754: ITP: hol-light -- HOL Light theorem prover
On 03/21/2012 10:23 PM, Hendrik Tews wrote:
> Stéphane Glondu writes: 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
>
> [snip]
>
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).
Regards,
--
Mehdi Dogguy مهدي الدڤي
http://dogguy.org/
Reply to: