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



Hello Makarius and Eugene,


I have the same effect (except with a different values).

My Computer:
MacBook Pro (Retina, 15-inch, Mid 2015)
2,5 GHz Intel Core i7
16 GB 1600 MHz DDR3
High Sierra 10.13.4


Isabelle version (more-or-less RC0):
$ hg id
4e27f5c361d2 tip



> I have studied the sources once again, and don't see how a negative
> value can emerged. There is probably something wrong at the very bottom
> of it.

I managed to get a negative total number of threads:


isabelle console -r
Poly/ML> fun f n = if n = 0 then () else ignore (Thread.Thread.fork (fn () => OS.Process.sleep (Time.fromSeconds 10), []));


After calling f with various numerical arguments (it requires a dozen of calls [I used values between 10 and 100, so it should be more that the number of threads required by Isabelle]; it also seems that different values must be used, but I have not found a reproducible way)

val it =
   {gcFullGCs = 0, gcPartialGCs = 0, sizeAllocation = 123731968,
    sizeAllocationFree = 2708352, sizeHeap = 123731968,
    sizeHeapFreeLastFullGC = 0, sizeHeapFreeLastGC = 0, threadsInML = 15,
    threadsTotal = ~1, threadsWaitCondVar = 0, threadsWaitIO = 13,
    threadsWaitMutex = 0, threadsWaitSignal = 1, timeGCSystem = 0.000,
    timeGCUser = 0.000, timeNonGCSystem = 1.243, timeNonGCUser = 0.517,
    userCounters = fromList[0, 0, 0, 0, 0, 0, 0, 0]}:

val it =
   {gcFullGCs = 0, gcPartialGCs = 0, sizeAllocation = 140509184,
    sizeAllocationFree = 1910304, sizeHeap = 140509184,
    sizeHeapFreeLastFullGC = 0, sizeHeapFreeLastGC = 0, threadsInML = 2,
    threadsTotal = ~29, threadsWaitCondVar = 0, threadsWaitIO = 1,
    threadsWaitMutex = 0, threadsWaitSignal = 1, timeGCSystem = 0.000,
    timeGCUser = 0.000, timeNonGCSystem = 1.791, timeNonGCUser = 0.670,
    userCounters = fromList[0, 0, 0, 0, 0, 0, 0, 0]}



Best,
Mathias


> 
>> On 06/15/2018 03:51 PM, Makarius wrote:
>>> 
>>> 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.
> 
> Can you try building Poly/ML from the bundled sources? Thus we could
> rule out odd effects from the rather old build environment (Ubuntu
> 12.04) of the official binaries.
> 
> You need to test the in the same Isabelle/PIDE environment as before.
> Apparently the raw console is not sufficient to see the effect.
> 
> 
> 	Makarius




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