Re: package HOL Light?
Le 07/03/2012 16:36, Hendrik Tews a écrit :
> has somebody ever considered to package HOL Light? It's a theorem
> prover that is actively developed by John Harrison. [...]
Not AFAIK.
> One problem is that currently John Harrison doesn't seem to
> provide releases. One would have to package svn snapshots.
Have you suggested him to make proper releases? Have you asked his
opinion on having HOL Light in Debian?
Keep in mind that Debian stable releases are there for 3 years; some
upstreams might not like that old version of their software can be
easily installed, especially for scientific software (sagemath is a
notorious example, but I've heard of others).
> 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
Looks good. But agains, I'd seek upstream approval first.
Cheers,
--
Stéphane
Reply to: