RFC: 'Measure time to cancellation' option

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 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

The proposal does not name files, tests, or an entry point. Start by tracing cancellation-token handling between the language processor and elaboration tasks, then determine where the debugging option belongs. Done means the option records cancellation and next-read timestamps and reports deltas over 500ms to stderr.