Re: [isabelle-dev] Supported Poly/ML versions

2016-02-14 Thread Clemens Ballarin
On 13 February, 2016 16:22 CET, Makarius wrote: > > 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

Re: [isabelle-dev] Supported Poly/ML versions

2016-02-13 Thread Lawrence Paulson
A pity that even this one is necessary. Has tracing somehow got worse since then, and can’t that be reversed? Larry > On 13 Feb 2016, at 13:42, Makarius wrote: > > * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a >detailed exception trace. Note that

Re: [isabelle-dev] Supported Poly/ML versions

2016-02-13 Thread Makarius
On Sat, 13 Feb 2016, Lawrence Paulson wrote: A pity that even this one is necessary. Has tracing somehow got worse since then, and can’t that be reversed? On 13 Feb 2016, at 13:42, Makarius wrote: * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a

Re: [isabelle-dev] Supported Poly/ML versions

2016-02-13 Thread Lars Hupel
> This question is relevant for the transition of isatest to Jenkins: many > isatest jobs are there to run old Poly/ML versions, and these CPU cycles > could be spared or put into better use. Interesting, I wasn't even aware of that. > * Old Poly/ML 5.3.0 is still needed in rare situations to

Re: [isabelle-dev] Supported Poly/ML versions

2016-02-13 Thread Makarius
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