RFC: 'Measure time to cancellation' option

[mhuisi]

Proposal

We have been hearing reports (e.g. from @b-mehta) that expensive tactics often keep running in the background despite the fact that the document has already changed since the invocation of the tactic. Examples mentioned so far include exact?, aesop? and norm_num. This hints at the fact that tactics don't check for cancellation often enough after the language processor has signaled the elaboration task to stop.

Since this issue is difficult to spot in practice, it would be great if we had better diagnostic tools to help detect this. For a start, I propose that we add a debugging option that takes the current timestamp when the cancellation token is set and when it is read the next time and simply prints a debug message to stderr when the delta exceeds 500ms. We can then use this flag to evaluate our tactics for cancellation issues or prompt users to use it when they experience Lean gradually getting bogged down in old elaboration runs.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[b-mehta]

cc @eric-wieser who I think also came across this

[eric-wieser]

https://github.com/leanprover-community/mathlib4/pull/16666 includes a diagnostic tool to detect this, but one built into core would definitely be better!