3a6c5cf4f1
This PR improves the canonicalizer used in the `grind` tactic and the diagnostics it produces. It also adds a new configuration option, `canonHeartbeats`, to address (some of) the issues. Here is an example illustrating the new diagnostics, where we intentionally create a problem by using a very small number of heartbeats. <img width="1173" alt="image" src="https://github.com/user-attachments/assets/484005c8-dcaa-4164-8fbf-617864ed7350" /> |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||