[isabelle-dev] a question about regulations

[José Manuel Rodriguez Caballero]

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 <makarius at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180629/06d162f8/attachment-0002.html>