[isabelle-dev] Poly/ML

[Clemens Ballarin]

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
>