[mizar] Re: Fwd: License for MML

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

Dear all,

thanks a lot for all your responses! Taking David Wheeler's comments:

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).
>
> 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).  Options include:
> * Dual licensing with both CC-BY-SA and the GNU GPL (version 2 or
> greater), if you wanted to require by law that further contributions
> be shared.
> * Dual licensing CC-BY-SA and GNU LGPL (version 2 or greater)
> * BSD-new (http://www.opensource.org/licenses/bsd-license.php).  That
> can be combined with CC-BY-SA, GPL GNU, and many others.
>
> For more discussion on licensing, you might want to look here:
> http://www.dwheeler.com/essays/gpl-compatible.html

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?

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?

Or does translation/formalization in Mizar count as sufficiently novel
work anyway (and this is a non-issue)? (I would not claim that about
my translation of Mizar to TPTP, but the law might have a different
opinion).

Is there any advice (or good adopted conventions) as to how exactly
should the MML maintainers keep track (and meet requirements) of the
CC-BY-SA and (L)GPL copyrights by authors/maintainers/refactorers?

Thanks again,
Josef Urban