Use HB.lock(-like) sealing
hierarchy-builder offers a sealing mechanism that looks extremely syntactically lightweight, while doing module-based sealing under the hood (meaning it probably seals better than our
seal type, though I am not sure if that makes a difference in practice.
HB.lock Definition new_concept := 999999. Lemma test x : new_concept ^ x ^ new_concept = x ^ new_concept ^ new_concept. Proof. Time Fail reflexivity. (* takes 0s *) rewrite new_concept.unlock. Time Fail reflexivity. (* takes 7s, the original body is restored *) Abort.
This is exactly the kind of locking API I always wanted: just adding a keyword in front of the
Definition, done. This would make it a no-brainer to seal basically every
iProp that our reusable libraries export.
- Check if this actually works in Iris
- Decide if we want to do this, and how -- are we okay with a dependency on hierarchy-builder?