Time limiting apply and by commands

[Makarius]

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