Email Gateway (Aug 24 2026 at 11:18): Email Gateway (Aug 24 2026 at 11:18):From: Steven Obua <steven.obua@gmail.com>
Given that the new Isabelle release is coming up, I am wondering if there
is a "timed" method or similar available by default now (according to NEWS,
this doesn't seem to be the case). If not, maybe it could be added? I am
adding it for every new Isabelle formalisation project currently. I am
attaching what I am using now with the January 2026 release.
Cheers,
Steven
Email Gateway (Aug 24 2026 at 11:57):From: Makarius <makarius@sketis.net>
On 24/08/2026 13:18, Steven Obua wrote:
Given that the new Isabelle release is coming up, I am wondering if there is a
"timed" method or similar available by default now (according to NEWS, this
doesn't seem to be the case). If not, maybe it could be added? I am adding it
for every new Isabelle formalisation project currently. I am attaching what I
am using now with the January 2026 release.
Shortly before a release is a very bad time to add "features" on the spot: it
usually means extra days/weeks to get everything right, but that time is
required for other things that are already in the pipeline for this release
(often these get postponed to a later release).
Moreover, the canonical question on this mailing list is "What is your
application? What is really required".
Sprinkling ML timeouts into the system is generally fragile: results become
erratic for various reasons, including technical side-conditions of the
Isabelle/ML runtime system. So we do need to know what the purpose really is
--- it will affect how to implement the idea properly, if this is possible in
the first place.
Makarius
Email Gateway (Aug 24 2026 at 12:43):From: Steven Obua <steven.obua@gmail.com>
Hi Makarius :smiley:
I think what the method does is self explanatory. Similarly to "sorry", it
would not be part of a polished finished theory, it is just a means to
detect a proof method that does not terminate when you run Isabelle from
the command line. Even better would be a command line switch that can
timeout any proof method that takes too much time; currently there is only
a timeout switch for the entire session, which is not precise enough,
because how long I am willing to wait for the whole session to succeed
(minutes) is substantially longer than how long I am willing to wait for
most proof methods to succeed (seconds).
It is no issue for me to just add this method to each of my developments,
so treat this as a JFYI, maybe for the release after the upcoming one in
case this makes sense to you. The advantage of just adding this method,
compared to a command-line switch, is that it is immediately portable.
Adding it to Main would also mean that the AFP could scan theories
automatically for it, and reject submissions that contain it.
Cheers,
Steven
On Mon, Aug 24, 2026 at 12:57 PM Makarius <makarius@sketis.net> wrote:
On 24/08/2026 13:18, Steven Obua wrote:
Given that the new Isabelle release is coming up, I am wondering if
there is a
"timed" method or similar available by default now (according to NEWS,
this
doesn't seem to be the case). If not, maybe it could be added? I am
adding it
for every new Isabelle formalisation project currently. I am attaching
what I
am using now with the January 2026 release.
Shortly before a release is a very bad time to add "features" on the spot:
it
usually means extra days/weeks to get everything right, but that time is
required for other things that are already in the pipeline for this
release
(often these get postponed to a later release).Moreover, the canonical question on this mailing list is "What is your
application? What is really required".Sprinkling ML timeouts into the system is generally fragile: results
become
erratic for various reasons, including technical side-conditions of the
Isabelle/ML runtime system. So we do need to know what the purpose really
is
--- it will affect how to implement the idea properly, if this is possible
in
the first place.Makarius
Email Gateway (Aug 24 2026 at 13:51):From: Makarius <makarius@sketis.net>
Larry, I think that Steven thinks more of batch builds, but you had told me
about PIDE interaction. I have rejected the "patch" some months ago, because
there where unfounded claims of everything being "trivial", "easy to fix" etc.
Such changes need to be thought out well, based on the past 20 years of
experience (and failures) including our timeout facilities. For example, to
detect long-running proof methods, or commands, or actual proofs: Why not show
that directly in the Prover IDE, instead of causing an unpredictable failure
that cannot be recovered?
Anyway, I am in the process to wrap up several open ends for the release, and
I will not revisit timeouts right now --- apart from proper process timeouts
for the "verit" executable, which is a quite different thing.
I also have some half-finished improvements of PIDE command status in the
pipeline, but can't say how much of it will be flushed. Shortly after the
release, there will be many more changes of session builds and PIDE
interaction, to unify these two historically separate approaches more and more.
Makarius
On 24/08/2026 15:19, Lawrence Paulson wrote:
Just for my two cents, the apply_timeout patch which I sent you many months
ago and which I have been using daily ever since would meet the same purpose,
i.e. to track down looping proof methods. This is a present one of the most
tedious aspects of managing change in a large development. And so easy to fix.Larry
On 24 Aug 2026 at 13:43 +0100, Steven Obua <steven.obua@gmail.com>, wrote:Hi Makarius :smiley:
I think what the method does is self explanatory. Similarly to "sorry", it
would not be part of a polished finished theory, it is just a means to
detect a proof method that does not terminate when you run Isabelle from the
command line. Even better would be a command line switch that can timeout
any proof method that takes too much time; currently there is only a timeout
switch for the entire session, which is not precise enough, because how long
I am willing to wait for the whole session to succeed (minutes) is
substantially longer than how long I am willing to wait for most proof
methods to succeed (seconds).It is no issue for me to just add this method to each of my developments, so
treat this as a JFYI, maybe for the release after the upcoming one in case
this makes sense to you. The advantage of just adding this method, compared
to a command-line switch, is that it is immediately portable. Adding it to
Main would also mean that the AFP could scan theories automatically for it,
and reject submissions that contain it.Cheers,
StevenOn Mon, Aug 24, 2026 at 12:57 PM Makarius <makarius@sketis.net
<mailto:makarius@sketis.net>> wrote:On 24/08/2026 13:18, Steven Obua wrote:
> Given that the new Isabelle release is coming up, I am wondering if
there is a
> "timed" method or similar available by default now (according to NEWS,
this
> doesn't seem to be the case). If not, maybe it could be added? I am
adding it
> for every new Isabelle formalisation project currently. I am attaching
what I
> am using now with the January 2026 release.
Shortly before a release is a very bad time to add "features" on the
spot: it
usually means extra days/weeks to get everything right, but that time is
required for other things that are already in the pipeline for this release
(often these get postponed to a later release).Moreover, the canonical question on this mailing list is "What is your
application? What is really required".Sprinkling ML timeouts into the system is generally fragile: results become
erratic for various reasons, including technical side-conditions of the
Isabelle/ML runtime system. So we do need to know what the purpose really is
--- it will affect how to implement the idea properly, if this is
possible in
the first place.Makarius
Email Gateway (Aug 24 2026 at 14:00):From: Makarius <makarius@sketis.net>
On 24/08/2026 14:42, Steven Obua wrote:
I think what the method does is self explanatory. Similarly to "sorry", it
would not be part of a polished finished theory, it is just a means to detect
a proof method that does not terminate when you run Isabelle from the command
line. Even better would be a command line switch that can timeout any proof
method that takes too much time; currently there is only a timeout switch for
the entire session, which is not precise enough, because how long I am willing
to wait for the whole session to succeed (minutes) is substantially longer
than how long I am willing to wait for most proof methods to succeed (seconds).
Instead of provoking a timed failure (timeout), you could try with a plain
display of long-running command. See also Isabelle2025-1/NEWS:
* System *
I've made that specifically for some super-high-end users, to get better
feedback on their continuous tests.
Makarius
Email Gateway (Aug 24 2026 at 20:56):From: Makarius <makarius@sketis.net>
Steven, if you want to continue the public part of this mailing list thread,
you are welcome --- I will follow.
(I will not continue any forked-off private threads. If anybody wants to talk
to me privately, it needs to start out as a different thread --- not an abuse
of a public thread.)
Makarius
Email Gateway (Aug 24 2026 at 23:41):From: Steven Obua <steven.obua@gmail.com>
I agree with Larry that having a timeout method that works on the level of
proof methods is essential. The "timed" method I suggested works well for
me, it is a simple way of letting an agent such as Codex or Claude try out
various proof methods quickly, and it works locally, without infecting
other theories in the base library that might actually need longer proof
method timeouts. The scenario here is: You have an Isabelle theory, the
agent modifies the theory, and runs the theory from the command line. This
works very well with Isabelle, through its existing command line interface,
the only addition I needed were some simple shell scripts invoking
Isabelle's command line, and this "timed" method to make proof experiments
quick. I don't need a REPL, I just need a way to run Isabelle from the
command line with local timeouts.
The more advanced way of letting an agent interact directly with the
interactive document model is very tempting, I was also designing Practal
with this idea in mind (see Practal Zero <https://zero.practal.com> for its
interactive document interface). But for now all that I am providing also
for Practal is the command line interface: agents are very good at creating
and modifying theories as a whole, so a simple way to invoke the prover
from the command line seems more than good enough for the short and medium
term.
I must admit, I am blown away by how well Isabelle works together with AI
out of the box, just via invoking Isabelle from the command line.
Formalisation work that I intended for several years now for abstraction
logic I was able to complete within just 2 days in Isabelle/HOL, yielding
25K lines: the soundness and completeness of abstraction logic. This was
done by just telling the AI to formalise what is in my book, and correcting
some of the definitions it messed up. And beyond that, important additions
to the logic such as additional proof rules, proving soundness and
completeness with respect to them, and support for plurals; all designed,
formalised, and proven correct within a matter of weeks.
Interactive theorem proving is really the killer app for AI, which is
funny, because outside of ITP, most people are blissfully ignorant of what
that even means, including all the big AI players, and inside of ITP, many
seem reluctant rather than excited. I mean, *formalising is now faster than
thinking* in many situations. They spent hundreds of billions of dollars to
make ITP really really REALLY good :rolling_on_the_floor_laughing:. What a time to live in.
Well. Slight detour from "timed" :laughing:.
On Mon, Aug 24, 2026 at 9:56 PM Makarius <makarius@sketis.net> wrote:
Steven, if you want to continue the public part of this mailing list
thread,
you are welcome --- I will follow.(I will not continue any forked-off private threads. If anybody wants to
talk
to me privately, it needs to start out as a different thread --- not an
abuse
of a public thread.)Makarius
Email Gateway (Aug 27 2026 at 15:46):From: Andras Salamon <cl-isabelle-users@lists.cam.ac.uk>
As an alternative to Larry's timeout patch or changes to Isabelle internals, for those using Python
pip install isabelle-watchdog
installs an isabelle-build wrapper that controls timeout behaviour of Isabelle, summarises the verbose build output in a way that seems useful for LLMs, and also optionally keeps trajectories of proof attempts in between verified builds.
This kind of third-party timeout handling should become less important over time as Isabelle support for LLM-driven workflows improves.
I developed this tool for our work on large LLM-generated proofs for low-level computational complexity results and I split it out as a standalone tool for others to use. Repo: https://github.com/ott2/isabelle-watchdog
Proof trajectories are rather interesting, but if they are not recorded they are lost like tears in rain. I wish I had started recording them earlier.
András Salamon
--
The University of St Andrews is a charity registered in Scotland, No.SC013532.
Last updated: Sep 02 2026 at 16:10 UTC