Email Gateway (Nov 19 2020 at 00:49): Email Gateway (Nov 19 2020 at 00:49):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I have been using a relatively recent snapshot version of Isabelle (Isabelle_04-Nov-2020). This version
does a rather better job of showing what is going on if the Monitor panel is raised. That is good.
My question is: In certain situations, if I use "try" and let it crunch for awhile, I can arrive at
a situation where there are perhaps 180K future tasks showing in the Monitor window. I can sometimes
then delete the "try" from the input buffer, but the future tasks remain and may take many minutes
to clear.
My question is: once I have deleted the "try" from the input buffer, why are the existing future tasks
still relevant? Why do they not get canceled somehow, so that they don't spam the interactive
session for an unknown period of time?
Please bear in mind that I don't have any idea about the technical aspects of the implementation.
It just strikes me that there is little point in having to wait many minutes to clear a queue of
future tasks that were started by a buffer input that has since been deleted.
Email Gateway (Jan 02 2021 at 10:36):From: Makarius <makarius@sketis.net>
Do you still see this in current Isabelle2021-RC1
https://isabelle.in.tum.de/website-Isabelle2021-RC1 ?
If yes, can you provide a reproducible example for such a situation?
Makarius
Last updated: Jul 15 2022 at 23:21 UTC