Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-10-02T17:23:06Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/31iMod doesn't handle mismatched mask2020-10-02T17:23:06ZGhost UseriMod doesn't handle mismatched maskLike in
```coq
Lemma vs_demo (l: loc) (E1 E2: coPset):
((|={E1, E2}=> True) ★ l ↦ #1)%I
⊢ WP !#l @ ⊤ {{ _, True }}.
Proof.
iIntros "(HPQ & Hl)".
iVs "HPQ". (* error: not a view shift *)
```
Ideally, since load is a...Like in
```coq
Lemma vs_demo (l: loc) (E1 E2: coPset):
((|={E1, E2}=> True) ★ l ↦ #1)%I
⊢ WP !#l @ ⊤ {{ _, True }}.
Proof.
iIntros "(HPQ & Hl)".
iVs "HPQ". (* error: not a view shift *)
```
Ideally, since load is atomic, using `iVs` here should generate two goals, the first one as a side condition saying that `E1 ⊆ ⊤`, and second one doing the view shift and send us to `E2` masked weakest pre.
cc @robbertkrebbers @jung. Hope I clarify the problem :p https://gitlab.mpi-sws.org/iris/iris/-/issues/29Bring back Logically Atomic Triples (Coq + docs)2019-11-01T13:09:17ZJeehoon Kangjeehoon.kang@kaist.ac.krBring back Logically Atomic Triples (Coq + docs)* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendi...* [x] Implement logically atomic triples in Coq.
* [ ] Do a LaTeX write-up of logically atomic triples (either in The Iris Documentation, or referenced from there).
---
Original description
- May I ask if the POPL 2015 paper's appendix is still in the repository (http://plv.mpi-sws.org/iris/appendix.pdf)?
- Do you have a plan to merge the appendix of POPL 2015 paper and that of ICFP 2016? It would be definitely helpful to readers like me.
---
@jung wrote
The POPL 2015 appendix has been split into two parts:
* The Iris Documentation is describing Iris in general, from the model through the base logic to the most important derived constructions. The version matching Iris 2.0 can be found on the website. It should have more derived constructions than it does, like STSs... however, we are currently in the process of redesigning how constructions like STSs describe their interface to the world, so now would be a bad time to update the documentation :/
* The details of logically atomic triples. These triples have not been ported to later versions of Iris, which is why they don't show up in the current appendix. Unfortunately, since pretty much all examples involve logically atomic triples, those are now all outdated as well. (On paper, that is.)
What, specifically, are you missing from the POPL 2015 appendix?
https://gitlab.mpi-sws.org/iris/iris/-/issues/16Document variable naming conventions2019-11-01T14:12:15ZRalf Jungjung@mpi-sws.orgDocument variable naming conventionsWe should
* [x] Convert naming.txt to markdown
* [ ] document the naming conventions for single-letter variable names
* [ ] maybe make them more consistent between Coq and LaTeX.
* [x] Document postfixes like C, T, R, G
Cc @robbertkreb...We should
* [x] Convert naming.txt to markdown
* [ ] document the naming conventions for single-letter variable names
* [ ] maybe make them more consistent between Coq and LaTeX.
* [x] Document postfixes like C, T, R, G
Cc @robbertkrebbers