NOTE: This FAQ is a simplified explanation and not legally binding in its details. See the license text itself for precise details. Who owns the MML? The owner, as far as copyright is concerned, of the MML is the SUM (in Polish: Stowarzyszenie Uzytkownikow Mizara, in English Association of Mizar Users - AMU). However, the SUM permits other people to use and redistribute the MML under some conditions. Each contributor also gets special permission to do anything he wishes, without any condition, with his own contribution. Who can use the MML? Anybody can use the MML for any purpose whatsoever without any restriction nor obligation, as long as "use" does not include redistributing (giving a copy) of (part of) the MML, nor any article using the MML, to any third party. "Using" the MML typically entails using definitions / theorems / schemas / notations / ... from the MML to write new proofs, or to add, delete or modify definitions / proofs / ... in the MML. What do I have to do if I want to redistribute the MML, or part thereof, unmodified? You have to inform the people you give the MML to of their rights and obligations. Specifically, include the files COPYING.* in the copy you redistribute. You may not forbid other people to exercise the rights given to them by the SUM. What do I have to do if I want to redistribute (part of) the MML, modified or augmented, or an article that invokes (a) theorem(s) / notation(s) / scheme(s) / ... from the MML? These instructions assume you do not wish to assign copyright of your work to the SUM. 0) Don't remove or alter the SUM copyright notice. 1) Add to the header of the file: Copyright © YEAR_OF_MODIFICATION YOUR NAME If your employer owns your work, that would be: Copyright © YEAR_OF_MODIFICATION YOUR_EMPLOYER 2) You have to give others the same rights you got, that is you have to license your modifications and your new articles under the GNU GPL v3 (or later), the Creative Commons BY-SA v3 (or later), or (preferably) both. If your employer owns your work, this requires his/her permission. 3) Briefly describe what you changed as a comment in the header or footer. E.g.: "Changed proof of theorem Cayley_Hamilton to follow proof by Shamir and Slotzky in their book 'Introduction to Linear Algebra for Dummies - the Collegiate Edition'" or "Add new redefinition of real numbers as sub-category of surreal (Conway) numbers" 4) Include the files COPYING.* in what you redistribute. The likely (and intended) effect of this is that sooner or later your modifications will become public, even if you choose to distribute it to precious few: some of them will redistribute to someone that will redistribute, ... and someone in the chain will just make it public. What do I have to do if I want my enhancements to go into the "official" version of the MML, distributed by mizar.org? 1) Sign the Fiduciary Licensing Agreement, if you have not already done so. If you live in France, sign the FLA again even if you did so in the past. Also for other jurisdictions that do not allow you to assign future work. 2) Update the SUM copyright line to include the current year. The format is: comma-separated list of disjoint singletons and hyphen-separated ranges of years, in increasing order. E.g. for modifications you did in 2010, change Copyright © 1989-1995 Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara, Białystok, Poland). to Copyright © 1989-1995,2010 Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara, Białystok, Poland). Change Copyright © 1989-2009 Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara, Białystok, Poland). to Copyright © 1989-2010 Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara, Białystok, Poland). For new articles, put in the header: Copyright © 2010 Association of Mizar Users (Stowarzyszenie Uzytkownikow Mizara, Białystok, Poland). 3) Send the signed FLA, along with your enhancements to the MML, to the Mizar project. Can I write a program that uses the MML? Yes, you can. However, if you wish to *distribute* this program, please observe the following: no restriction is put on your program as long as it does not contain (part of) the MML itself. Your program can use the MML as data. E.g. you can write a Mizar implementation, a proof transformer / converter, ... In this case, no restriction is put on your program. However, the result of running your program over the MML (e.g. proofs converted to Isar or HOL Light, beautified proofs, ...) is still covered by the SUM copyright and subject to the same permissions and conditions as the original MML. If (part of) the MML ends up in your program itself, even in another shape than text files (e.g. as a parse tree or memory dump that is in the executable file), then your whole program needs to be released under the GNU GPL, or a license compatible with it (e.g. 2-clause BSD, X11/MIT, ...). See http://www.gnu.org/licenses/license-list.html#GPLCompatibleLicenses A good rule of thumb is: If - your program compiles and links completely without the build process using (part of) the MML (in any shape) at all; - the compiled program is byte-to-byte identical to the compilation in the presence of the MML; - the compiled program is independently useful (for example, it would be useful on an article written in the Mizar language that does not use the MML); then there is probably no restriction on your program. Your program can e.g. use the MML in its automated test-suite: when you run the test-suite, your program is already fully compiled. Obviously, if you distribute the MML along with your program, you still have to obey the conditions for the MML. I want to do something not allowed by the license. Get in touch with the SUM, explaining what you want to do, why you cannot do it under the terms of the GNU GPL or CC-BY-SA, and why the SUM should allow that. If your project advances science ands its broad availability to humankind, you may get permission from the SUM. If you wish to commercially exploit the MML, the SUM may be willing to sell you a license that fits your needs. E.g. if you want to integrate the MML into an interactive exercise system for mathematics system and you sell (access to) this system. What is the story with the two licences? Do I have to obey both? No, you may choose either of them, and obey only that one. Please indicate your choice clearly. All instructions in this FAQ refer to the common denominator between the two licenses. I submitted an enhancement to a MML article, and it got accepted. Can I do anything (e.g. sell copies of or a commercial license on) the whole article? I wrote an article for the MML. Can I do anything with future versions of the article? No, the special permission to contributors to do anything they wish applies only to your own work. So, in the first example, it applies only to your enhancement, not the whole article (that includes work by other people). Naturally, if you cooperate with (or get permission from) all other authors of all previous versions of this article, you all together as a group may do anything you wish. Similarly, if you submit a new article to the MML, the special permission applies only to your original version (plus any enhancement you make), not to any version that includes any change by another contributor. May I distribute a printed version of (part of) the MML? Yes, and e.g. a PDF counts as "printed version", but you must: 1) Give people an electronic copy of the MML in source form (preferred form for modification) on a medium customary at the time, or a URL/URI to a free of charge download link for the MML in source format. If you print the unmodified MML, this can be a link to the (version of the MML you print) hosted at mizar.org, or any other download server, such as your own. If you modified the MML before printing, you have to organise your own download service. 2) Mention the SUM copyright, and state that the articles are free to use / modify / redistribute under the GPL and/or the CC-BY-SA, and include a copy of the GPL and/or CC-BY-SA, or at least the URL to the license(s). 3) Effectively allow people to exercise their rights. E.g., you may not use DRM techniques or anti-photocopy backgrounds to keep people from further distributing / sharing / copying the printed version. If you e.g. publish a MML article as part of a journal, this restriction does not apply to your whole journal, nor the whole issue in which the MML article appears, only the MML article itself. You are not legally obligated to publish the pretty-printing program you used (if any), but it would be appreciated if you did and licensed it under a Free / Open Source license.