Run command at end of every file?

Stream: lean4

[Scott Morrison]

I would like to register a command to run at the end of every (subsequent) file, or alternatively to run after each new declaration is added to the environment. Are either of these possible?

In particular, I'd like explore building the library_search cache incrementally, using a persistent environment extension. (I would either just persist the state as an Array (Name × Array (DiscrTree.Key)), and then build the actual DiscrTree when library_search is used, or possibly persist the state as an actual DiscrTree, and provide a function Array DiscrTree → DiscrTree to merge the saved states from multiple imports.)

[Gabriel Ebner]

You could register a linter. They are run after every top-level command.

[Jannis Limperg]

FYI I already wrote functions for merging DiscrTrees. They should be in std.