[isabelle-dev] Supported Poly/ML versions
makarius at sketis.net
Sat Feb 13 16:22:51 CET 2016
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.
More information about the isabelle-dev