[isabelle-dev] Poly/ML

[Makarius]

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