Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-01-17T02:16:40Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/351Decouple framing and IntoSep2022-01-17T02:16:40ZRalf Jungjung@mpi-sws.orgDecouple framing and IntoSepCurrently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disab...Currently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disabled some `IntoSep` instances in Perennial for this reason.
It might make sense to have a separate IntoSep for framing that is more optimized for performance and, for example, does not try to exploit fractional things.
This is somewhat similar to https://gitlab.mpi-sws.org/iris/iris/-/issues/186.
To avoid making a mess, probably we should figure out https://gitlab.mpi-sws.org/iris/iris/-/issues/139 first.https://gitlab.mpi-sws.org/iris/iris/-/issues/315Port HeapLang tactics to more efficient style2020-07-15T19:27:00ZRobbert KrebbersPort HeapLang tactics to more efficient styleThe heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248The heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248