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 the people who show up here to say 
> that they knew that already.

I used this a while ago, with the help of Makarius, to debug a looping 
sublocale invocation.

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

Clemens

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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


Some years ago David Matthews simplified the treatment of exceptions in 
the run-time system, to reduce the overhead. As a consequence of that, a 
partial "handle" already counts like a total one, i.e. the trace is 
truncated there.


Asking David the same question as above, he pointed out that the debugger 
can do this and much more. It only needs to be wrapped-up for actual use.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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



Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev