Re: Package Moscow ML and HOL
On Sat, Jul 05, 2003 at 11:28:58AM +0200, Sven Luther wrote:
> On Thu, Jul 03, 2003 at 05:36:30PM +0800, ZHAO Wei wrote:
> > On Thu, 2003-07-03 at 14:47, Ralf Treinen wrote:
> > > I remember vaguely that there used to be a licence problem with
> > > Moscow ML. What is its exact licence now?
> >
> > Under the mosml/copyright directory, there are three license files:
> >
> > 1. gpl2 - which is exactly a copy of GPL v2
> > 2. copyright.att - which covers part of the library come from SML/NJ,
> > and as I read it, it's mostly BSDish
> > 3. copyright.cl - covers code come from CAML Light, which looks a little
> > bit strange, but to my unexperienced eyes, looks like a homebrew GPL
> >
> > Anyway, I think it's generally acceptable to put it in Debian main.
> > What's you opinion?
>
> No, it is not. It is the caml-light licence which is the tumbling block.
> It can still be going in non-free though, as the older ocaml used to
> have the exact same licence. Look at the (4 to 5 year old) archives of
> debian-legal for discussion on this.
I even doubt that it can into non-free. As someone else on the
debian-devel list pointed out, GPL and Inria licence are incompatible.
As I understand it: If you redistribute Moscow ML then you also have
to distribute the part that stems from CamlLight under GPL, and of
course you don't have the right to do so. Don't count on convincing
INRIA to re-release Caml Light under GPL (see the mail by Sven).
If your main objective is to packahe HOL then maybe you can migrate
it to OCaml? It seems that there are camlp4 scripts that do this
translation at least partially.
I have sent this message to the debian-ocaml-maint mailing list
instead of debian-devel, this seems a more appriate place for
this discussion.
Cheers -Ralf.
--
Reply to: