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 so
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
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 "hol.ml
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
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.
I
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 wi
Stéphane Glondu 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 "-".
This is caused by u
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 ocaml-nox/ocaml-
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
instal
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 extens
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
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 am
Hi,
On Tue, Mar 13, 2012 at 13:38, Hendrik Tews wrote:
> * License : HOL Light licence
According to the google code page, it's actually BSD.
Laurent.
--
To UNSUBSCRIBE, email to debian-wnpp-requ...@lists.debian.org
with a subject of "unsubscribe". Trouble? Contact listmas...@lists.de
Package: wnpp
Owner: Hendrik Tews
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 theorem prover
HOL
14 matches
Mail list logo
