Re: [isabelle] Difficult to reproduce bug hanging Isabelle in jEdit session
Am 22.04.2013 16:27, schrieb Lars Noschinski:
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
Unfortunately, hitting "Cancel" doesn't work here at Karlsruhe. However,
in the student's computer pool hitting "Check" while a large theory file
is being processed, seems to reliabely result in the same freeze of the
As there is no error message in the Output panel or at the command line,
what are our options to investigate the problem? Is there an option to
log the communication between jEdit and the isabelle process? Would this
information help to find the cause?
Karlsruher Institut für Technologie (KIT) IPD Snelting
Am Fasanengarten 5, Gebäude 50.34, Raum 025
Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: denis.lohner at kit.edu
KIT - Universität des Landes Baden-Württemberg und
nationales Forschungszentrum in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and