User attribute caching

Stream: metaprogramming / tactics

[Jannis Limperg]

I'm writing a tactic that'll make fairly heavy use of user attributes. As a result, I'm running into two limitations of the user attribute cache API (docs#user_attribute_cache_cfg):

1) The function that creates a cache receives the list of declarations to which the attribute was applied, but not the parameters gives to those attributes. So if you write

@[attr 42] def d := ...

you can cache the fact that d was tagged with attr, but not that it was tagged with 42. This is annoying for my use case because I rely a lot on attribute parameters, so a lot of work ends up uncached.

2) As far as I can tell, cache construction is not incremental: the cache-constructing function is given a list of tagged declarations, but there is no way to add or remove declarations. I suspect this leads to a lot of duplicate work. In particular, I believe the construction of the simp set is a significant cost center, which is no surprise if it is reconstructed from scratch all the time.

Any chance one of our resident C++ wizards would like to take a look at this?

[Gabriel Ebner]

The main performance footgun is described here: https://leanprover-community.github.io/mathlib_docs/notes.html#user%20attribute%20parameters

[Jannis Limperg]

That's a good note, thanks! So can I use get_param_untyped in the function that constructs the attribute cache, then parse that expr by hand? Can I assume that this expr is fully evaluated? That would solve problem 1.

[Gabriel Ebner]

Yes you should parse it by hand. It is fully elaborated.

[Gabriel Ebner]

(By providing a custom reflected instance, you can also store the data as an ill-typed expression.)

[Jannis Limperg]

Okay, very nice. That'll be a bunch of work, but not too bad. Any comments on the non-incrementality issue?

[Gabriel Ebner]

Worry about it later?

[Jannis Limperg]

Fair enough. At the current rate, the tactic won't be done until we're all on Lean 4 anyway. :upside_down: