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

[Stéphane Glondu <glondu@debian.org>]

Sorry for taking so much time to reply...

Le 26/03/2012 10:23, Hendrik Tews a écrit :
> I believe I fixed all the issues in the package hol-light.
> [...]

It looks good from a technical point of view. However:

 - Jordan/float.ml is copyright Thomas C. Hales, and under a different
   license (GPL). This should be mentioned in debian/copyright.
 - There are many other copyright holders that appear in "git grep -i
   copyright" output and don't appear in debian/copyright. It looks like
   lots of them are distributed under the same license terms as HOL
   Light, so it should be fine... but I'd add "and others" after John
   Harrison's name. However, please check the licenses and make explicit
   in debian/copyright files that are under a different license
 - Putting your packaging work under GPL makes your patches GPL, which
   would make me reluctant to merge them if I were upstream. Is that
   intentional? The general practice is to put debian/* under the same
   license(s) as upstream, as if it could be merged upstream.
 - Please refer to:
     http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
   in the Format field of debian/copyright.


Cheers,

-- 
Stéphane