feat(tactic/frozen): add tactics about frozen locals #7652
Conversation
In Lean, any `revert` can fail due to frozen local instances. I add some tactics to detect this situation and unfreeze local instances as necessary. See the module docs for details. --- I need this to make some of my other tactics more robust.
| the local constants whose unique names appear in `hs` are frozen. -/ | ||
| meta def unfreeze_if_necessary_for_name_set (hs : name_set) : tactic bool := do | ||
| tt ← any_is_frozen_name_set hs | pure ff, | ||
| unfreeze_local_instances, |
There was a problem hiding this comment.
unfreeze should always be followed by freeze, since thawed instances are slow. Please check out and use the unfreezing combinator.
There was a problem hiding this comment.
BTW, there's also unfreezing_hyp which is similar to this function.
There was a problem hiding this comment.
Yeah, I found the unfreezing combinator after I had written all this stuff. My eventual use case is to make sure that certain reverts aren't blocked by frozen instances. Is it even worth checking whether the revert would be blocked (which can be somewhat expensive), versus just unfreezing (revert_lst ...) without the check?
There was a problem hiding this comment.
Freeze and unfreeze are fairly cheap. Freeze requires lean to check for every hypothesis whether it is a type class or not, but that's it. There should be no performance impact (after the freeze) if the instances do not change.
The main performance issue is staying in the unfrozen state, because this disables the TC cache.
gebner
added
the
awaiting-author
|
This is made fully redundant by the way Lean 4 deals with the instance cache. |
In Lean, any
revertcan fail due to frozen local instances. I add sometactics to detect this situation and unfreeze local instances as necessary. See
the module docs for details.
I need this to make some of my other tactics more robust.