Hi Sascha,
Thanks for the clarification. Since Z3 needs to be knowingly
activated, I agree this should be sufficient. I did not imply
distributing Z3 with Isabelle was not legal, merely some users may
want to know that they will be downloading software for non-commercial
use only ahead of time.
Clemens
Quoting Sascha Boehme <[email protected]>:
Hi Clemens,
Please note that Z3's license explicitly allows distribution for
non-commercial purposes such as teaching, academic research or public
demonstrations. Although Isabelle's BSD-style license would allow
Isabelle to be applied to commercial applications, too, it still is a
research product and non-commercial itself. As long as we never plan
to turn theorem proving with Isabelle into a business, we should be
able to distribute Z3 with Isabelle. Furthermore, we require users of
Z3 within Isabelle to explicitly state the non-commercial usage (i.e.,
an explicit step to optionally enable Z3 for Isabelle), and include
Z3's license. I'm not a laywer, but to me this setup looks
sufficiently legal.
Cheers,
Sascha
Clemens Ballarin wrote:
Thank you, Jasmin and Makarius. I managed to replace my Poly/ML
installation by the one included in Isabelle2011.app. It took 15
minutes to download this, though.
I noted that the bundle contains software that is free for
non-commercial use only (z3). This might be problematic for some
users.
Clemens
Quoting Makarius <[email protected]>:
>On Tue, 21 Jun 2011, Jasmin Blanchette wrote:
>
>>Am 21.06.2011 um 23:11 schrieb Clemens Ballarin:
>>
>>>After updating my Isabelle repository (which I haven't done
>>>for quite a while) Poly/ML stopped to start up. I have 5.2
>>>and according to the release notes this is no longer
>>>supported. Do I need to build 5.4 for myself or do we provide
>>>a pre-built version for MacOS 10.5 somewhere? The Isabelle
>>>download page is surprisingly silent about Poly/ML nowadays.
>>
>>There might be a more official way of doing it, but what worked
>>for me on Mac and Linux was to install the full Isabelle2011
>>bundle and cannibalize it, i.e. steal its interesting
>>third-party components. For example,
>>
>>ln -s /Applications/Isabelle2011.app/Isabelle/contrib/polyml ~/polyml
>>
>>will create a symlink that will be automatically picked up by
>>the repository version of Isabelle (if your repository is
>>somewhere under ~).
>
>Yes, I also recommend to reuse things from the last official
>release as much as possible, and only replace parts when there is
>a real need for update.
>
>The automatic "picking up" of most contrib components is more and
>more being discontinued. I.e. except for polyml it would be some
>"init_component" line in etc/settings or addition to
>etc/components.
>
>
> Makarius
>
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
