[isabelle-dev] Poly/ML

[Sascha Boehme]

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