[isabelle-dev] a question about regulations

[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