Leaff: a Lean library diff tool

Abstract: I'll present the design and implementation, and a usage demo, for a Lean diff tool called Leaff. This has at least two potential uses. One is summarising the changes to a library's Lean environment over time, for example when a new commit modifies a Lean library, or when the version of Lean being used to compile the library changes, the resulting library will be measurably different, in ways that are not always apparent from the source changes. But with Leaff we can get a short summary listing lemmas added and removed, renames that took place, attributes and imports that changed etc., which can be helpful when reviewing contributions, or making sure that proposed modifications to Lean don't have unintended downstream consequences. The other use for this tool is when upgrading dependencies, the Lean ecosystem is relatively accepting of breaking changes, normally little backwards compatibility is maintained over time in mathlib, Std or in Lean core itself. This makes the problem of upgrading dependencies time consuming, if a definition or lemma is moved or renamed, downstream libraries must be modified to complete the upgrade, and disentangling what relevant changes were made can be hard from looking at source commits alone. I'll discuss this a bit, and how a future version of this tool may be able to allieviate some such issues completely automatically.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the topic

Lean Together 2024