Hello,
We are looking for feedback regarding a new timeout feature based on allocation limits: PR Experiment: command modifier and tactic for allocation limits by SkySkimmer · Pull Request #17266 · coq/coq · GitHub. Similar to deterministic timouts in Lean, allocation limits use a more portable and more reliable measure of how long the tactic runs: number of allocations done by the computation rather than time elapsed. We are looking for feedback from people who use timeouts, or who could make use of deterministic timeouts, in terms of ergonomy of the feature and possible desired improvements.
It is also easy for us to implement memory limits in a similar way: aborting a computation when it takes too much memory. Therefore we are also looking for feedback regarding such a possible feature, e.g. best way this could be presented to the user.