<div dir="ltr">Hi Makarius and <span style="font-size:12.8px;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">Gerwin,</span><div><span style="font-size:12.8px;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">  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 <span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">Makarius worries with open source, I'm the first who enjoys open source.</span></span></div><div><span style="font-size:12.8px;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></span></div><div><span style="font-size:12.8px;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">Kind Regards,</span></span></div><div><span style="font-size:12.8px;text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><span style="font-size:small;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">José M.</span></span></div></div><div class="gmail_extra"><br><div class="gmail_quote">2018-06-28 12:06 GMT+02:00 Makarius <span dir="ltr"><<a href="mailto:makarius@sketis.net" target="_blank">makarius@sketis.net</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 28/06/18 07:55, José Manuel Rodriguez Caballero wrote:<br>
> <br>
>   Motivated by my exchange of experiences with professionals using<br>
> proof-assistants like Coq for commercial purposes, I would like to ask<br>
> the following question is: which are the regulations of Isabelle for<br>
> commercial use? For example, if a software company is interested in<br>
> selling .thy files to clients, which conditions apply?<br>
<br>
</span>(Why is this on isabelle-dev? It is not relevant to the Isabelle<br>
development process. Isabelle theory development is a normal user activity.)<br>
<br>
Isabelle itself is subject to the very liberal BSD-style license scheme.<br>
Its add-on tools might have other Open Source licenses. The overall<br>
Isabelle application taken together converges to the strictest Open<br>
Source license of any of its components, similar to a Linux distribution.<br>
<br>
Whatever you produce yourself with the Isabelle application is *not*<br>
affected by any of this. You can publish your own outcome by whatever<br>
license you like, even a non-Open-Source license.<br>
<br>
<br>
But note that after some decades of Open Source culture, almost<br>
everything of relevance is published Open Source now. Even if you "sell"<br>
sources, you can often tell the one who pays for it that it is vital to<br>
publish the results under such a reusable license: this will allow other<br>
people in the same situation to build on it and improve the body of<br>
available material in the next round of the universal iteration process.<br>
<br>
Ideally it will all end up in the Archive of Formal Proofs eventually,<br>
where it is maintained "automagically", i.e. updated to new Isabelle<br>
versions as they emerge. This is a privilege of the participants in the<br>
Open Source cartel.<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
        Makarius<br>
</font></span></blockquote></div><br></div>