Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T13:24:47Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/123Add a general constructor from an affine BI2019-11-01T13:24:47ZRalf Jungjung@mpi-sws.orgAdd a general constructor from an affine BIIn master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just...In master, there is a nice correspondence between the proofs in `primitive.v` and the rules in the appendix. We should try to maintain such a correspondence. Currently, `upred.v` proofs things in the model that can be derived, and just claims them to be `(ADMISSIBLE)` in a comment.
I see two ways to achieve that:
* We could provide a general way to construct a `BiMixin` from a proof of all the laws given in the appendix.
* We could do the more specific thing and first prove the appendix laws for `uPred`, and subsequently not use `unseal` when proving the `BiMixin`.https://gitlab.mpi-sws.org/iris/iris/-/issues/117Make some of the `wp_` tactics language independent2019-11-01T13:23:45ZRobbert KrebbersMake some of the `wp_` tactics language independentA large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.A large part of `wp_bind`, `wp_pure`, `wp_apply` and `wp_simpl_expr` is duplicated for each language Iris is instantiated with. It would be good to factor out some part of the code.https://gitlab.mpi-sws.org/iris/iris/-/issues/104smarter iIntros for plainly modality2019-11-01T13:16:44ZRobbert Krebberssmarter iIntros for plainly modalityThe following discussion from !71 should be addressed:
- [ ] @jung started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/71#note_20642): (+1 comment)
> Would it be a good idea or not for `iIntros` to be able...The following discussion from !71 should be addressed:
- [ ] @jung started a [discussion](https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/71#note_20642): (+1 comment)
> Would it be a good idea or not for `iIntros` to be able to do this without us having to apply `persistently_impl_plainly`? To me, that looks very similar to how it pulls out universal quantifiers from below a box.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/89Support negative selection patterns2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgSupport negative selection patternsIt would be nice to say something like "clear everything except for ...".It would be nice to say something like "clear everything except for ...".https://gitlab.mpi-sws.org/iris/iris/-/issues/78Trouble with iApply and typeclass inference order2019-11-01T13:16:44ZRalf Jungjung@mpi-sws.orgTrouble with iApply and typeclass inference orderThe following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```The following says it all:
```
Lemma test_iApply_1 (M : ucmraT) (P : nat → uPred M) :
▷ (∃ x, P x) -∗ ∃ x, ▷ P x.
Proof.
iIntros "H". Fail iApply uPred.later_exist.
rewrite -uPred.later_exist. by iNext.
Qed.
```https://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 conventions2022-04-08T09:49:43ZRalf 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