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

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

Stéphane Glondu <glondu@debian.org> writes:

   Sorry for taking so much time to reply...

no problem!

    - Jordan/float.ml is copyright Thomas C. Hales, and under a different
      license (GPL). This should be mentioned in
      debian/copyright.

done, similarly for Minisat/zc2mso/zc2mso.C

    - 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

I checked the copyright statements and added appropriate entries
in debian/copyright. However, the files Unity/* and pa_j* have no
license statement and are copyright by somebody else. I ask
upstream to provide a license for those.

    - 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.

changed.

Thanks for your comments!

Bye,

Hendrik