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

[Joachim Breitner]

Hi,

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.

The machines in question are Fedora 18 systems, 64 bit, 4GB RAM, no swap
and the file systems on NFS. We also reproduced it on machines with more
RAM and on machien with the 32 bit libraries installed in addition. We
cannot reproduce it on our own workstations, though.

It seems it is happening more easily on slower machine. Maybe some race
condition?

We are at a loss here – any idea how to get it working more reliable?

Thanks,
Joachim


--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

[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 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

[Denis Lohner]

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
> times.

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
Output panel.

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?

Thanks,
Denis


--
Karlsruher Institut für Technologie (KIT) IPD Snelting

Denis Lohner
wissenschaftlicher Mitarbeiter

Am Fasanengarten 5, Gebäude 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: denis....@kit.edu

http://pp.info.uni-karlsruhe.de

KIT - Universität des Landes Baden-Württemberg und
nationales Forschungszentrum in der Helmholtz-Gemeinschaft

[Makarius]

On Tue, 23 Apr 2013, Denis Lohner wrote:

> 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
>> times.
>
> 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 Output
> panel.
>
> 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?

The "Protocol" panel in Isabelle/jEdit gives a full transcript of the two
processes communicating, although that slows down things considerably, and
usually makes such non-deterministic problems disappear.


There have been reports about several such real-time reactivity problems
in the past few months, but so far very few concrete hints of the actual
reasons. Problems with Fedora 18 in particular had been reported before,
but this does not say much -- recent Linux distributions all tend towards
instabilities that were not there 1 or 2 years ago.

In the next round of refinements of Isabelle/Scala and Isabelle/jEdit, I
will be more defensive in the use of certain Java 7 GUI / window popup
features, and also in the use of Scala actors. There are reasons to
believe that these basic building blocks of the interactive framework are
not 100% reliable.

Apart from that, any more concrete observation where things don't work in
Isabelle2013 will be treated with the usual scrutiny.


Makarius