Depend on Coq-elpi
Coq-elpi might bring various benefits to Iris:
- We can use its locker to replace our sealing mechanism. As noticed in #527, locker might be more efficient, and it also reduces the amount of boilerplate.
- We can use Elpi to create "deriving" like mechanisms, for example, for the infamous
inG
andΣ
definitions. - In the future we can investigate if we can use Elpi to implement parts of the Iris Proof mode more efficiently.
Coq-elpi is available in opam, and seems pretty stable. What do we think of letting Iris depend on Coq-elpi?