[isabelle-dev] Supported Poly/ML versions

Gerwin Klein Gerwin.Klein at nicta.com.au
Sat Feb 13 23:17:18 CET 2016

> 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.



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.

More information about the isabelle-dev mailing list