Re: [isabelle] ML goes "incommunicado" for minutes at a time during sledgehammering
On Thu, 21 Apr 2016, Eugene W. Stark wrote:
The problem is that, during sledgehammering using "try" it seems that ML
will go "incommunicado" for minutes at a time, and it is hard to figure
On the snapshot from the "Heap" window, you can see spikes in memory
usage, leading to what appears to be a major GC. Upon completion of the
major GC, the "freeze" sets in, and no data is sent to the monitor for
several minutes. When the data resumes, the heapsize is much lower, but
quickly spikes up to the max and the cycle repeats. Because there is no
data during the freeze period, it is difficult to tell what is going on,
but I have to wonder what it is doing during those 3+ minutes when there
is only a short spike of computing activity that takes place before it
Could anyone comment on whether this behavior is considered "normal"?
It sounds indeed like a normal consequence of a situation where the ML
heap is under high pressure: tons of data produced and the GC + heap
compaction phases trying to reclaim memory.
When the Poly/ML runtime system performs such GC-related operations, all
ML threads are stopped. The Monitor data is produced by such a regular ML
thread, so nothing will be reported during that time.
I am suspicious of some kind of thread signalling/synchronization issue,
but not knowing anything about the actual implementation, can only
From the description of the problem, it does not really look like that.
Although there is always a possibility for something really strange going
In conclusion, my guess from a distance is that "sledgehammer" or "try"
produce more data than expected, potentially due to unusually big
theories. You could also try to reset the machine-learning information in
Since you are using 64bit Poly/ML with substantial amounts of heap space,
the question is what makes the theories so big that this is required. Even
the biggest applications on AFP still fit into the small memory model of
32bit with 3.5 GB heap. There is a penalty of approx. factor 2 in memory
requirements, when switching from 32bit to 64bit.
This archive was generated by a fusion of
Pipermail (Mailman edition) and