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/407Tracking issue for list RA2021-03-17T11:50:01ZRalf Jungjung@mpi-sws.orgTracking issue for list RAThis is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper....This is the tracking issue for the list RA that went to staging in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/654. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* The laws of the list camera are kind of weird, because it's very awkward to deal with "holes" in the list, which typically occurs when separating ghost state.
* Is the list RA ever actually needed, or can we replace it by `gmap` + `map_seq`? That deals better with "holes", but [lacks some closure properties](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/371#note_62685) that can sometimes be useful.https://gitlab.mpi-sws.org/iris/iris/-/issues/406Slow typechecking / nonterminating Qed when using auxiliary definitions in RAs2021-03-18T08:26:06ZArmaël GuéneauSlow typechecking / nonterminating Qed when using auxiliary definitions in RAs```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Defin...```coq
From iris.base_logic Require Export invariants gen_heap.
From iris.program_logic Require Export weakestpre ectx_lifting.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac auth gmap excl list.
Definition memspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition regspecUR : ucmraT :=
gmapUR nat (prodR fracR (agreeR (leibnizO nat))).
Definition memreg_specUR := prodUR regspecUR memspecUR.
Definition exprUR : cmraT := (exclR (leibnizO nat)).
Definition cfgUR : ucmraT := prodUR (optionUR exprUR) memreg_specUR.
Class cfgSG Σ := CFGSG {
cfg_invG :> inG Σ (authR cfgUR);
cfg_name : gname }.
Section S.
Context `{cfgSG Σ}.
Lemma spec_heap_valid (e:option (excl (leibnizO nat))) a q w
(rm: gmapUR nat (prodR fracR (agreeR (leibnizO nat))))
(mm: gmapUR nat (prodR fracR (agreeR (leibnizO nat)))) :
False →
own cfg_name (● (e,(rm,mm))) ∗
own cfg_name (◯ (ε, (∅,{[ a := (q, to_agree w) ]})))
-∗ False.
Proof. intro.
iIntros "(Hown & Ha)".
iDestruct (own_valid_2 with "Hown Ha") as "HH". exfalso. assumption.
Qed.
End S.
```
The snippet above:
- works fine with Iris 3.3
- takes a very long time at Qed with Iris 3.4 (modulo replacing `cmraT` with `cmra` in the script)
The issue seems to be with the use of auxiliary definitions to define the resource algebra `cfgUR`. Manually inlining `cfgUR` and the other auxiliary definitions in the definition of `cfgSG` makes it work again with Iris 3.4.
Since the fix is relatively simple, this issue doesn't seem to be too big of a deal, but I thought that I'd report it just in case.
Coq version used: 8.12.1 in both cases.https://gitlab.mpi-sws.org/iris/iris/-/issues/405Tracking issue for HeapLang interpreter2021-02-16T11:03:04ZRalf Jungjung@mpi-sws.orgTracking issue for HeapLang interpreterThis is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
...This is the tracking issue for the HeapLang interpreter added in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/564. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Generalize the monad and move it to std++, and generalize the tactics for the monad.
* Find some way to avoid the `pretty_string` instance, or move it to std++.https://gitlab.mpi-sws.org/iris/iris/-/issues/404Make string-ident a standard part of Iris2021-03-24T11:03:52ZLennard Gähergaeher@mpi-sws.orgMake string-ident a standard part of IrisSince support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this w...Since support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this would have the benefits of
* not having to explicitly require the user to install the plugin in developments using Iris,
* and thus be beneficial to overall code quality of developments using Iris (since there would be a clear argument for using the new intro pattern instead of using auto-generated names).
@jung suggested I create an issue for this.https://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/402iFrame performance issues2022-05-06T12:56:32ZRalf Jungjung@mpi-sws.orgiFrame performance issuesThere are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into ...There are some situations where iFrame is rather slow.
- For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
- Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
- Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.
- https://gitlab.mpi-sws.org/iris/iris/-/issues/434 for diverging iFrame because Hint Mode is accidentally being circumvented.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/400Integrate Tej's simp-lang?2021-02-17T08:49:46ZRalf Jungjung@mpi-sws.orgIntegrate Tej's simp-lang?@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04...@tchajed has created https://github.com/tchajed/iris-simp-lang, which is a simple "demo language" to show how to use the Iris language interface. It even comes with an [accompanying Youtube video](https://www.youtube.com/watch?v=HndwyM04KEU&feature=youtu.be)! I took a look and watched the video, and I really like it.
I propose we give this more visibility by referencing it from the Iris repo and website, and also we should find some way to ensure that the Coq code remains compatible with latest Iris. The easiest way to do that would be to add an "iris_simp_lang" package in this repository and move the code there. The README could go into the subfolder. @tchajed would that work for you, or did you have other plans? I don't want to appropriate your work, just ensure that it does not bitrot. I could imagine declaring you the maintainer of that subdirectory, so you could e.g. merge MRs for it yourself. @robbertkrebbers what do you think?
I also have some more specific low-level comments, which I leave here just so I do not forget -- but it probably make more sense to discuss the high-level points first. It's really just one remark so far:
* In `heap_ra`, I find it confusing that you end up basically copying (parts of) `gen_heap`. IMO it would make more sense to either use `gen_heap`, or else (for the purpose of exposition) to define something that specifically works for values and locations of this language, but then it should not be called "gen(eral)".https://gitlab.mpi-sws.org/iris/iris/-/issues/399Upstream more big_op lemmas from Perennial2021-02-17T08:49:05ZRalf Jungjung@mpi-sws.orgUpstream more big_op lemmas from PerennialPerennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.Perennial has a bunch of big_op lemmas at <https://github.com/mit-pdos/perennial/tree/master/src/algebra/big_op>. At least some of those are certainly worth upstreaming, but I find it hard to figure out where to draw the line.https://gitlab.mpi-sws.org/iris/iris/-/issues/398Use `dom` instead of `∀ k, is_Some (.. !! k) ...`2021-02-17T08:48:46ZRobbert KrebbersUse `dom` instead of `∀ k, is_Some (.. !! k) ...`See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas...See for example `big_sepM_sep_zip_with`, `big_sepM_sep_zip`, `big_sepM2_intuitionistically_forall`, `big_sepM2_forall`.
The version with `dom` is more intuitive, and likely easier to prove because one can reason equationally with lemmas for `dom`. However, the fact that the set (here `gset`) has to specified explicitly might be annoying.
Note that if we perform this change, there are also some lemmas in std++ that need to be changed.https://gitlab.mpi-sws.org/iris/iris/-/issues/397`iRename` fails with bad error message when not in proof mode2021-02-17T08:48:22ZRobbert Krebbers`iRename` fails with bad error message when not in proof mode```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
wit...```coq
Lemma silly : True.
Proof.
iRename "H" into "H".
```
fails with
```
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11770)
(environments.env_spatial ?M11770) ?M11775"
with "True".
```
The tactic probably does not call `iStartProof` at the beginning.https://gitlab.mpi-sws.org/iris/iris/-/issues/396Intro pattern `>` has wrong behavior with side-conditions of `iMod`2021-04-29T09:25:46ZRobbert KrebbersIntro pattern `>` has wrong behavior with side-conditions of `iMod````coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> ...```coq
Section atomic.
Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
(* These tests check if a side-condition for [Atomic] is generated *)
Check "wp_iMod_fupd_atomic".
Lemma wp_iMod_fupd_atomic E1 E2 P :
(|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
Proof.
iIntros ">H".
```
fails with
```
In environment
Σ : gFunctors
heapG0 : heapG Σ
E1, E2 : coPset
P : iProp Σ
Unable to unify
"unseal environments.pre_envs_entails_aux ?PROP (environments.env_intuitionistic ?M11809)
(environments.env_spatial ?M11809) ?M11814"
with
"∀ (σ : language.state heap_lang) (e' : language.expr heap_lang) (κ :
list
(language.observation
heap_lang))
(σ' : language.state heap_lang) (efs : list (language.expr heap_lang)),
language.prim_step (#() #()) σ κ e' σ' efs
→ match stuckness_to_atomicity NotStuck with
| StronglyAtomic => is_Some (language.to_val e')
| WeaklyAtomic => irreducible e' σ'
end".
```
See also https://mattermost.mpi-sws.org/iris/pl/r47q3gcq4fddxnhpddj91yb1wyhttps://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/394Document relation between Discrete and Timeless (in appendix?)2021-01-06T13:08:34ZPaolo G. GiarrussoDocument relation between Discrete and Timeless (in appendix?)See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not s...See discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/607#note_61127 by @robbertkrebbers:
> I also wondered about this a long time ago and came to the same conclusion as you: Discrete P → Timeless P holds, but is not so useful; Timeless P → Discrete P does not hold; discrete propositions are unlikely to exist.
> It might be worth documenting this somewhere, but I don't know what's the best place. Maybe the appendix?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/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gi...Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/391Add append-only list RA to Iris2021-05-17T16:32:27ZRalf Jungjung@mpi-sws.orgAdd append-only list RA to IrisAppend-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize l...Append-only lists are probably the most often requested RA that is not available in Iris. This is a special case of https://gitlab.mpi-sws.org/iris/iris/-/issues/244, that (a) can be landed without having to figure out how to formalize lattices in general, and (b) would probably be a useful dedicated abstraction even if we get general lattices one day.
@haidang wrote [a version of this](https://gitlab.mpi-sws.org/iris/gpfsl/-/blob/graphs/theories/examples/list_cmra.v), which was forked at some point by @jtassaro [for Perennial](https://github.com/jtassarotti/iris-inv-hierarchy/blob/fupd-split-level/iris/algebra/mlist.v) while also adding a logic-level wrapper for `auth (mlist T)` with the following three core assertions:
* authoritative ownership of the full trace
* persistent ownership that some list is a prefix of the trace
* persistent ownership that index i in the trace has some particular value
Perennial also has [another version of this](https://github.com/mit-pdos/perennial/blob/master/src/algebra/append_list.v) by @tchajed that is based on (the Perennial version of) `gmap_view`. And finally, @msammler has [his own implementation](https://gitlab.mpi-sws.org/FCS/lang-sandbox-coq/-/blob/master/theories/lang/heap.v#L18) that is based on the list RA.
I do not have a strong preference for which approach to use for the version in Iris, but we should probably look at all of them to figure out what kinds of lemmas people need for this.Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/iris/-/issues/389Citation guide2020-12-08T17:17:32ZTej Chajedtchajed@gmail.comCitation guideThe docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.The docs should have a page explaining what a paper using Iris should cite, between the several Iris papers, the journal paper, and the two IPM papers.https://gitlab.mpi-sws.org/iris/iris/-/issues/388Dropping support for Coq 8.102020-12-16T12:17:28ZTej Chajedtchajed@gmail.comDropping support for Coq 8.10At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the `"%H"` intro pattern wi...At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the `"%H"` intro pattern without any additional work from the user.
- Custom entries [had some bugs](https://github.com/coq/coq/pull/11530) that seem to block their use in !554; in Coq 8.11 and forward we can give good notation for dfracs.
We should probably release Iris 3.4 before dropping support. Before that out of the current MRs I think !572 is the most important, to avoid releasing the mnat library and then immediately renaming it.