Re: [isabelle] Difficult to reproduce bug hanging Isabelle in jEdit session



On 22.04.2013 15:29, Joachim Breitner wrote:
here at Karlsruhe we are offering a practical Course on Isabelle which
began last week and we were badly surprised that Isabelle/jEdit 2013 had
severe issues on the machines in the student’s pool room: A short while
into editing the highlighting (errors and the light blue) and the output
window are no longer updated.

We could reproduce it most easily by writing, say,
         theory Scratch imports Main begin lemma "foobar"
and then changing "lemma" to "le mma" and back in very rapid succession.

I occasionally had similar problems but did not manage to produce a reproducible example yet. However, I managed to get the system back to working by hitting the "Cancel' button in the "Theories" window a few times.

If I remember correctly, the problem occurred often when editing a proof which was followed by a "lemma (in LOC)" where LOC was a reasonably big locale from HOL-Algebra.

This occurred both with Isabelle 2013 and a recent Isabelle development snapshot. Debian with a 64-bit Isabelle, 6GB RAM, Core 2 Duo and a Gnome 3 desktop.

  -- Lars




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