Demo (Skimmer): replacing deprecated declarations

Stream: mathlib4

[Thomas Murrills]

I'm currently working on infrastructure for elaboration-aware library-scale utilities (Skimmer), and I'm starting with the use case of refactoring occurrences of deprecated declarations by replacing them with their current version. Here's a small demo of the core action:
AdprecationDemo.mp4

Currently this requires that the names only differ in their last component, but the goal is of course to make this utility fully general, and to also allow custom specification of arbitrarily complex refactors. More generally, Skimmer is intended to be a "cotool" that provides an environment in which to build and a harness in which to run other, modular tools at library scale like refactors

Crucial to all this, though, are the ergonomics, which are not addressed by the demo! Skimmer ought to

• be easy to control/use (activate, run tools, etc.)
• be easy to extend locally, via third parties, and also "mid-library"
• be able to run its tools nonlocally (i.e. in CI)
• be able to run its tools without asking the user to make changes to (or to leave!) their repo/lakefile; an initial setup should be enough to make it accessible and extendable

among other requirements.

One approach that currently seems promising for these goals is the use of lake plugins. They let us run initializers at the start of each file during build, and thus hook into the actual build process with e.g. linters and environment extensions without creating a custom frontend (which would be subject to drifting away from the "real" frontend, and would necessitate its own custom notion of a build, which comes with a maintainability cost).

(Another option is to try to use lake facets somehow, but these can only fetch the result of the build, and thus miss out on all the elaboration information which is crucial to tools like this. I don't know a way to inject something into the build process itself within a facet without either creating a custom frontend/build process there (which again is fragile and less maintainable) or turning back to plugins anyway.)

I'd love to hear any other ideas or prior art re: library development tools, even in other languages; I'm especially curious about the ergonomics and UX. Thanks! :)