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

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

One more concern, after remembering this:
http://gowers.wordpress.com/2009/01/27/is-massively-collaborative-mathematics-possible/
.

The licensing and related treatment of such collaborative scientific
projects probably should not forget about attribution (speaking in
favor of CC-BY SA). But I also wonder how much is the Linux-kernel
"signing-off contributions" model an attribution-like mechanism on top
of GPL, in practice giving similar value as CC-BY-SA. Any ideas?

Josef
(I have contacted the Software Freedom Law Center last week, as
Stephan Schulz suggested)


On 2/23/10, Josef Urban <josef.urban@gmail.com> wrote:
> ---------- 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
>