[isabelle-dev] Supported Poly/ML versions

[Gerwin Klein]

> On 14.02.2016, at 02:22, Makarius <makarius at sketis.net> wrote:
>
> On Sat, 13 Feb 2016, Lars Hupel wrote:
>
>>>  * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a
>>>    detailed exception trace. Note that this needs to be done with
>>>    isabelle_process or isabelle console, since PIDE requires socket I/O
>>>    and Poly/ML 5.3.0 does not work with that anymore.
>>
>> IMHO this sounds too obscure to be useful. How many users are actually aware of that possibility?
>
> Maybe 2-3 people on this mailing list, but this is only a guess. So lets make a constructive proof and count the people who show up here to say that they knew that already.
>
> It is indeed all very obscure.  Time is better invested in making the Poly/ML 5.6 debugger work for the Pure bootstrap as well, and add some explicit support for exceptions to it.

I agree. No need from my side to hold on to the older polyml versions.

Cheers,
Gerwin

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.