Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-01-21T21:41:49Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/439Tracking issue for append-only list RA2022-01-21T21:41:49ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
The a...This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
The algebra part of this has been merged; what remains is the base_logic wrapper.
## Open issues
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use. This is discussed in more generality at https://gitlab.mpi-sws.org/iris/iris/-/issues/412.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper....This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/405Tracking issue for HeapLang interpreter2021-02-16T11:03:04ZRalf Jungjung@mpi-sws.orgTracking issue for HeapLang interpreterThis is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
...This is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.