Stream: Mirror: Isabelle Development Mailing List

Topic: Time limiting apply and by commands

Email Gateway (Apr 13 2026 at 10:13):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

A year or two ago, I proposed an option to let users impose a time limit on the execution of proof methods, to make it easier to find performance regressions after making a change to a large development. It would also make it easier to find slow steps in any large development. Some people opposed to this on the grounds that it was “not portable”, which misses the point: it is not intended to be left in a completed development In the first place. All it can do is make a proof fail.

It would be a useful feature to have, and extremely easy to implement, so I hope this time there will be no objections.

Larry

Email Gateway (May 04 2026 at 19:12):

From: Makarius <makarius@sketis.net>

On 13/04/2026 12:13, Lawrence Paulson via isabelle-dev wrote:

A year or two ago, I proposed an option to let users impose a time limit on
the execution of proof methods, to make it easier to find performance
regressions after making a change to a large development. It would also make
it easier to find slow steps in any large development. Some people opposed to
this on the grounds that it was “not portable”, which misses the point: it is
not intended to be left in a completed development In the first place. All it
can do is make a proof fail.
It would be a useful feature to have, and extremely easy to implement, so I
hope this time there will be no objections.
I am still busy elsewhere, approx. for the next 2 weeks, due to project
deadlines. This means, I still did not find time to retrieve the relevant mail
threads from 1-2 years ago. Without that it does not make sense to do
"extremely easy" things. (Where is the proof for that claim?)

We do have fundamental problems with ML timeouts, due to complexities of
multithreading and garbage collection. I won't enter that lair right now ---
maybe a bit later, when revisiting many PIDE document processing concepts. And
that might actually expose better approaches and proper solutions to old problems.

I am not following the recent trend to apply adhoc changes blindly, without
understanding of the overall context --- of the sources and discussions about
approaches to the problem at hand.

Makarius

Last updated: Jun 04 2026 at 18:19 UTC