Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-07-15T16:05:09Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/306Iris 3.3 release planning2020-07-15T16:05:09ZRalf Jungjung@mpi-sws.orgIris 3.3 release planningWhat needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed s...What needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed script in the CHANGELOG.
* [x] Release a matching std++.
* [x] Write announcement.
* [x] Release opam packages on coq opam registry.
* [x] Send out announcements.Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/403Iris 3.42021-03-06T12:22:13ZRalf Jungjung@mpi-sws.orgIris 3.4There was a Coq 8.13 release, so following our promise for the Coq Platform, we should make a compatible release ASAP (the Coq release was already more than a month ago).
[Milestone with potential release blockers](https://gitlab.mpi-sw...There was a Coq 8.13 release, so following our promise for the Coq Platform, we should make a compatible release ASAP (the Coq release was already more than a month ago).
[Milestone with potential release blockers](https://gitlab.mpi-sws.org/iris/iris/-/milestones/6)https://gitlab.mpi-sws.org/iris/iris/-/issues/333Iris Library Best Practices2020-08-06T16:37:12ZRalf Jungjung@mpi-sws.orgIris Library Best PracticesWe should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered for...We should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @blaisorblade pointed out that it is non-obvious that specs should not contain `own` but instead wrap those things in their own definitions that depend on `libG` instead of `inG`.https://gitlab.mpi-sws.org/iris/iris/-/issues/239Iris logo2021-02-05T12:43:21ZRobbert KrebbersIris logoWe need a logo for the project. The issue collects proposals so far:
By @janno:
![Janno](https://robbertkrebbers.nl/iris_logos/janno.jpg)
By @lgg:
![Janno](https://robbertkrebbers.nl/iris_logos/leon.jpg)
As @dreyer said: I think if ...We need a logo for the project. The issue collects proposals so far:
By @janno:
![Janno](https://robbertkrebbers.nl/iris_logos/janno.jpg)
By @lgg:
![Janno](https://robbertkrebbers.nl/iris_logos/leon.jpg)
As @dreyer said: I think if we all start singing I-R-I-S to the tune of YMCA, we'll really be getting somewherehttps://gitlab.mpi-sws.org/iris/iris/-/issues/68iSpecialize should work even if the wand is under a later.2017-05-19T15:20:29ZJacques-Henri JourdaniSpecialize should work even if the wand is under a later.In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?In the proofmode, if I have, say, the hypothesis `"H1" : ▷ (A -* B)`, then `iSpecialize ("H1" with "[]")` does not work. Is there any good reason for this ?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/325iSpecialize with "[% //]" does not report an error if done fails2020-06-26T10:51:38ZTej Chajedtchajed@gmail.comiSpecialize with "[% //]" does not report an error if done failsiSpecialize on `SPureGoal true` does not report an error message.
```coq
From iris Require Import proofmode.tactics.
Theorem test {PROP: bi} (P: PROP) :
(⌜False⌝ -∗ P) -∗
P.
Proof.
iIntros "Hwand".
iSpecializePat_go "Hwand" [sp...iSpecialize on `SPureGoal true` does not report an error message.
```coq
From iris Require Import proofmode.tactics.
Theorem test {PROP: bi} (P: PROP) :
(⌜False⌝ -∗ P) -∗
P.
Proof.
iIntros "Hwand".
iSpecializePat_go "Hwand" [spec_patterns.SPureGoal true] (* with "[% //]" *).
Abort.
```
The reason is that this match is failing: https://gitlab.mpi-sws.org/iris/iris/-/blob/11f9d567c2a8b1f52d00e562d5cc39262463cf9e/theories/proofmode/ltac_tactics.v#L849. It should have another case that prints the normal Coq goal rather than the IPM goal.https://gitlab.mpi-sws.org/iris/iris/-/issues/25iSplitL "persistent_hyp": Improve error2016-08-06T00:12:25ZRalf Jungjung@mpi-sws.orgiSplitL "persistent_hyp": Improve errorCurrently, if I say `iSplitL "H"` where `H` is persistent, it says that `H` has not been found. That's confusing, "H" exists -- but it looked in the spatial context only. The tactic should either accept persistent hypotheses or the error...Currently, if I say `iSplitL "H"` where `H` is persistent, it says that `H` has not been found. That's confusing, "H" exists -- but it looked in the spatial context only. The tactic should either accept persistent hypotheses or the error should say "... has not been found in the spatial context" or so.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/199iSplitL no longer checks if assumptions are spatial2018-06-10T20:13:10ZRalf Jungjung@mpi-sws.orgiSplitL no longer checks if assumptions are spatialThe following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```The following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/146Lemmas about updates should be instantiated by default witht the current BI i...2018-07-13T08:51:27ZJacques-Henri JourdanLemmas about updates should be instantiated by default witht the current BI instead of `iProp`The instances for the `FUpd` and `FUpdFacts` type classes are set in a way that gives the priority to `iProp`? Therefore, when using lemmas about updates in `vProp`, we sometimes have to manually instantiate them with the current BI. Oth...The instances for the `FUpd` and `FUpdFacts` type classes are set in a way that gives the priority to `iProp`? Therefore, when using lemmas about updates in `vProp`, we sometimes have to manually instantiate them with the current BI. Otherwise, the lemmas are instantiated with `iProp` and used through the embedding.
See, for example https://gitlab.mpi-sws.org/FP/sra-gps/blob/gen_proofmode_WIP/theories/examples/circ_buffer.v#L236
The instances for the `AsValid` type class prioritizes the fact of not using the embedding, so we should be able to fix this issue by simply making sure the search for `AsValid` occurs before `FUpd`, but I do not know how to do that.
@robbertkrebbers, any idea?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/81Let iAlways clear the spatial context2017-10-27T12:33:40ZRalf Jungjung@mpi-sws.orgLet iAlways clear the spatial contextRight now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is simil...Right now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is similar to the difference between `iIntros "!>"` and `iNext` -- the latter may affect the context, the former will not. Furthermore, this is backwards compatible because iAlways will now only succeed in strictly more cases.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/473Logically atomic triples conflict with autosubst notation2023-09-26T10:38:05ZRalf Jungjung@mpi-sws.orgLogically atomic triples conflict with autosubst notationAutosubst uses `>>` and `>>>` as notation for some operations, which conflicts with our logically atomic triples:
```
Section notation_conflicts.
Context `{!heapGS Σ}.
(* Test compatibility with autosubst notation. *)
Reserved Not...Autosubst uses `>>` and `>>>` as notation for some operations, which conflicts with our logically atomic triples:
```
Section notation_conflicts.
Context `{!heapGS Σ}.
(* Test compatibility with autosubst notation. *)
Reserved Notation "f >>> g" (at level 56, left associativity).
Reserved Notation "sigma >> tau" (at level 56, left associativity).
Lemma conflict_test1 P Q e v :
⊢ <<< P >>> e @ ∅ <<< Q, RET v >>>.
(* Syntax error: '>>>' expected after [term level 200] (in [term]) *)
```
I tried changing the `'>>>'` in our notations to `>>>` or to `'>' '>' '>'`, neither of that helped. (We are using `} } }` for texan triples, I have no idea why.) I also tried removing the level declarations from the logatom triples, again that made no difference. I don't actually understand what is happening here anyway, these were complete shots in the dark.
We need someone who actually understand the Coq notation system for this... maybe @blaisorblade?https://gitlab.mpi-sws.org/iris/iris/-/issues/69Make `done` solve the goal when one of the Iris hypothesis is `False`2017-05-19T15:20:29ZJacques-Henri JourdanMake `done` solve the goal when one of the Iris hypothesis is `False`As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.As in Coq, this should work even if the hypothesis is not syntacticaly `False`, but only convertible to it.https://gitlab.mpi-sws.org/iris/iris/-/issues/148Make `iNext` smarter for mixed `▷` and `▷^(n+m)`2018-02-20T15:29:40ZLéon GondelmanMake `iNext` smarter for mixed `▷` and `▷^(n+m)`Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n m : ▷ ▷^...Following the (fixed) issue (https://gitlab.mpi-sws.org/FP/iris-coq/issues/141), there is still an error w.r.t. addition in the laterN modality:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n m : ▷ ▷^(n+m) P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
```
```coq
(* Gives
"H" : ▷ ▷^(n + m) P
--------------------------------------∗
▷ P
*)
```
forgetting erroneously to cancel `n` in the premise `"H"`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/141Make `iNext` smarter for mixed `▷` and `▷^n`2018-01-27T16:11:56ZRobbert KrebbersMake `iNext` smarter for mixed `▷` and `▷^n`See below:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n : ▷ ▷^n P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
(* Gives
"H" : ▷ ▷^n P
--------------------------------------∗
▷ P
*)
```See below:
```coq
From iris Require Import proofmode.tactics.
Lemma foo {M} (P : uPred M) n : ▷ ▷^n P ⊢ ▷^n ▷ P.
Proof. iIntros "H". iNext.
(* Gives
"H" : ▷ ▷^n P
--------------------------------------∗
▷ P
*)
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/155Make `iPureIntro` able to introduce affine pure assertions when the context i...2018-02-15T16:08:05ZJacques-Henri JourdanMake `iPureIntro` able to introduce affine pure assertions when the context is emtpy.The current lemma behind `iPureIntro` is:
```coq
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
```
Could we change it a bit, ...The current lemma behind `iPureIntro` is:
```coq
Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
Proof. intros ??. rewrite /envs_entails -(from_pure _ Q). by apply pure_intro. Qed.
```
Could we change it a bit, so that we ask for `FromPure true Q φ` when the context is empty? That way, we could introduce CFML's affine pure assertions transparently when the context is empty.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/343Make CI fail when proofs depend on auto-generated names2021-04-12T17:11:13ZRalf Jungjung@mpi-sws.orgMake CI fail when proofs depend on auto-generated namesWe already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.We already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.https://gitlab.mpi-sws.org/iris/iris/-/issues/158Make clear which arguments of tactics are optional in `ProofMode.md`2020-12-19T17:43:20ZRobbert KrebbersMake clear which arguments of tactics are optional in `ProofMode.md`See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050See the discussion in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/116#note_25050https://gitlab.mpi-sws.org/iris/iris/-/issues/30Make coqchk (make verify) work2016-08-19T10:00:16ZRalf Jungjung@mpi-sws.orgMake coqchk (make verify) workCurrently, `make verify` fails with a stack overflow while checking `iris.prelude.pretty.pretty_N_inj`. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/s...Currently, `make verify` fails with a stack overflow while checking `iris.prelude.pretty.pretty_N_inj`. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/show_bug.cgi?id=4788). Can we find a similar work-around here?
Cc @robbertkrebbers https://gitlab.mpi-sws.org/iris/iris/-/issues/112Make invariants and slices closed under equivalence2018-02-08T10:43:12ZRalf Jungjung@mpi-sws.orgMake invariants and slices closed under equivalenceThis has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the followi...This has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
```coq
Lemma inv_iff P Q :
later persistently (P <-> Q) -> inv P -> inv Q.
```
I think this may be worth it, *if* it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for `slice`, which requires either a separate closure in `slice` (so the one in `inv` does not help), or doing the same kind of closure in `saved_prop_own` (but then, do we also want the equivalent law for `saved_pred_own`?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.https://gitlab.mpi-sws.org/iris/iris/-/issues/101Make Iris run in jsCoq2017-11-30T09:53:53ZRalf Jungjung@mpi-sws.orgMake Iris run in jsCoqCurrent status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert al...Current status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert already mentioned that he wanted to look into that.