Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-10-26T19:12:53Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/437Typo in documentation2021-10-26T19:12:53ZAlexandre MoineTypo in documentationHi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two l...Hi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two lines. This seems to be the only occurrencehttps://gitlab.mpi-sws.org/iris/iris/-/issues/436opam package description is not helpful2021-10-26T21:59:09ZMichael Soegtropopam package description is not helpfulThe package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_l...The package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
```
The description should more elaborate on the question what this can be used for.
See (https://coq.inria.fr/opam/released/packages/coq-iris/coq-iris.3.4.0/opam)
See (https://coq.inria.fr/opam/released/packages/coq-iris-heap-lang/coq-iris-heap-lang.3.4.0/opam)
Please note that (afaik) it is no issue to change the description of opam packages without creating a new version.https://gitlab.mpi-sws.org/iris/iris/-/issues/435Please create a tag for Coq 8.14 in Coq Platform 2021.112021-11-14T18:33:05ZMichael SoegtropPlease create a tag for Coq 8.14 in Coq Platform 2021.11The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of di...The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.4.0) does not work with Coq 8.14+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
ee6a36b3e803ebec465bf44bb5bcbf9b19fe6b62 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag, or communicate us any existing tag that works with Coq branch v8.14, preferably before November 15, 2021?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/139https://gitlab.mpi-sws.org/iris/iris/-/issues/432iApply "auto frame": bad error message2021-09-06T06:47:59ZRalf Jungjung@mpi-sws.orgiApply "auto frame": bad error messageThe following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable t...The following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable tactic.
```
There is a `fail "iSpecialize: premise cannot be solved by framing"` in the tactic code but that does not seem to work.https://gitlab.mpi-sws.org/iris/iris/-/issues/430iInduction does not work well for induction principles involving `Forall`2022-02-11T10:28:24ZRalf Jungjung@mpi-sws.orgiInduction does not work well for induction principles involving `Forall`Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind...Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind`, where `expr_ind` is a custom induction principle that uses `Forall` to handle nested lists.
Here's a self-contained testcase:
```coq
Inductive tree (T : Type) := Tree : list (tree T) → tree T.
Arguments Tree {T}.
Lemma tree_ind' T (P : tree T → Prop) :
(∀ l, Forall P l → P (Tree l)) →
∀ t, P t.
Proof.
intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
induction l as [|t l IH].
{ constructor. }
constructor; last apply IH.
apply REC.
Qed.
Lemma test_iInduction_Forall (t : tree nat) (P : PROP) : ⊢ P.
Proof. iInduction t as [] "IH" using tree_ind'.
```
This shows a goal
```
PROP : bi
l : list (tree nat)
P : PROP
============================
"IH" : <pers> ?P
--------------------------------------□
P
```
An `unshelve` shows that the `IntoIH` simply was not resolved, which seems like a bug in its own right -- `iInduction` should fail in that case.
In fact this testcase is interesting in the sense that even adding the instance from Simuliris (even after getting rid of the `BiAffine` assumption) does not help:
```coq
Section tactics.
Import iris.bi.bi.
Import iris.proofmode.base environments classes modality_instances.
Import bi.
Import env_notations.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
Import coq_tactics.
Local Instance into_ih_Forall {A} (φ : A → Prop) (l : list A) Δ Φ :
(∀ x, x ∈ l → IntoIH (φ x) Δ (Φ x)) → IntoIH (Forall φ l) Δ (∀ x, ⌜x ∈ l⌝ → Φ x) | 2.
Proof.
rewrite /IntoIH Forall_forall => HΔ Hf. apply forall_intro=> x.
iIntros "Henv %Hl". iApply (HΔ with "Henv"); eauto.
Qed.
End tactics.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/421Bad error message for failing iInduction2021-06-14T13:59:19ZRalf Jungjung@mpi-sws.orgBad error message for failing iInductionI am not sure what is going wrong with the following `iInduction`, and IPM's error doesn't tell me:
```
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t...I am not sure what is going wrong with the following `iInduction`, and IPM's error doesn't tell me:
```
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t v_s :
val_rel v_t v_s -∗ True.
Proof. iInduction v_t as [| |] "IH" forall v_s.
(* Error: No matching clauses for match. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/414Tracking issue for monotone RA2023-09-11T07:41:21ZRalf Jungjung@mpi-sws.orgTracking issue for monotone RAThis is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open iss...This is the tracking issue for the "monotone" RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/597. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* How should the RA be called? `monotone` is a very general term, it would be good to find something more specific. Currently it is called `mra` which is short but cryptic. `principal` should then likely become `mra_principal` and all lemmas be prefixed with `mra` as well.
* Do a solid review of the API surface.
Cc @amintimany @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/409Proposed change to naming convention for "dataful" `*G`s2021-06-03T09:08:26ZRalf Jungjung@mpi-sws.orgProposed change to naming convention for "dataful" `*G`sSome of our `*G` typeclasses are different than others: they contain not just `inG` but actual relevant data; usually a `gname` but in the case of `irisG` also some further information about how the Iris program logic is being instantiat...Some of our `*G` typeclasses are different than others: they contain not just `inG` but actual relevant data; usually a `gname` but in the case of `irisG` also some further information about how the Iris program logic is being instantiated. These dataful classes come with a `*PreG` that represent their `inG` (dataless) part.
Dataful `*G`s need to be treated differently, e.g. they have special initialization lemmas and they should not be bundled in library's `*G` as that leads to duplication of said data. So I propose to adjust our naming convention such that one can tell from the name whether a `*G` is dataful or not.
The new naming convention is up for bikeshedding; here are some proposals coming to my mind:
1. We call the dataful class `*DataG` and its `inG`-only part `*G`. So e.g. `heapG` → `heapDataG` and `heapPreG` → `heapG`.
2. We call the dataful class `*DataG` and its `inG`-only part `*PreG`. So e.g. `heapG` → `heapDataG`; `heapPreG` stays.
2. We call the dataful class `*DG` and its `inG`-only part `*PreG`. So e.g. `heapG` → `heapDG`; `heapPreG` stays.
I think I prefer (2) or (3) over (1) because it prevents confusion due to accidentally using the `inG`-only part, and also because it is easier for migration since we don't reuse an old name for a different purpose.
@robbertkrebbers @tchajed @jtassaro what do you think?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/408bi.weakestpre imports a module from program_logic2021-06-18T13:09:56ZRalf Jungjung@mpi-sws.orgbi.weakestpre imports a module from program_logic`bi.weakestpre` imports `program_logic.language`, which is a layering violation. We should somehow fix this, either by breaking the dependency or by moving one of the two modules to the other side.`bi.weakestpre` imports `program_logic.language`, which is a layering violation. We should somehow fix this, either by breaking the dependency or by moving one of the two modules to the other side.https://gitlab.mpi-sws.org/iris/iris/-/issues/401wp_bind does not report a failure message2021-03-05T17:25:13ZTej Chajedtchajed@gmail.comwp_bind does not report a failure messageThe `first [ t1 | fail ]` here is incorrect: https://gitlab.mpi-sws.org/iris/iris/-/blob/4c96a5043ab4f648f4082f2398888c879efd3c36/iris_heap_lang/proofmode.v#L200
```coq
first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind...The `first [ t1 | fail ]` here is incorrect: https://gitlab.mpi-sws.org/iris/iris/-/blob/4c96a5043ab4f648f4082f2398888c879efd3c36/iris_heap_lang/proofmode.v#L200
```coq
first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
| fail "wp_bind: cannot find" efoc "in" e ]
```
The failure causes the entire construct to fail with a generic error message; what was intended is `fail 1` to bubble it up. Furthermore there's no test of this failure.
This bug was originally reported by François Pottier against https://github.com/tchajed/iris-simp-lang/, which inherited this bug from heap_lang.Tej Chajedtchajed@gmail.comTej Chajedtchajed@gmail.comhttps://gitlab.mpi-sws.org/iris/iris/-/issues/395Generalize frac to dfrac in view camera2021-03-03T16:01:46ZSimon Friis VindumGeneralize frac to dfrac in view cameraThe use of `frac` in the view camera could be generalized to `dfrac`. This would make it possible to "freeze" or persist the authorative element. I don't have a use case for this myself, but, if I recall correctly, @jung or @tchajed had ...The use of `frac` in the view camera could be generalized to `dfrac`. This would make it possible to "freeze" or persist the authorative element. I don't have a use case for this myself, but, if I recall correctly, @jung or @tchajed had one?
The notation would be the same as for the points-to predicate, and in the future the custom entries `dfrac` notation could be reused for this. The view camera is rather new, so breaking changes here are less critical, and it thus seems like a fine place to start with regards to trying to use `dfrac` more.
What do you think? I'd like to work on this if there is support.https://gitlab.mpi-sws.org/iris/iris/-/issues/393fupd_plainly_laterN = fupd_plain_laterN ?2020-12-23T11:12:46ZPaolo G. Giarrussofupd_plainly_laterN = fupd_plain_laterN ?It seems `fupd_plainly_laterN` is a misnamed copy of `fupd_plain_laterN`. I confirmed this by giving the following proof to the existing statement:
```coq
Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
(▷^n |={E}=> P) ⊢ |={...It seems `fupd_plainly_laterN` is a misnamed copy of `fupd_plain_laterN`. I confirmed this by giving the following proof to the existing statement:
```coq
Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
(▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
Proof. exact: fupd_plain_laterN. Qed.
```
I'm happy to leave the fix to anybody else.https://gitlab.mpi-sws.org/iris/iris/-/issues/387Deprecate unqualified "Instance"2020-12-19T17:43:58ZRalf Jungjung@mpi-sws.orgDeprecate unqualified "Instance"With https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594 (and potentially some follow-up changes), all `Hint` in Iris will be qualified with `Local` or `Global`. I think we should do the same with `Instance`.
@tchajed is there a w...With https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/594 (and potentially some follow-up changes), all `Hint` in Iris will be qualified with `Local` or `Global`. I think we should do the same with `Instance`.
@tchajed is there a way to adjust your script to do that, or will we have to ask the Coq devs for an (opt-in) deprecation warning for `Instance` first, similar to the `Hint` warning that your script is based on?https://gitlab.mpi-sws.org/iris/iris/-/issues/378Graveyard for obsolete code2021-06-02T22:38:25ZRobbert KrebbersGraveyard for obsolete codeThere is some obsolete code in Iris, like Hoare triples, view shifts, STS, the logic-level wrapper for auth, that have bit rot quite a bit and should basically never be used by end-users.
Since this code supports some claims in papers, ...There is some obsolete code in Iris, like Hoare triples, view shifts, STS, the logic-level wrapper for auth, that have bit rot quite a bit and should basically never be used by end-users.
Since this code supports some claims in papers, it might be useful to keep it in some form. But what would be the best place?https://gitlab.mpi-sws.org/iris/iris/-/issues/373Quote does not handle ⊣⊢2020-11-05T11:12:30ZRodolphe LepigreQuote does not handle ⊣⊢The `solve_sep_equiv` tactic from `bi.tactics` cannot be used to solve goals of the form `_ ⊣⊢ _`.
This is due to `quote` only accepting goals of the form `_ ⊢ _` (see [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/b...The `solve_sep_equiv` tactic from `bi.tactics` cannot be used to solve goals of the form `_ ⊣⊢ _`.
This is due to `quote` only accepting goals of the form `_ ⊢ _` (see [here](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/tactics.v#L136)). Can it be made more general?https://gitlab.mpi-sws.org/iris/iris/-/issues/370Add missing instances for `Duplicable` and fix `Hint Immediate` for `persiste...2020-11-04T12:05:50ZSimon Friis VindumAdd missing instances for `Duplicable` and fix `Hint Immediate` for `persistent_duplicable`Following the merge of !481 instances of `Duplicable` for `<subj>` and `embed` should be added.
@robbertkrebbers has kindly offered to do this.Following the merge of !481 instances of `Duplicable` for `<subj>` and `embed` should be added.
@robbertkrebbers has kindly offered to do this.https://gitlab.mpi-sws.org/iris/iris/-/issues/363Collect Iris versions required by artifacts2020-11-23T12:56:33ZRalf Jungjung@mpi-sws.orgCollect Iris versions required by artifactsI'd like to clean up https://gitlab.mpi-sws.org/iris/opam, to avoid opam issues due to having too many versions of a package. However, it turns out in the past some of the Iris paper artifacts are not self-contained, and instead rely on ...I'd like to clean up https://gitlab.mpi-sws.org/iris/opam, to avoid opam issues due to having too many versions of a package. However, it turns out in the past some of the Iris paper artifacts are not self-contained, and instead rely on the opam repository. We should figure out which versions of Iris are required by an artifact, and keep them in the repository.https://gitlab.mpi-sws.org/iris/iris/-/issues/361gen_heap: provide init lemma for non-empty heap that provides the points-to f...2020-11-10T18:03:57ZRalf Jungjung@mpi-sws.orggen_heap: provide init lemma for non-empty heap that provides the points-to factsOur current `gen_heap_init` can be used with a non-empty heap, but then the points-to facts for the initial location are lost. Sometimes however they are needed: both Perennial and time-credits violate the gen_heap abstraction to be able...Our current `gen_heap_init` can be used with a non-empty heap, but then the points-to facts for the initial location are lost. Sometimes however they are needed: both Perennial and time-credits violate the gen_heap abstraction to be able to initialize with a non-empty heap and obtain all the points-to facts.
We should just provide a lemma for this. However, this is blocked on `gmap_view` having such a lemma, which requires having "map fragments" besides the currently available "singleton fragments".https://gitlab.mpi-sws.org/iris/iris/-/issues/358Add a logic-level version of gmap_view2021-03-06T11:34:41ZRalf Jungjung@mpi-sws.orgAdd a logic-level version of gmap_viewWe now have `gmap_view` on the RA level, but this library seems useful enough that we want to have a logic-level wrapper as well, with notations for "owning a location in a ghost heap", so to speak. Perennial has `auth_map` (and some pre...We now have `gmap_view` on the RA level, but this library seems useful enough that we want to have a logic-level wrapper as well, with notations for "owning a location in a ghost heap", so to speak. Perennial has `auth_map` (and some predecessors) for this and it is used all over the place.https://gitlab.mpi-sws.org/iris/iris/-/issues/356gmap_view: add fraction support to gmap_view_auth2020-10-21T10:09:04ZRalf Jungjung@mpi-sws.orggmap_view: add fraction support to gmap_view_authTo fully supplement Perennial's `auth_map`, we need to equip `gmap_view_auth` with support for a fraction. `view` already supports fractions so this should not be too hard.To fully supplement Perennial's `auth_map`, we need to equip `gmap_view_auth` with support for a fraction. `view` already supports fractions so this should not be too hard.