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



On 15/06/18 22:11, Eugene W. Stark wrote:
> 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.

I cannot follow that conclusion.

The statistics are produced by the Poly/ML runtime system, and
Isabelle/ML + Isabelle/Scala merely pass-on the values to the GUI panel.

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.


> 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


Attachment: signature.asc
Description: OpenPGP digital signature



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