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
Email Gateway (Jul 20 2026 at 19:25):From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] [BUG] Delay.run() rethrows exception, killing global Event_Timer thread
Dear Isabelle developers,
I am writing to follow up on the discussion in this thread regarding the re-throw of exceptions in Delay.scala and its interaction with the timer.
I noticed that commit 8575712445d4 (https://isabelle.in.tum.de/repos/isabelle/rev/8575712445d4), made on May 18 after my original email, includes substantial changes to Delay.scala.
From reviewing the changeset, I can see exactly how the timer crash issue has been resolved. By introducing the Delay_Ops class and the app(event) wrapper, the execution of delayed events is now decoupled from the central Event_Timer thread and delegated to specific execution environments (such as GUI_Thread.later). This structural shift, combined with the new logging framework, ensures that if an event throws an exception, it is now safely caught and explicitly logged within its respective execution context, completely preventing the error from bubbling up and terminating the core timer.
Could you confirm whether this rework addresses the observation I pointed out in my previous email?
I am asking as I am writing a paper describing the project.
Thank you.
Kindest regards,
Bartosz
From: Bartosz Glowacki <bartosz.gowacki@kcl.ac.uk>
Sent: Friday, July 3, 2026 1:02 PM
To: Mohammad Ahmad Abdulaziz Ali Mansour <mohammad.abdulaziz@kcl.ac.uk>; Karine Even-Mendoza <karine.even_mendoza@kcl.ac.uk>
Subject: Fw: [isabelle] [BUG] Delay.run() rethrows exception, killing global Event_Timer thread
From: Makarius <makarius@sketis.net>
Sent: Friday, 17 April 2026 11:26:24
To: Bartosz Glowacki <bartosz.gowacki@kcl.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
On 13/04/2026 21:45, Bartosz Glowacki wrote:
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.
The patch is of the "fixed bug" kind, without any explanations whatsoever. The
actual change is also bad, because it swallows an exception without further
reporting. It requires more work (and actual understanding of the overall
situation) to really improve the status-quo, without silently degrading its
quality.
"AI" cannot do anything of that.
To continue this, please refrain from using misleading terms like "bug",
"fix", "issue", and also refrain from posting adhoc patches --- these are a
real danger to continued system integrity.
Makarius
Email Gateway (Jul 20 2026 at 22:03):From: Makarius <makarius@sketis.net>
Subject: [isabelle] [BUG] Delay.run() rethrows exception, killing global Event_Timer thread
On 20/07/2026 20:17, Bartosz Glowacki (via cl-isabelle-users Mailing List) wrote:
Dear Isabelle developers,
I am writing to follow up on the discussion in this thread regarding the re-
throw of exceptions in /Delay.scala/ and its interaction with the timer.
I noticed that commit 8575712445d4 (https://isabelle.in.tum.de/repos/isabelle/
rev/8575712445d4 <https://isabelle.in.tum.de/repos/isabelle/
rev/8575712445d4>), made on May 18 after my original email, includes
substantial changes to |Delay.scala|.
From reviewing the changeset, I can see exactly how the timer crash issue has
been resolved. By introducing the /Delay_Ops/ class and the /
app(event)/ wrapper, the execution of delayed events is now decoupled from the
central /Event_Timer/ thread and delegated to specific execution environments
(such as /GUI_Thread.later/). This structural shift, combined with the new
logging framework, ensures that if an event throws an exception, it is now
safely caught and explicitly logged within its respective execution context,
completely preventing the error from bubbling up and terminating the core timer.
Could you confirm whether this rework addresses the observation I pointed out
in my previous email?
I am asking as I am writing a paper describing the project.
Hi Bartosz,
again, as far as I can tell on my side, it was another random re-reading and
re-writing of sources.
I did repeat your experiments to see an explicit crash of the Java timer, with
explicit exception showing up in the user program. Explicit errors are good,
and not really a problem. Hidden errors are a problem.
Since there were hints about the timer crashing silently, I inspected its Java
sources, and found them overall quite OK, for their rather old age. It was
also clear, how to fit this traditional Java module into our Isabelle/Scala
mindset today, so that we manage the exceptions instead of Java.
The main work on the Isabelle/Scala side was to sort out many details of the
Logger module (not "logging framework"), which was originally introduced for
Isabelle/VSCode. Now it fits better to Isabelle/jEdit with its regular console
log output. This required many changes here and there --- as usual in Isabelle
development. In the end, there is hopefully a more robust and better-defined
situation, with clear documentation as source program text.
There is not a single changeset which "fixes" anything particular. In fact, we
don't have "fixes" at all, just continued "tuning" and "clarification" of our
sources to make them monotnically better.
Here is another recent change, that improves a related situation in Isabelle/ML:
changeset: 84951:a5869d792251
user: wenzelm
date: Wed Jul 15 11:35:13 2026 +0200
files: src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/isabelle_thread.ML src/Pure/General/exn.ML
description:
more informative failure (see also 88acf2619921, 019cec83b49f);
Before the exception was silently ignored: which is bad. Afterwards it is
"more informative".
In conclusion: again some polishing and linting out our sources here and there.
Makarius
Last updated: Jul 22 2026 at 14:00 UTC