Re: [isabelle] 2014-RC1 issues
On Thu, 7 Aug 2014, Lars Noschinski wrote:
I encountered such a case yesterday (with 2014-RC2) with a tactic with
resulted in a non-productive result sequence, i.e. the equivalent of
fun inf_seq () = Seq.cons 0 (inf_seq ())
val nonprod_seq = Seq.filter (K false) (inf_seq ())
After some looking around, I found that I get a little hint in the Raw
Output panel -- if the panel is open while the failing code is executed.
The above example provokes a *soft* breakdown of ML user code. The
Poly/ML run-time systems maps that to an interrupt, which is not printed
in PIDE. There are other visual clues that something is wrong with the
command transaction. It is then left as an exercise to find section "4.2
Low-level output" in the Isabelle/jEdit manual, and connect it
semantically to such sitations.
I wonder whether the raw output panel could accumulate, say, the last 8k
worth of messages even if it is closed?
There is always the question how much technology is built around low-level
errors. They occurr so rarely that an incident can become a big desaster
if the error handling infrastructure itself gets overloaded. This could
lead to spectacular events of "total failure of existence", which we've
had occasionally had in the past. (That phrase is from Starship Titanic
due to Douglas Adams and Terry Jones, where it is called S.M.E.F.
"Spontaneous Massive Existence Failure".)
Nonetheless, I have made some changes for the Isabelle2014 code base some
months ago concerning Syslog output -- to have a buffer and a limit on it,
with some hope that bombing the front-end is avoided. So there might be a
chance to print certain low-level messages on Syslog, instead of raw
output, but such experiments are not for this release.
Also, a "clear" button would be nice (although closing/reopening works).
The panel is a plain Swing text area, so you can just select all text and
Interestingly, asking for an exception trace (via
[[ML_exception_trace]]) for this code sends polyml into a another
desperate quest for memory: It has been running on my machine a few
minutes with 4086M VIRT and 3956M RES -- so basically exhausting its
full address space -- before giving up:
In these cases I could be useful to get at least at a partial trace
(which would probably already indicate which functions went into a
This looks like a *hard* breakdown of the ML runtime system. David
Matthews is the only one who can say more about it.
Note that driving the system against a concrete wall routinely causes big
damage. In the past couple of years, David Matthews has managed to move
concrete walls many times, but it is a never ending process. (The JVM is
even more fragile under low-memory situations.)
After 32bit address space is left behind -- presumably soon -- such VM
problems will go away, and the good old disk-thrashing on swap space will
This archive was generated by a fusion of
Pipermail (Mailman edition) and