Email Gateway (Apr 13 2026 at 10:13): 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
Last updated: Apr 29 2026 at 06:25 UTC