Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-11-01T13:02:01Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/263IPM/MoSeL nested disjunction syntax2019-11-01T13:02:01ZDan FruminIPM/MoSeL nested disjunction syntaxWould it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.Would it be possible to support the following syntax for nested disjunctions:
`iDestruct H as (H|H|H)`? Similarly to the `(H1&H2&H3)` syntax for nested separating conjunctions.https://gitlab.mpi-sws.org/iris/iris/-/issues/40iRewrite and internal equality on predicates2016-10-27T14:34:24ZJannoiRewrite and internal equality on predicatesConsider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
```
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iR...Consider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
```
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iRewrite "E".
Abort.
```
It seems to me that iRewrite should succeed here. Is there a logical reason for it to fail? (As opposed to an engineering reason.)
(We are using commit 9c5a95d3b271f4e0d0c657964dfa386070d0b322 in case that matters.)https://gitlab.mpi-sws.org/iris/iris/-/issues/152iRewrite: Support rewriting with Coq hypotheses2019-11-01T12:51:27ZRalf Jungjung@mpi-sws.orgiRewrite: Support rewriting with Coq hypothesesiRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without `Proper` instances.
Cc @tslilyaiiRewrite should be able to rewrite with a Coq equality embedded into Iris. Ideally, if the embedded equality is Leibniz equality, this would work even without `Proper` instances.
Cc @tslilyaiRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/106Iris 3.12018-01-09T15:55:25ZRalf Jungjung@mpi-sws.orgIris 3.1In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels o...In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels of `_ ;; _` and `_ <- _ ;; _`
* [ ] Make sure all our CI'd reverse dependencies build with master.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/209Iris 3.1.0 is compatible with Coq 8.8.1 and coq-mathcomp-ssreflect 1.7.02018-08-29T10:49:18ZJannoIris 3.1.0 is compatible with Coq 8.8.1 and coq-mathcomp-ssreflect 1.7.0The `opam` file currently claims otherwise because these versions of Coq and ssreflect didn't exist when it was written. The only changes necessary are to adapt the `opam` entries for these two packages by increasing their respective upp...The `opam` file currently claims otherwise because these versions of Coq and ssreflect didn't exist when it was written. The only changes necessary are to adapt the `opam` entries for these two packages by increasing their respective upper bound's minor version by 1. I have tested this locally and have not encountered any issues.https://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/273Iris shadows ssreflect new syntax2019-11-22T16:31:07ZPaolo G. GiarrussoIris shadows ssreflect new syntaxIris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
In 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op notations....Iris `[^` notation shadows (and prevents using) ssreflect's new [^ syntax for "block introductions": `move/elim => [^ prefix]`.
In 8.10.1 ssreflect introduced syntax using `[^` and `[^~`, but they're shadowed by iris's big_op notations.
Here's a mininal example. Block introductions are pointless here — but useful for big datatypes.
```coq
From iris.algebra Require Import base.
Lemma foo (n : nat) : n = n.
elim: n => [^ s]. (* Works *)
Restart.
elim: n => [^~ s]. (* Works *)
Abort.
From iris.proofmode Require Import tactics.
Locate "[^". (* big_op notations *).
Lemma foo (n : nat) : n = n.
(* Parse error for each of the following commands: *)
elim: n => [^~ s].
elim: n => [^ s].
(* Each gives:
Syntax error: [tactic:ssripats_ne] expected after '=>' (in [tactic:ssrintros_ne]).
*)
```
Iris version: dev.2019-11-02.2.ea809ed4.https://gitlab.mpi-sws.org/iris/iris/-/issues/329Iris Website Reform2020-09-29T15:48:56ZRalf Jungjung@mpi-sws.orgIris Website ReformWe had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* W...We had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* We'd like to split the website into sub-pages, as the list of papers is getting too long.
* We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
* In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
* We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).
I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.https://gitlab.mpi-sws.org/iris/iris/-/issues/137Iris-internal solve_proper2019-11-01T12:51:26ZRalf Jungjung@mpi-sws.orgIris-internal solve_properWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRustWe have some cases where a variant of `solve_proper` that works *inside* the logic would be really useful:
* When using the fixed point of a monotone function (e.g., total WP).
* For showing co(ntra)variance of types in lambdaRusthttps://gitlab.mpi-sws.org/iris/iris/-/issues/335iris.sty incompatible with acmart2020-07-15T12:25:40ZRalf Jungjung@mpi-sws.orgiris.sty incompatible with acmartThe `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the ...The `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.https://gitlab.mpi-sws.org/iris/iris/-/issues/419Iron slowdown investigation2021-06-17T07:20:40ZRalf Jungjung@mpi-sws.orgIron slowdown investigationIron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iri...Iron has [slowed down by 1.8%](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-metric=instructions&var-project=iron&var-branch=master&var-config=All&var-group=().*&from=1621369920715&to=1622831955880) just by updating Iris from `dev.2021-03-06.3.b0708b01` to `dev.2021-06-03.0.2959900d`. I am not sure if we can do anything about that, but it would be good to at least figure out which changes caused the slowdown (though it looks like there at several, so this might be "death by a thousand cuts").https://gitlab.mpi-sws.org/iris/iris/-/issues/168iSpecialize on implications behaves inconsistently2019-11-01T13:35:17ZRalf Jungjung@mpi-sws.orgiSpecialize on implications behaves inconsistentlyIn a goal like
```
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
```
doing `iSpecialize ("HPQ" with "HP")` behaves as expected, but `iSpecialize ("HPQ" with "[]")` ...In a goal like
```
"HP" : ■ P
--------------------------------------□
"HPQ" : ■ P → Q
--------------------------------------∗
Q
```
doing `iSpecialize ("HPQ" with "HP")` behaves as expected, but `iSpecialize ("HPQ" with "[]")` fails saying
```
iSpecialize: (■ P → Q)%I not an implication/wand.
```
Here's a testcase:
```coq
Lemma test_plain_impl `{BiPlainly PROP} P Q :
(■ P → (■ P → Q) -∗ Q)%I.
Proof.
iIntros "#HP HPQ".
Fail iSpecialize ("HPQ" with "[]").
Fail iApply "HPQ".
iSpecialize ("HPQ" with "HP"). done.
Qed.
```https://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@mit.eduiSpecialize 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/424Laterable cleanup2021-07-15T07:49:33ZRalf Jungjung@mpi-sws.orgLaterable cleanuphttps://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `late...https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/636 made `make_laterable` more like a normal Iris citizen, but some cleanup remains until this is a regular modality:
* [ ] Define `Laterable` in terms of `make_laterable` (see `laterable_alt`).
* [ ] Rename `make_laterable` to follow our modality naming scheme... `laterably`?
* [ ] Resolve TC backtracking issue around `persistent_laterable`
* [ ] `iMod` for `make_laterable` elimination?