[isabelle-dev] Poly/ML

[Clemens Ballarin]

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 <boehmes at in.tum.de>:

> 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 <makarius at sketis.net>:
>>
>> >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
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>