tactic-block-local caching

Stream: general

[Patrick Massot]

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

[Keeley Hoek]

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.