Re: [isabelle-dev] a question about regulations

2018-06-29 Thread Makarius
On 29/06/18 08:08, José Manuel Rodriguez Caballero wrote: >   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. By default you can post everything on isabelle-users, unless it

Re: [isabelle-dev] a question about regulations

2018-06-29 Thread 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,

Re: [isabelle-dev] a question about regulations

2018-06-28 Thread 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

Re: [isabelle-dev] a question about regulations

2018-06-28 Thread Gerwin.Klein
Isabelle is distributed under a BSD 3-clause license. The only restrictions for Isabelle itself are (see COPYRIGHT file): * Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. * Redistributions in binary form must

[isabelle-dev] a question about regulations

2018-06-28 Thread José Manuel Rodriguez Caballero
Dear Sir or Madam, 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