BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Alex Best (King's College London) DTSTART:20240110T174500Z DTEND:20240110T181500Z DTSTAMP:20260405T221251Z UID:LeanTogether2024/9 DESCRIPTION:Title: Leaff: a Lean library diff tool\nby Alex Best (King's College London) as part of Lean Together 2024\n\n\nAbstract\nI'll present the des ign and implementation\, and a usage demo\, for a Lean diff tool called Le aff.\nThis 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 compi le the library changes\, the resulting library will be measurably differen t\, in ways that are not always apparent from the source changes.\nBut wit h Leaff we can get a short summary listing lemmas added and removed\, rena mes that took place\, attributes and imports that changed etc.\, which can be helpful when reviewing contributions\, or making sure that proposed mo difications to Lean don't have unintended downstream consequences.\nThe ot her use for this tool is when upgrading dependencies\, the Lean ecosystem is relatively accepting of breaking changes\, normally little backwards co mpatibility is maintained over time in mathlib\, Std or in Lean core itsel f. This makes the problem of upgrading dependencies time consuming\, if a definition or lemma is moved or renamed\, downstream libraries must be mod ified to complete the upgrade\, and disentangling what relevant changes we re made can be hard from looking at source commits alone. I'll discuss thi s a bit\, and how a future version of this tool may be able to allieviate some such issues completely automatically.\n LOCATION:https://researchseminars.org/talk/LeanTogether2024/9/ END:VEVENT END:VCALENDAR