[isabelle-dev] Fwd: status (AFP)

[Makarius]

On Fri, 14 Oct 2011, Gerwin Klein wrote:

> Is anyone else observing intermittent problems like this?
>
> Building Jinja ...
> poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion `val.IsDataPtr()' failed.
> /home/kleing/volatile/isadist/Isabelle_13-Oct-2011/lib/scripts/run-polyml: line 77: 20095 Aborted                 "$POLY" -q $ML_OPTIONS
> Jinja FAILED

Yes, occasionally.  Such hard crashes were more frequent in the past, and 
we are running much more and bigger jobs now.

It often helps to modify ML_OPTIONS a bit, such as -H for the initial heap 
size.


> We're investigating if possibly something is wrong with the test 
> server's memory, but it seems unlikely (our L4.verified sessions are 
> larger and stable).

Is this the machine that is producing these test results?

   http://isabelle.in.tum.de/devel/stats/afp.html

There used to be much less fluctuation with AFP on the hardware at TUM, 
IIRC. Since the charts are derived from the "Finished" status it might 
also involve the file-system.  Instead the inner "Timing" could be used to 
get closer to the raw CPU characteristics.  Mira should also contain that 
information.


 	Makarius