Zulip Chat Archive

Stream: new members

Topic: caching information in a tactic


view this post on Zulip Kevin Lacker (Oct 20 2020 at 21:52):

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.

view this post on Zulip Julian Berman (Oct 20 2020 at 22:05):

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)

view this post on Zulip Julian Berman (Oct 20 2020 at 22:06):

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

view this post on Zulip Kevin Lacker (Oct 20 2020 at 22:15):

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

view this post on Zulip Alex J. Best (Oct 20 2020 at 22:17):

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

view this post on Zulip Kevin Lacker (Oct 20 2020 at 22:18):

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

view this post on Zulip Alex J. Best (Oct 20 2020 at 22:20):

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

view this post on Zulip Kevin Lacker (Oct 20 2020 at 22:27):

hmm, that PR looks a bit abandoned

view this post on Zulip Kevin Lacker (Oct 20 2020 at 22:27):

caching blocks seems like a pretty good idea though

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:31):

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.


Last updated: May 14 2021 at 07:19 UTC