Time limiting apply and by commands

[Lawrence Paulson]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20260413/b64aa7fa/attachment.htm>