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