Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-07-18T09:46:52Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/205Make notation for pure and plainly affine2021-07-18T09:46:52ZRalf Jungjung@mpi-sws.orgMake notation for pure and plainly affineI think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/196Extend `iApply` to deal with pure goals2019-11-01T12:50:03ZGlen MévelExtend `iApply` to deal with pure goalsIf I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Pr...If I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Prop) (P : iProp Σ) :
(A → B) → (P -∗ ⌜A⌝) → (P -∗ ⌜B⌝).
Proof.
iIntros (ab pa) "p".
(* what I would like to write directly: *)
Fail iApply ab. (* Tactic failure: iPoseProof: not a uPred. *)
(* what I need to write instead: *)
iApply (uPred.pure_mono _ _ ab).
iApply pa.
iExact "p".
Qed.
```
(tested with coq-iris dev.2018-04-10.0)https://gitlab.mpi-sws.org/iris/iris/-/issues/130Make iApply "with" specialization lazier2019-11-01T13:46:23ZRobbert KrebbersMake iApply "with" specialization lazierFor example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tr...For example, the `[$]` specialization pattern for frame inference is too eager. In the example below, it would like to be able to prove the premises of `swap_spec` by framing. However, this does not quite work because `wp_apply` first tries to prove the premises of the lemma by framing, and then tries to match the goal. Since framing is performed first, it instantiates evars in the wrong way. If it would first try to match the goal, and then frame, the evars would already be instantiated when framing is performed.
```coq
From iris.heap_lang Require Import proofmode notation.
Parameter swap : val.
Definition rotate_r : val := λ: "x" "y" "z",
swap "y" "z";; swap "x" "y".
Section proof.
Context `{!heapG Σ}.
Lemma swap_spec x y v1 v2 :
{{{ x ↦ v1 ∗ y ↦ v2 }}} swap #x #y {{{ RET #(); x ↦ v2 ∗ y ↦ v1 }}}.
Proof. Admitted.
Lemma rotate_r_spec x y z v1 v2 v3 :
{{{ x ↦ v1 ∗ y ↦ v2 ∗ z ↦ v3 }}}
rotate_r #x #y #z
{{{ RET #(); x ↦ v3 ∗ y ↦ v1 ∗ z ↦ v2 }}}.
Proof.
iIntros (Φ) "(Hx & Hy & Hz) Post". do 3 wp_lam.
Fail wp_apply (swap_spec with "[$]").
wp_apply (swap_spec y z with "[$]").
Admitted.
End proof.
```
It's probably easy to come up with a simpler example, but I ran into this one while preparing the Iris tutorial.
Another example:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```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/235Documentation for the algebra folder2019-11-01T11:10:11ZRobbert KrebbersDocumentation for the algebra folderIt would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical...It would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical structures are used.https://gitlab.mpi-sws.org/iris/iris/-/issues/332Become part of Coq Platform?2020-07-21T18:01:10ZRalf Jungjung@mpi-sws.orgBecome part of Coq Platform?We should consider making iris part of the [Coq Platform](https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md).
Quoting Michael Soegtrop:
> So if IRIS becomes part of the platform, the platform takes care that there is ...We should consider making iris part of the [Coq Platform](https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md).
Quoting Michael Soegtrop:
> So if IRIS becomes part of the platform, the platform takes care that there is a reliable, fast and fool proof way to install Coq including IRIS on Windows, OSX and - maybe a bit less fool proof - Linux. This should make it easier for teachers and interested explorers to install IRIS. On the other hand you agree to do your best to deliver a working release of IRIS for any major Coq release (like 8.12, 8.13) within at most 3 months, better 1 month.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.