Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-06-18T13:09:56Zhttps://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@mit.eduwp_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@mit.eduTej Chajedtchajed@mit.eduhttps://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.https://gitlab.mpi-sws.org/iris/iris/-/issues/355Break dependency of algebra on base_logic2020-10-20T15:11:03ZRalf Jungjung@mpi-sws.orgBreak dependency of algebra on base_logicCurrently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separ...Currently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separating the base_logic and program_logic folders into a separate package, should we ever want to do that.
The plan is to instead add a file like `base_logic/algebra.v` and prove those lemmas there, thus fixing the dependency inversion.https://gitlab.mpi-sws.org/iris/iris/-/issues/353CHANGELOG should spell out what changed in auth due to views MR better2020-10-03T10:02:54ZTej Chajedtchajed@mit.eduCHANGELOG should spell out what changed in auth due to views MR better!516 makes some changes that aren't obvious. For example, `auth_validI` is gone because it used the projections, should now explicitly use `auth_auth_validI`, `auth_frag_validI`, or `auth_both_validI` as appropriate.!516 makes some changes that aren't obvious. For example, `auth_validI` is gone because it used the projections, should now explicitly use `auth_auth_validI`, `auth_frag_validI`, or `auth_both_validI` as appropriate.https://gitlab.mpi-sws.org/iris/iris/-/issues/346Typeclass inference fails to trigger.2020-09-21T18:08:44ZArthur Azevedo de AmorimTypeclass inference fails to trigger.I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap num...I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/345Check for `options.v` should only consider files in _CoqProject2020-09-12T10:10:58ZRobbert KrebbersCheck for `options.v` should only consider files in _CoqProjectNow if I have random files in my theories folder, `make` will give errors.Now if I have random files in my theories folder, `make` will give errors.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/344Set Default Goal Selector2020-11-10T19:12:02ZRalf Jungjung@mpi-sws.orgSet Default Goal SelectorAs a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.As a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.https://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/342Missing {u,}rFunctors and conversions2020-09-10T17:45:28ZPaolo G. GiarrussoMissing {u,}rFunctors and conversionsSome missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable throu...Some missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable through the above conversion, and @jung suggests that's an oversight; OTOH, that alerted me to a bug; I only needed it because I tried writing `GFunctor (gmapRF ...)`, which does not seem useful
- `listRF` does not exist (which I noticed while grepping)https://gitlab.mpi-sws.org/iris/iris/-/issues/337Weird automatically generated names2020-08-12T16:46:47ZRobbert KrebbersWeird automatically generated namesAfter @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatic...After @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatically generated hypothesis `x`.
```
1 subgoal
PROP : bi
x : True
______________________________________(1/1)
_ : ⌜0 = 0⌝
--------------------------------------□
True
```
I don't understand where the name `x` comes from, but it's very annoying. The `∃ _ : ..., ...` pattern is often used for `inG`, and the `inG` being called `x` is very annoying. It prevents one from using `x` for other variables.
Obviously, in this case I could use `iDestruct foo as (name_for_my_inG) "?"`, but I really don't want to name that hypothesis.