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 <makar...@sketis.net>: > 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