[isabelle-dev] Using PolyML's memory consumption profiling on Isabelle

[Makarius]

On Thu, 13 Oct 2011, Thomas Sewell wrote:

> 3) After adding a 400-element record to a test theory built on the HOL image.

Your original motivation was to isolate mysterious performance issues in 
the record package.  Did you now manage to pin that down in the 
measurement?

In that case a bisection could reveal the point in history where the 
change happened, so one might learn from it another detail about the ML 
runtime-system.


 	Makarius