Zulip Chat Archive

Stream: general

Topic: unfreezeI


Johan Commelin (Apr 25 2020 at 13:53):

I've never understood what unfreezeI was for. But I know that we needed it because of "core". Now that "core" is no longer a reason... can we get rid of unfreezeI?

Gabriel Ebner (Apr 25 2020 at 14:10):

The "core" reason is deeply buried in type class resolution. IIRC, calling unfreezeI (partly) disables caching for type class resolution. @Anne Baanen tried to remove this caching mechanism, but apparently it's not entirely trivial.

Sebastian Ullrich (Apr 25 2020 at 17:56):

But the caching was actually broken for the longest time in such a way that unfreezeI etc wasn't necessary, until Leo fixed it. Can't that fix just be reverted? I don't remember anyone noticing any actual benefits such as better performance from the fix.

Patrick Massot (Apr 25 2020 at 18:07):

I have a more relevant question (I think). Do we know what will be the situation in Lean 4? We don't want to unlearn our instance cache management habits in Lean 3 only to relearn them when we'll switch to Lean 4? I don't expect Leo will change his mind on this question, but maybe the question itself will become irrelevant in Lean 4.

Sebastian Ullrich (Apr 25 2020 at 18:18):

I believe the plan is that all surface-level binders automatically reset the cache. Only tactics introducing instances internally have to worry about it.

Patrick Massot (Apr 25 2020 at 18:21):

I'm afraid I don't understand this whole story well enough to parse this answer.

Patrick Massot (Apr 25 2020 at 18:21):

Does it mean we won't need haveI and letI?

Sebastian Ullrich (Apr 25 2020 at 18:28):

Yes, unless you're a tactic writer and care about that level of optimization.


Last updated: Dec 20 2023 at 11:08 UTC