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 bisec
On Fri, 14 Oct 2011, Andreas Schropp wrote:
Isabelle is generating a *lot* of copies of types& terms, particularly
via Term.map_atyps. Since shareCommonData eliminates them, many are
duplicates. It's possible that further use of the "same" variants from
Term_Subst might help. It's also possibl
On Fri, 14 Oct 2011, David Matthews wrote:
I can only guess that allocation of mutable stuff costs extra.
Allocation of a mutable, at least a fixed-size mutable such as ref,
doesn't cost any more than allocating an immutable. However, if a
mutable survives a GC it has an impact on subsequen
On 14/10/2011 10:56, Makarius wrote:
On Fri, 14 Oct 2011, Andreas Schropp wrote:
val dummy_task = Task(NONE, ~1)
Values are not shared?! What the hell?
Datatypes and tuples that contain only constant data are created once
during compilation.
This looks like an older version. Thomas was re
On 14/10/2011 09:13, Andreas Schropp wrote:
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
Good day all. Just wanted to let the Isabelle developers know about
the latest feature David Matthews has added to PolyML, and to let you
all know how useful it is.
The feature allows profiling of objects a
On Fri, 14 Oct 2011, Andreas Schropp wrote:
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
There are surprisingly many dummy tasks.
[...]
918632 Task_Queue.dummy_task(1)
Such numbers always need to be put in relation. The original list was
like that:
918632 Task_Queue.dummy_task(1
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
There are surprisingly many dummy tasks.
[...]
918632 Task_Queue.dummy_task(1)
val dummy_task = Task(NONE, ~1)
Values are not shared?! What the hell?
___
isabelle-dev mailing list
isabelle-...@in
On 10/13/2011 01:24 PM, Thomas Sewell wrote:
Good day all. Just wanted to let the Isabelle developers know about the latest
feature David Matthews has added to PolyML, and to let you all know how useful
it is.
The feature allows profiling of objects after garbage collection. When code is
comp
Good day all. Just wanted to let the Isabelle developers know about the latest
feature David Matthews has added to PolyML, and to let you all know how useful
it is.
The feature allows profiling of objects after garbage collection. When code is
compiled with PolyML.compiler.allocationProfiling s
