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