Leaff on mathlib PR

Stream: general

[Andrew Yang]

Sorry for cross-posting, but I think not much people is following the Lean Together 2024 stream now.
Is it possible to run leaff on a mathlib PR? I remember seeing some instructions but cannot find it now.

[Eric Rodriguez]

cc @Alex J. Best

[Alex J. Best]

It used to be possible to just merge #8479 into (a new copy of) your branch, to get a diff in the github actions output. However I have not had time recently to update leaff so until the lean version is bumped to the version mathlib uses that wont work. I'll see if the update builds but if it doesnt im not sure when I'll get round to fixing it sadly

[Andrew Yang]

It is a great tool but if manual labour is needed everytime lean updates, I'm worried if this will rot quickly. Is there not a better solution or it is unavoidable as lean is still in rapid development?

[Alex J. Best]

Some aspects of this are unavoidable, Leaff makes heavy use of lean
internals and meta stuff which can change with less backwards compatibility
than e.g. some parts of mathlib for example right now.
There is the more general issue, that there is (as far as I know) no ready
to go analogue of https://github.com/leanprover-contrib/lean-upgrade-action
that handles clean updates automatically, and notifies the developer of the
library only when something manual needs to be done. Writing such an action
probably would only take the right person a day or something and I think at
this point would benefit the community a lot (though maybe something
analogous is on the reservoir roadmap anyway).
Btw I did the upgrade yesterday so that Leaff should now work with new
mathlib.