Zulip Chat Archive

Stream: general

Topic: tactic-block-local caching


view this post on Zulip Patrick Massot (Apr 03 2019 at 09:40):

@Keeley Hoek could you tell us a bit about #837? Is it something end users should know about? Do we need to do anything?

view this post on Zulip Keeley Hoek (Apr 03 2019 at 09:56):

It's a utility function for tactic-writers mainly, which lets you compute something once in a tactic block or per definition (the idea that I should have different scopes was Simon's). It doesn't save-restore computed proofs like the other code I was spruiking a while ago unfortunately, which doesn't work via this method. Saving and loading expressions is so slow from within lean that barring a small modification to lean which adds io functions which do that for you from C++, I don't think it could be possible in vanilla.


Last updated: May 10 2021 at 23:11 UTC