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

ML <
 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 deleted it.


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 loop).

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 come back.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.