caching information in a tactic

Stream: new members

[Kevin Lacker]

Is there any way to cache information between multiple runs of a tactic? For example, whenever you run library_search, some of the work is specific to the current goal and environment, like looking up every lemma whose head symbol matches the current goal and seeing if it can be applied to the current goal. That work is then redone every time you run library_search until the goal changes. You'd need a way to store and access global or global-ish variables, and a way to flush the cache whenever the imports or the goal changes.

[Julian Berman]

someone who knows what they're talking about will likely answer this, my non-functional-programming brain just knows that I think the answer for these languages has you something something state monad'ing, but just grepping finds https://leanprover-community.github.io/mathlib_docs/tactic/cache.html if that helps (it doesn't do what you want but probably it'd need to manipulate persistent state for a goal it looks like so you may be able to steal from its implementation)

[Julian Berman]

or https://github.com/leanprover-community/mathlib/blob/f75dbd3/src/tactic/local_cache.lean#L207 looks even more likely to be relevant though it doesn't have a docstring in the docs

[Kevin Lacker]

hmm, its implementation (for the first link) seems to be via things like unfreeze_local_instances that call into c++

[Alex J. Best]

the second one of those links was introduced in #837 and library_search is one of the stated goals there in fact.

[Kevin Lacker]

run_once_under_name looks promising. i guess get_env and add_decl let you manipulate data globally

[Alex J. Best]

There is also the open pr #2300 for caching whole blocks also by Keeley

[Kevin Lacker]

hmm, that PR looks a bit abandoned

[Kevin Lacker]

caching blocks seems like a pretty good idea though

[Mario Carneiro]

I don't think either of Keeley's PR's can solve the problem in general, and in fact I don't think there is any way to do this in pure lean without C++ support, because it requires caching across different runs of the same file, which is much harder. Lean currently treats the entire file as a functional program that it can pause and restart at various points in order to allow the live editing behavior without "old" data from previous runs affecting the result, but this makes it much harder for anything a tactic does to store information in any permanent way except through the environment, which is discarded in a new run.