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

2012-04-24 Thread Hendrik Tews
Hi, there is a new upstream svn commit that fixes the license issues. The package contains now this latest version together with a rather long copyright file, that lists all the exceptions form the general hol light license. I have not yet created a signed tag in the repository, but I would do

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

2012-03-26 Thread Hendrik Tews
Hi, I believe I fixed all the issues in the package hol-light. - I imported a new upstream version, which is distributed now with a BSD 2 clause license - The camlp5 dependencies are right - hol-light is a binary package with a lintian override for arch-dep-package-has-big-usr-share - One

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

2012-03-21 Thread Hendrik Tews
Stéphane Glondu writes: I: hol-light: arch-dep-package-has-big-usr-share 17934kB 100% It's not an error, it's an info :-) Please override it with a useful comment, and don't split the package. Done. It should be possible to compile stuff so that your: #use

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

2012-03-20 Thread Stéphane Glondu
Le 19/03/2012 13:18, Hendrik Tews a écrit : camlp5 is a development package, not a runtime one. From your description, hol-light would also be a development package. I am sorry, but I don't understand the distinction between runtime and development packages and its importance for

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

2012-03-19 Thread Hendrik Tews
Stéphane Glondu writes: camlp5 is a development package, not a runtime one. From your description, hol-light would also be a development package. I am sorry, but I don't understand the distinction between runtime and development packages and its importance for packaging and dh_ocaml.

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

2012-03-18 Thread Hendrik Tews
Stéphane Glondu glo...@debian.org writes: camlp5's provides). The question is: why dh_ocaml doesn't put it in hol-light? I'll have a deeper look at this (but feel free to beat me on this) I believe the problem is that in /var/lib/ocaml/md5sums/camlp5.md5sums the runtime field is -.

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

2012-03-18 Thread Stéphane Glondu
Le 18/03/2012 21:54, Hendrik Tews a écrit : I believe the problem is that in /var/lib/ocaml/md5sums/camlp5.md5sums the runtime field is -. This is caused by using --runtime-map camlp5 in the rules file of camlp5, which sets only the development package name. If I build camlp5 with

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

2012-03-16 Thread Hendrik Tews
Hi, a first version of the hol-light package is available at git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git Comments are welcome! The current package has the following issues: - the precise upstream license is not clear yet, I've asked upstream about it, see the messages at

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

2012-03-16 Thread Stéphane Glondu
Le 16/03/2012 11:36, Hendrik Tews a écrit : a first version of the hol-light package is available at git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git Even though I've pushed (cosmetic) stuff there, I've not yet fully looked at everything. I believe the compiled syntax

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

2012-03-16 Thread Hendrik Tews
There is already an automatically computed camlp5 ABI (have a look at camlp5's provides). The question is: why dh_ocaml doesn't put it in hol-light? I'll have a deeper look at this (but feel free to beat me on this) Maybe because there is no executable and the only cmo is

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

2012-03-16 Thread Hendrik Tews
camlp5's provides). The question is: why dh_ocaml doesn't put it in hol-light? I'll have a deeper look at this (but feel free to beat me on this) The --with ocaml was missing. Now I see hol-light depends on camlp5 v6.04-1 through Eprinter hol-light depends on

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

2012-03-13 Thread Hendrik Tews
Package: wnpp Owner: Hendrik Tews hend...@askra.de Severity: wishlist * Package name: hol-light Version : 20120312 Upstream Author : John Harrison * URL or Web page : http://www.cl.cam.ac.uk/~jrh13/hol-light/ * License : HOL Light licence Description : HOL Light

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

2012-03-13 Thread Laurent Fousse
Hi, On Tue, Mar 13, 2012 at 13:38, Hendrik Tews hend...@askra.de wrote: * License         : HOL Light licence According to the google code page, it's actually BSD. Laurent. -- To UNSUBSCRIBE, email to debian-bugs-dist-requ...@lists.debian.org with a subject of unsubscribe. Trouble? Contact

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

2012-03-13 Thread Hendrik Tews
Laurent Fousse writes: According to the google code page, it's actually BSD. The text in the LICENSE file [1] actually differs from the BSD license. It requires that changes are clearly documented and it does not require that redistribution in binary form reproduces the copyright. I