user_attribute.cache_cfg

Stream: general

[Yury G. Kudryashov]

Hi, what is the purpose of user_attribute.cache_cfg. In particular, what does to_additive.cache_cfg do?
Here is the code:

cache_cfg := ⟨λ ns, ns.mfoldl (λ dict n, do
    val ← to_additive_attr.get_param n,
    pure $ dict.insert n val) mk_name_map, []⟩

[Scott Morrison]

Unfortunately this is poorly documented... Simon Hudon has explained it to me at least once, but since none of my tactics have ended up using it I still don't know the details.

[Mario Carneiro]

The ns input is a list of all declarations that have the attribute, and the function is responsible for filling the cache from the list

[Mario Carneiro]

In this case, the cache keeps track of the mapping of mul -> add definitions, and the data is stored in the attribute data, so we have to look up each definition and put the stored parameter in the map

[Yury G. Kudryashov]

@Mario Carneiro When Lean calls this function?

[Mario Carneiro]

when the user attribute is applied to a new theorem

[Simon Hudon]

@Mario Carneiro I think it might applied more lazily than that. The cache may be invalidated every time you apply the attribute to a new definition / theorem but you don't actually need to rebuild the cache right then and there. You can wait until the next time the cache gets queried.