[isabelle] Threads tab in Monitor panel (Isabelle2018-RC0)



I'm not doing any funny stuff with system debugging -- just using Isabelle2018-RC0
"out of the box".

I just tried the "isabelle console" thing you suggested, and the output from PolyML
appears reasonable.  I have attached that, as well as the Monitor window from
JEdit, which does not appear reasonable.  I tried forking a thread and the
stats reported by PolyML changed as expected.  So does not look like a PolyML
issue.



On 06/15/2018 03:51 PM, Makarius wrote:
> On 08/06/18 11:46, Eugene W. Stark wrote:
>> I happened to be perusing the tabs in the Monitor panel in Isabelle2018-RC0
>> and noticed that one of the values (threads total? displayed as some kind of
>> red line on my system) has a bizarre value of about -375.  The auto-scaling
>> adjusts for this, making the overall graph pretty useless.
>>
>> This is on Ubuntu 16.04 LTS:
>> Linux 4.4.0-124-generic #148-Ubuntu SMP Wed May 2 13:00:18 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux
>> CPU: Intel(R) Core(TM) i5-4670K CPU @ 3.40GHz
> 
> I haven't seen anything like this myself, but I remember that you have
> used Linux with special system debugging options before: that might
> somehow confuse the built-in system statistics of the Poly/ML 5.7.1
> runtime system (in Isabelle2017 that was Poly/ML 5.6).
> 
> This is how to access that data without anything of Isabelle/ML system
> infrastructure getting in between:
> 
>   $ isabelle console -r
>   Poly/ML> PolyML.Statistics.getLocalStats ();
> 
> You can also fork a few threads and then inspect the statistics again:
> 
>   Poly/ML> Thread.Thread.fork (fn () => OS.Process.sleep
> (Time.fromSeconds 10), []);
> 
> 
> If you feel like it, you may also rebuild the bundled Poly/ML version
> from sources, and experiment with the resulting poly executable:
> 
>   $ cd Isabelle2018-RC0/contrib/polyml-5.7.1-5/src
>   $ ./configure && make compiler && make compiler
>   $ ./poly
>   > PolyML.print_depth 100;
>   > PolyML.Statistics.getLocalStats ();
> 
> Note that this gives you x86_64-linux by default: it can be compared
> directly with Isabelle2018-RC0/contrib/polyml-5.7.1-5/x86_64-linux/poly
> -- the Isabelle default is normally the x86-linux version, provided you
> have the package lib32stdc++6 installed, but building it requires more
> packages and options.
> 
> Anyway, if there is a deeper problem behind it, we should move this to
> the Poly/ML mailing list.
> 
> 
> 	Makarius
> 


Attachment: Screenshot from 2018-06-15 16-06-00.png
Description: PNG image

Attachment: Screenshot from 2018-06-15 16-06-07.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.