package HOL Light?

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

Hi,

has somebody ever considered to package HOL Light? It's a theorem
prover that is actively developed by John Harrison. There is a
group of people that try to formalize the proof of the Kepler
conjecture in Hol Light. 

One problem is that currently John Harrison doesn't seem to
provide releases. One would have to package svn snapshots.


What would be the right procedure to follow?

1. file an ITP bug for HOL Light
2. dom-new-git-repo hol-light ...
3. do the packaging
4. post an RFS here

?

Bye,

Hendrik