RFC: global diagnostics

Proposal

Meta.Diagnostics is a useful tool for assessing problems local to a single declaration, but there are currently no analogous tools for assessing global impact.

We propose creating an environmental extension (or extensions) which tracks the applications and successes of simp theorems and typeclass instances. This could be expanded to include other aspects that are currently tracked in Diagnostics like unfolding of semireducible terms. Eventually heartbeat tracking would be very nice.

Why? Often, the overall of impact of an issue can be quite substantial with each individual impact being difficult to notice.

For example, a simple minded version of this found an expansive list of simp theorems that were often applied across mathlib but which never unify.

Knowing during the review process or shortly after whether a new simp theorem or instance is likely to cause expensive detours would help to improve design.

The simplest start would be to just write the data from Diagnostics to the environment. Hiding this behind a flag, like with diagnostics itself, would avoid a general performance penalty. These need to only run periodically similar to debug flags for common build processes.

Most everything is available in diagnostics for simp theorems already. Tracking which instances often side-track typeclass synthesis would need some new logic and possibly new state. But this need not be part of the initial release.

• User Experience: How does this feature improve the user experience? This provides the user with a new tool to understand their code and help adapt it to the existing infrastructure. Hiding it behind an option flag avoids the need to a user to interact with it without explicit effort.

• Beneficiaries: Which Lean users and projects benefit most from this feature/change? All users would benefit though perhaps most benefit would accrue to library maintainers. Casual users can get feedback on their code not currently possible. Maintainers of large libraries can validate the quality of code more efficiently. Even developers of core would benefit from the feedback upstreamed about anti-patterns. In the example linked above, you can see which keys are problematic for example.

• Maintainability: Will this change streamline code maintenance or simplify its structure? A tool with hard data would help make the performance dimension of maintainability less prone to speculation. I don't foresee a significant maintenance burden for the global diagnostics themselves. It is likely with global diagnostics promoting better design that requests to refactor complex parts of the core can be avoided more frequently.

Community Feedback

The desire for such global diagnostics first arose during a Mathlib maintainers meeting where it received strong support. It was then put to Zulip for further community discussion.

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.

Start by reading the existing Meta.Diagnostics functionality described in the proposal and review the linked Zulip discussion about tracking frequently applied simp theorems. Compare what diagnostics already records with the proposed environment-level data, including the option flag and periodic-use constraints. Done would require a concrete, agreed design for global tracking; typeclass-instance tracking is explicitly outside the initial scope.