Re: [isabelle-dev] a question about regulations
On 29/06/18 08:08, José Manuel Rodriguez Caballero wrote: > Thank you by the information. I sorry if this mailing list was not the > best to ask this legal question, I did not find another one more > appropriated for this subject. By default you can post everything on isabelle-users, unless it really refers to the ongoing Isabelle development process. The larger audience on isabelle-users might actually have more legal experts. > With respect to Makarius worries with > open source, I'm the first who enjoys open source. I am actually not worried about open source, I am worried about the remaining minority that thinks it can economically survive with the obsolete closed-source model. Even Microsoft has joined the Open Source movement now, and will be soon running Github. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] a question about regulations
Hi Makarius and Gerwin, Thank you by the information. I sorry if this mailing list was not the best to ask this legal question, I did not find another one more appropriated for this subject. With respect to Makarius worries with open source, I'm the first who enjoys open source. Kind Regards, José M. 2018-06-28 12:06 GMT+02:00 Makarius : > On 28/06/18 07:55, José Manuel Rodriguez Caballero wrote: > > > > Motivated by my exchange of experiences with professionals using > > proof-assistants like Coq for commercial purposes, I would like to ask > > the following question is: which are the regulations of Isabelle for > > commercial use? For example, if a software company is interested in > > selling .thy files to clients, which conditions apply? > > (Why is this on isabelle-dev? It is not relevant to the Isabelle > development process. Isabelle theory development is a normal user > activity.) > > Isabelle itself is subject to the very liberal BSD-style license scheme. > Its add-on tools might have other Open Source licenses. The overall > Isabelle application taken together converges to the strictest Open > Source license of any of its components, similar to a Linux distribution. > > Whatever you produce yourself with the Isabelle application is *not* > affected by any of this. You can publish your own outcome by whatever > license you like, even a non-Open-Source license. > > > But note that after some decades of Open Source culture, almost > everything of relevance is published Open Source now. Even if you "sell" > sources, you can often tell the one who pays for it that it is vital to > publish the results under such a reusable license: this will allow other > people in the same situation to build on it and improve the body of > available material in the next round of the universal iteration process. > > Ideally it will all end up in the Archive of Formal Proofs eventually, > where it is maintained "automagically", i.e. updated to new Isabelle > versions as they emerge. This is a privilege of the participants in the > Open Source cartel. > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] a question about regulations
On 28/06/18 07:55, José Manuel Rodriguez Caballero wrote: > > Motivated by my exchange of experiences with professionals using > proof-assistants like Coq for commercial purposes, I would like to ask > the following question is: which are the regulations of Isabelle for > commercial use? For example, if a software company is interested in > selling .thy files to clients, which conditions apply? (Why is this on isabelle-dev? It is not relevant to the Isabelle development process. Isabelle theory development is a normal user activity.) Isabelle itself is subject to the very liberal BSD-style license scheme. Its add-on tools might have other Open Source licenses. The overall Isabelle application taken together converges to the strictest Open Source license of any of its components, similar to a Linux distribution. Whatever you produce yourself with the Isabelle application is *not* affected by any of this. You can publish your own outcome by whatever license you like, even a non-Open-Source license. But note that after some decades of Open Source culture, almost everything of relevance is published Open Source now. Even if you "sell" sources, you can often tell the one who pays for it that it is vital to publish the results under such a reusable license: this will allow other people in the same situation to build on it and improve the body of available material in the next round of the universal iteration process. Ideally it will all end up in the Archive of Formal Proofs eventually, where it is maintained "automagically", i.e. updated to new Isabelle versions as they emerge. This is a privilege of the participants in the Open Source cartel. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] a question about regulations
Isabelle is distributed under a BSD 3-clause license. The only restrictions for Isabelle itself are (see COPYRIGHT file): * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. * Neither the name of the University of Cambridge or the Technische Universitaet Muenchen nor the names of their contributors may be used to endorse or promote products derived from this software without specific prior written permission. This is very permissive. There are no restrictions for other .thy files, only the usual copyright and other IP laws apply. We have commercial contracts that deliver .thy files quite routinely. Cheers, Gerwin > On 28 Jun 2018, at 07:55, José Manuel Rodriguez Caballero > wrote: > > Dear Sir or Madam, > > Motivated by my exchange of experiences with professionals using > proof-assistants like Coq for commercial purposes, I would like to ask the > following question is: which are the regulations of Isabelle for commercial > use? For example, if a software company is interested in selling .thy files > to clients, which conditions apply? > > Sincerely yours, > José M.l Rodriguez Caballero > Université du Québec à Montréal > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
