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

Makarius makarius at sketis.net
Fri Oct 14 14:50:25 CEST 2011

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 

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 


More information about the isabelle-dev mailing list