Email Gateway (Apr 02 2026 at 17:50): Email Gateway (Apr 02 2026 at 17:50):From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
I found a bug in Delay.run() (src/Pure/Concurrent/delay.scala, line 29) where a non-interrupt exception is logged but then rethrown. The rethrown exception propagates through TimerTask.run() into java.util.TimerThread.mainLoop(), which does not catch RuntimeException from tasks — the timer thread terminates and the global event_timer singleton dies permanently.
After that, every Delay.invoke() call in the process either throws IllegalStateException ("Timer already cancelled") or silently fails. This breaks all debouncing and throttling in the editor.
Call chain:
Delay.invoke() → Event_Timer.request() → TimerTask fires → Delay.run()
→ catch block logs + rethrows → escapes TimerTask.run() → kills TimerThread
Minimal fix — remove the rethrow in delay.scala line 29 (Isabelle2025/src/Pure/Concurrent/delay.scala:29):
Patch is attached to this email.
The exception is still logged for visibility, but Delay.run() exits normally so TimerThread.mainLoop() continues its loop and the global timer stays alive.
I have a standalone test (DelayBugTest) that reproduces this reliably:
The test passes after applying the fix above.
I am aware that there is a known bug that jEdit slows down after a long time. I am not sure, but I believe it might be somehow connected, that there is some runtime exception, which silently kills the timer and the perceived 'slowdown' is just the fact that some tasks that use timer are not executed, however, this requires further tests.
I am happy to provide the full test code or any additional information. This was found as part of my dissertation work on frontend testing of the Isabelle platform.
Best regards,
Bartosz Glowacki
King's College London
Email Gateway (Apr 07 2026 at 18:25):From: Fabian Huch <huch@in.tum.de>
While this does look suspicious, speaking of a 'bug' doesn't really make
sense here: If a task fails with an unrecoverable error on a background
thread, I would expect that the background thread is in a failure state
too. Looking only at your description, I would actually argue that the
system should instead fail immediately (loudly). But judging the
situation requires looking into the sources and history, to find out
what the intention was.
In any case, this is still missing an actual problem -- does the
Exception actually occur, or does the behavior under the hypothesized
state actually coincide with a known issue? If yes, how to trigger the
problem? I have seen this state manifest a couple of times, but only
after a (very obvious) catastrophic failure somewhere else.
Fabian
On 4/2/26 19:24, Bartosz Glowacki (via cl-isabelle-users Mailing List)
wrote:
Dear Isabelle developers,
I found a bug in Delay.run() (src/Pure/Concurrent/delay.scala, line
29) where a non-interrupt exception is logged but then rethrown. The
rethrown exception propagates through TimerTask.run() into
java.util.TimerThread.mainLoop(), which does not catch
RuntimeException from tasks — the timer thread terminates and the
global event_timer singleton dies permanently.After that, every Delay.invoke() call in the process either throws
IllegalStateException ("Timer already cancelled") or silently fails.
This breaks all debouncing and throttling in the editor.Call chain:
Delay.invoke() → Event_Timer.request() → TimerTask fires → Delay.run()
→ catch block logs + rethrows → escapes TimerTask.run() → kills
TimerThreadMinimal fix — remove the rethrow in delay.scala line 29
(Isabelle2025/src/Pure/Concurrent/delay.scala:29):
Patch is attached to this email.The exception is still logged for visibility, but Delay.run() exits
normally so TimerThread.mainLoop() continues its loop and the global
timer stays alive.I have a standalone test (DelayBugTest) that reproduces this reliably:
1. Create a Delay whose event throws RuntimeException
2. Invoke it and wait for it to fire
3. Create a second Delay and try to invoke it
4. The second invoke throws IllegalStateException — the timer is deadThe test passes after applying the fix above.
I am aware that there is a known bug that jEdit slows down after a
long time. I am not sure, but I believe it might be somehow connected,
that there is some runtime exception, which silently kills the timer
and the perceived 'slowdown' is just the fact that some tasks that use
timer are not executed, however, this requires further tests.I am happy to provide the full test code or any additional
information. This was found as part of my dissertation work on
frontend testing of the Isabelle platform.Best regards,
Bartosz Glowacki
King's College London
Email Gateway (Apr 12 2026 at 19:18):From: Makarius <makarius@sketis.net>
On 02/04/2026 19:24, Bartosz Glowacki (via cl-isabelle-users Mailing List) wrote:
Dear Isabelle developers,
I found a bug in Delay.run() (src/Pure/Concurrent/delay.scala, line 29) where
a non-interrupt exception is logged but then rethrown. The rethrown exception
propagates through TimerTask.run() into java.util.TimerThread.mainLoop(),
which does not catch RuntimeException from tasks — the timer thread terminates
and the global event_timer singleton dies permanently.After that, every Delay.invoke() call in the process either throws
IllegalStateException ("Timer already cancelled") or silently fails. This
breaks all debouncing and throttling in the editor.Call chain:
Delay.invoke() → Event_Timer.request() → TimerTask fires → Delay.run()
→ catch block logs + rethrows → escapes TimerTask.run() → kills TimerThreadMinimal fix — remove the rethrow in delay.scala line 29 (Isabelle2025/src/
Pure/Concurrent/delay.scala:29):
Patch is attached to this email.
Hi Bartosz,
I've seen this mail some weeks ago and ignored it immediately, because of the
use of ill-defined words "bug" and "fix". My usual definitions first: "bug"
usually means "unexpected behaviour", and "fix" usually means "I did not
understand all details, but here is an adhoc patch that might improve the
situation, or not". (Note that your patch was actually lost.)
My first impulse when something looks odd in the Isabelle sources is to browse
our glorious history, to see where the piece of source comes from. Here is an
approximative result from doing this for only 5min (it usually requires 20min
to 2h):
changeset: 64810:05b29c8f0add
user: wenzelm
date: Thu Jan 05 22:57:59 2017 +0100
files: src/Pure/Concurrent/standard_thread.scala
src/Tools/VSCode/src/channel.scala src/Tools/VSCode/src/server.scala
description:
more informative error for spurious crash;
changeset: 56770:e160ae47db94
user: wenzelm
date: Mon Apr 28 14:41:49 2014 +0200
files: src/Pure/Concurrent/simple_thread.scala
src/Pure/GUI/swing_thread.scala src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/monitor_dockable.scala src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
description:
mane delayed events outside of Swing thread -- triggers no longer require
Swing_Thread.later;
I guess that the Swing Thread behaves more robustly in the face of exceptions
than java.util.Timer. At least I've never the Swing dispatcher disappear, like
the timer thread.
That is certainly bad, and Java could be blamed for it, but they document this
fragile behavior (which I've overlooked so far). So it probably requires a
diligent change on our side to "make it more robust", meaning it works better
under more rough side-conditions.
Anyway, apart from such theoretical failures, did you encounter an actual
problem in using Isabelle/jEdit practically?
The exception is still logged for visibility, but Delay.run() exits normally
so TimerThread.mainLoop() continues its loop and the global timer stays alive.I have a standalone test (DelayBugTest) that reproduces this reliably:
1. Create a Delay whose event throws RuntimeException
2. Invoke it and wait for it to fire
3. Create a second Delay and try to invoke it
4. The second invoke throws IllegalStateException — the timer is deadThe test passes after applying the fix above.
I am interested in the materials from this experiment, but please note that
"bugs" vs. "fixes" are alien to the Isabelle development model.
I am aware that there is a known bug that jEdit slows down after a long time.
Do you mean jEdit or Isabelle/jEdit? (This makes a big difference.)
I am happy to provide the full test code or any additional information. This
was found as part of my dissertation work on frontend testing of the Isabelle
platform.
So what is your overall approach? I guess that the Java Swing GUI stuff is
pretty easy to get into bad situations, due to race conditions etc.
Makarius
Email Gateway (Apr 12 2026 at 19:31):From: Makarius <makarius@sketis.net>
On 12/04/2026 21:17, Makarius wrote:
I guess that the Swing Thread behaves more robustly in the face of exceptions
than java.util.Timer. At least I've never the Swing dispatcher disappear, like
the timer thread.That is certainly bad, and Java could be blamed for it, but they document this
fragile behavior (which I've overlooked so far). So it probably requires a
diligent change on our side to "make it more robust", meaning it works better
under more rough side-conditions.
Spending 5min longer on the Java documentation of java.util.Timer, I get the
impression that it is overall very weak. They also point to the later
ScheduledThreadPoolExecutor as an alternative.
I will eventually study the sources of both, and then see what can be really
improved on our side (not "fixed", please).
Makarius
Email Gateway (Apr 13 2026 at 20:20):From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,
Thank you for looking into this and for the historical context from the changesets.
To your question about practical problems: The easiest way to observe the effect is to chmod 000 a HOL dependency (e.g. HOL/List.thy) before launching Isabelle/jEdit. The editor starts, but all theory text renders black with no semantic highlighting, and the state does not recover even after restoring the file. In fact, there is no retry for the timer, so later usage of the software is just pointless. This is admittedly an unusual situation, but files on network mounts or removable media could produce similar I/O exceptions transiently.
Regarding jEdit vs Isabelle/jEdit slowdown: I meant Isabelle/jEdit specifically. I speculated that some instances of perceived slowdown (known issue in Isabelle, after longer usage time) might involve the timer thread dying after a transient exception, causing delay-scheduled UI updates to stop. This is just a hypothesis - I have not confirmed a connection.
Apologies for the lost patch — I am re-attaching it to this email. I understand it may not be the right approach; however, I believe that rethrowing the exception can only kill the timer with no additional benefits. I look forward to seeing what you arrive at after studying the Timer and ScheduledThreadPoolExecutor sources, I believe that this change might be also required.
My overall dissertation approach is systematic testing of the Isabelle/PIDE frontend infrastructure — the Scala layer between the prover and the GUI. For Whitebox testing, I use generative AI to initially scan the Isabelle/scala source code to look for vulnerabilities, then evaluate the results and write the tests case. I attach the test case, patch and markdown explaining the testing technique.
Best regards,
Bartosz
From: Makarius <makarius@sketis.net>
Sent: Sunday, April 12, 2026 9:28 PM
To: Bartosz Glowacki <bartosz.gowacki@kcl.ac.uk>; cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Cc: Mohammad Ahmad Abdulaziz Ali Mansour <mohammad.abdulaziz@kcl.ac.uk>; Karine Even-Mendoza <karine.even_mendoza@kcl.ac.uk>
Subject: Re: [isabelle] [BUG] Delay.run() rethrows exception, killing global Event_Timer thread
[Some people who received this message don't often get email from makarius@sketis.net. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]
On 12/04/2026 21:17, Makarius wrote:
I guess that the Swing Thread behaves more robustly in the face of exceptions
than java.util.Timer. At least I've never the Swing dispatcher disappear, like
the timer thread.That is certainly bad, and Java could be blamed for it, but they document this
fragile behavior (which I've overlooked so far). So it probably requires a
diligent change on our side to "make it more robust", meaning it works better
under more rough side-conditions.
Spending 5min longer on the Java documentation of java.util.Timer, I get the
impression that it is overall very weak. They also point to the later
ScheduledThreadPoolExecutor as an alternative.
I will eventually study the sources of both, and then see what can be really
improved on our side (not "fixed", please).
Makarius
0001-Delay-bug-fix.patch
DelayBugTest.md
DelayBugTest.scala
Last updated: May 02 2026 at 13:17 UTC