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
