[mizar] Fwd: Fwd: Fwd: License for MML

[Josef Urban <josef.urban@gmail.com>]

---------- Forwarded message ----------
From: Lionel Elie Mamane <lionel@mamane.lu>
Date: Tue, Feb 23, 2010 at 12:55 PM
Subject: Re: Fwd: Fwd: License for MML


On Tue, Feb 23, 2010 at 12:16:35AM +0100, Josef Urban wrote:
> On Mon, Feb 22, 2010 at 8:16 AM, Josef Urban <josef.urban@gmail.com> wrote:
>> ---------- Forwarded message ----------
>> From: "David A. Wheeler" <dwheeler@dwheeler.com>
>> Date: Sun, 21 Feb 2010 21:34:49 -0500 (EST)
>> Subject: Re: Fwd: License for MML (xyzzy)

>> So, what license(s) do you pick?  There are various options, but let me at least
>> recommend a set of requirements.  The most common licenses by *far* for
>> community-developed materials are:
>> * CC-BY-SA for non-software (GNU FDL is probably #2, but diminishing)
>> * GNU GPL for software (more than 50%; others common ones are LGPL,
>> BSD-new, and MIT).

The question is "are proofs software". Formally, under "proofs as
programs" they are. But on the other hand, they are also documents for
human consumption, so the kind of things that are usually covered by
CC-BY-SA and friends. Multi-licensing with (at least) one license from
each of the two groups seems the most prudent to me.


>> That doesn't mean you have to use those two licenses, but I believe
>> it is critically important that whatever license(s) you choose are
>> compatible with those two (for their respective domains).

It is also critically important that your licensing be compatible with
other projects that you want to import content from or export content
to.

> It would seem good to dual-license MML under CC-BY-SA and (L)GPL .

> However, the last link above talks about the dangers of dual
> licensing. Is it true that if we dual license as above,
> copying/modifying proofs from Wikipedia/PlanetMath will not be
> possible, because WP/PlanetMath are not released under (L)GPL?

Yes, that is correct. But it will be possible to copy from the MML and
put in WP/PlanetMath.

> Similarly for copying/modifying from Isabelle Archive of Formal
> Proofs (AFP): If we take (L)GPL-ed Isabelle formalization, will it
> be possible to release the Mizar result also under CC-BY-SA?

No, it won't be possible. But it will be possible to make FROM
SCRATCH, without using the Isabelle file, a Mizar article that
implements the same mathematical proof (seen as proof-as-programs, the
same algorithm) and licensed under CC-BY-SA.

Essentially, the MML has a problem because two projects that we want
to be "copyable" from/to have an incompatible license. The MML cannot
keep a uniform licensing situation *and* be copyable both ways with
WP/PlanetMath *and* be copyable both ways with the Isabelle
AFP. Remove one clause from that conjunction and it becomes
possible. Non-uniform licensing is hard to deal with for users (they
have to check each individual file they want to use to know what they
can and cannot do), especially if the intersection of the licenses
over the whole library is empty. It also rapidly becomes messy. The
MML could e.g. require new submissions to be dual-licensed, but
"ports" from other systems can retain their license to minimise the
mess. Also, mark files with their license status clearly!

Another path is to convince AFP and/or WP/PlanetMath to relicense to
dual (L)GPL / CC-BY-SA. I get the impression that AFP will be the
easiest there.

--
Lionel