Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-10-27T11:54:07Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/488Move iris.sty towards being a community standard2022-10-27T11:54:07ZJonas KastbergMove iris.sty towards being a community standardMy impression is that there a multiple people who take inspiration from the `iris.sty` file
when writing papers about Iris.
For one, we use (a variant of) it in the Iris Lecture Notes (Soon to be publicly available).
I find that it would...My impression is that there a multiple people who take inspiration from the `iris.sty` file
when writing papers about Iris.
For one, we use (a variant of) it in the Iris Lecture Notes (Soon to be publicly available).
I find that it would be beneficial to have a "community standard" for this collection of macros,
to guarantee that notation is uniform throughout Iris papers (while of course authors should be free to diverge from the standard as need be).
To achieve this the style-file should be kept up to date with changing notation, terminiology, etc.
While good effort has already been put towards this, I find that more improvements could be made,
e.g. by reviewing the current file on terms such as:
- Completeness of the macro set (For one there is currently no `\pointsto`)
- Names of the macros (For one `\always` seem outdated in terms of the current "persistently" terminology)
- Notation of the macros
- Formatting of macros (kerning, squashing, etc.)
The merge request !851 is an attempt at an initial step in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/487Adding pointer order comparison to HeapLang2022-10-14T19:33:59ZArthur Azevedo de AmorimAdding pointer order comparison to HeapLangAs the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4...As the following file shows, HeapLang makes it possible to compare pointers for their relative ordering. Should we extend the primitive comparison operation on HeapLang to work on pointers as well?
[pointer_comparison.v](/uploads/f638e4e4e81b856b5be629e623fe608f/pointer_comparison.v)https://gitlab.mpi-sws.org/iris/iris/-/issues/441Upstream later credits2022-10-14T16:34:37ZRalf Jungjung@mpi-sws.orgUpstream later credits@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I k...@robbertkrebbers and me seem to agree that having @simonspies's later credits in Iris proper would be great, but there are still a lot of details to be worked out. Let's use this issue to collect relevant information.
In particular, I keep forgetting what exactly are the `fupd` laws that we would lose by doing this, so maybe we can put that here. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/490Move heaplang.sty towards being a community standard2022-10-14T13:38:49ZJonas KastbergMove heaplang.sty towards being a community standardSimilarly to #488 I believe it is beneficial to more carefully curate the `heaplang.sty` file contained in this repository.
Some immediate considerations that might make sense to review are:
- The notion-style supported by the language ...Similarly to #488 I believe it is beneficial to more carefully curate the `heaplang.sty` file contained in this repository.
Some immediate considerations that might make sense to review are:
- The notion-style supported by the language macros - e.g. parentheses vs spaces for function arguments
- The naming of each macro, to avoid clashes with popular latex packages
- Discuss what similarities we want HeapLang to have with existing languages (formerly ML, but has since moved quite past it)
- Casing of constructs, both in Latex and notation. Currently we have discrepancies such as `ref` and `Alloc` even though they live on the same level. The latex macros are mostly consistent, with some outliers like `\poison` and `\fold` / `\unfold`
The MR's !852 and !853 are some initial steps in this direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/486make: warnings that egrep/fgrep are deprecated2022-10-07T08:41:13ZArmaël Guéneaumake: warnings that egrep/fgrep are deprecatedRunning `make` outputs a number of warnings indicating that using `egrep`/`fgrep` is deprecated:
```
fgrep: warning: fgrep is obsolescent; using grep -F
egrep: warning: egrep is obsolescent; using grep -E
[...]
```
This is when using (...Running `make` outputs a number of warnings indicating that using `egrep`/`fgrep` is deprecated:
```
fgrep: warning: fgrep is obsolescent; using grep -F
egrep: warning: egrep is obsolescent; using grep -E
[...]
```
This is when using (the recently released) GNU grep 3.8.https://gitlab.mpi-sws.org/iris/iris/-/issues/474Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.092022-09-06T13:36:55ZMichael SoegtropPlease pick the version you prefer for Coq 8.16 in Coq Platform 2022.09The Coq team released Coq `8.16+rc1` on June 01, 2022.
The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**.
It can be delayed in case of difficulties until October 15, 2022, but this should b...The Coq team released Coq `8.16+rc1` on June 01, 2022.
The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**.
It can be delayed in case of difficulties until October 15, 2022, but this should be an exception.
This issue is to inform you that the opam package we are currently testing in Coq Platform CI **works fine** with Coq `8.16+rc1`.
Coq Platform CI is currently testing opam package `coq-iris.3.6.0`
from platform patch repository https://github.com/coq/platform/tree/main/opam/opam-coq-archive/released/packages/coq-iris/coq-iris.3.6.0/opam. **This means we had to weaken some version restrictions in the opam package, but no other changes were required.**
**In case this is the version you want to see in Coq Platform, there is nothing to do for you - please just close this issue.**
In case you would prefer to see an updated or an older version in the upcoming Coq Platform `2022.09`, please inform us as soon as possible and before **August 31, 2022**!
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.16+rc1~2022.09~preview1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.16~2022.09~preview1.sh) which already supports Coq version `8.16+rc1` and contains already working (possibly patched / commit pinned) Coq Platform packages.
In case you want to select a different version, 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/274https://gitlab.mpi-sws.org/iris/iris/-/issues/478Adding satisfiable to Iris2022-08-17T05:24:37ZSimon SpiesAdding satisfiable to IrisSeveral Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notio...Several Iris projects have structured their adequacy proofs using the notion of a "`satisfiable`-proposition" (instead of following the current adequacy setup of the weakest precondition). It could be interesting to see whether the notion of `satisfiable` can be added to Iris in a meaningful way and whether it can enable more modular adequacy proofs in the future.https://gitlab.mpi-sws.org/iris/iris/-/issues/476Have `known_make_absorbingly` and `make_absorbingly_default` instances in the...2022-08-15T14:17:18ZRalf Jungjung@mpi-sws.orgHave `known_make_absorbingly` and `make_absorbingly_default` instances in the same fileThe following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instan...The following discussion from !842 should be addressed:
> This makes me think, it's a bit annoying that the default instance and `known_make_absorbingly` are not at the same place. Could we somehow refactor that? Move the default instances to `classes_make`, or move the other one here?https://gitlab.mpi-sws.org/iris/iris/-/issues/475Provide some way to "seal" a BI2022-08-12T14:53:14ZRalf Jungjung@mpi-sws.orgProvide some way to "seal" a BIOne reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms i...One reason why GPFSL and Iron are slower might be that their BI is bigger -- it is constructed via a combinator on top of iProp. So whenever the proof mode needs to query some property of the BI, there is one extra step, and also terms in general are just bigger.
It might be worth investigating some nice way to seal a BI (but that would probably have to be a macro):
- either lightweight sealing by just making it TC opaque and forwarding all instances
- or a proper seal that makes terms no convertible any more, and a *lot* of forwarding of things
We *do* seal `iProp` pretty heavily (in fact even more proper than the "proper" seal, this is the one place where we use a module type for sealing to be *really sure*), so Iris itself doesn't have this problem.
@robbertkrebbers IIRC you did an experiment along the lines of doing that by hand once? What were the results of that again?https://gitlab.mpi-sws.org/iris/iris/-/issues/303Canonical structures have major performance impact2022-08-12T14:48:02ZRobbert KrebbersCanonical structures have major performance impactAs I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and ...As I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.https://gitlab.mpi-sws.org/iris/iris/-/issues/472Rename laterN_plus into laterN_add2022-08-09T21:19:10ZRobbert KrebbersRename laterN_plus into laterN_addThe following discussion from !808 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/808#note_82564): (+1 comment)
> Hmm, we already have:
>
> ```
...The following discussion from !808 should be addressed:
- [ ] @robbertkrebbers started a [discussion](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/808#note_82564): (+1 comment)
> Hmm, we already have:
>
> ```
> Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
> ```
>
> So, with plus instead of add.
>
> Since the new convention in Coq is to use add, maybe the laterN lemma should be renamed?https://gitlab.mpi-sws.org/iris/iris/-/issues/417Revert !118: Use ∃ instead of SIgma for extension axiom2022-08-02T16:52:12ZRobbert KrebbersRevert !118: Use ∃ instead of SIgma for extension axiomI am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet ...I am trying to define a camera for general multisets, so multisets where the types can be an arbitrary OFE instead of a countable type (as for `gmultiset`).
The approach I'm following is to define:
```coq
Record multiset A := MultiSet { multiset_car : list A }.
```
And define `dist` and `(≡)` to be modulo permutations. For permutations I use https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.SetoidPermutation.html
Unfortunately, this does not work: the extension axiom of cameras does not seem provable.
```coq
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
```
The problem is that I need to construct `z1` and `z2` as a sigma type, not an ordinary exist. But the type of permutations is a `Prop`, so I cannot do this.
Here's the whole code I have so far:
```coq
From Coq Require Import SetoidPermutation.
From iris.algebra Require Export cmra.
Lemma PermutationA_mono {A} (R1 R2 : relation A) xs1 xs2 :
(∀ x1 x2, R1 x1 x2 → R2 x1 x2) →
PermutationA R1 xs1 xs2 → PermutationA R2 xs1 xs2.
Proof. induction 2; econstructor; by eauto. Qed.
Record multiset A := MultiSet { multiset_car : list A }.
Arguments MultiSet {_} _.
Arguments multiset_car {_} _.
Section multiset.
Context {A : ofe}.
Implicit Types x y : A.
Implicit Types X Y : multiset A.
Local Instance multiset_equiv_instance : Equiv (multiset A) := λ X1 X2,
∀ n, PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_dist_instance : Dist (multiset A) := λ n X1 X2,
PermutationA (≡{n}≡) (multiset_car X1) (multiset_car X2).
Local Instance multiset_valid_instance : Valid (multiset A) := λ _, True.
Local Instance multiset_validN_instance : ValidN (multiset A) := λ _ _, True.
Local Instance multiset_unit_instance : Unit (multiset A) := MultiSet [].
Local Instance multiset_op_instance : Op (multiset A) := λ X1 X2,
MultiSet (multiset_car X1 ++ multiset_car X2).
Local Instance multiset_pcore_instance : PCore (multiset A) := λ X, Some ε.
Global Instance multiset_singleton : Singleton A (multiset A) := λ x,
MultiSet [x].
Lemma multiset_ofe_mixin : OfeMixin (multiset A).
Proof.
split; rewrite /equiv /dist /multiset_equiv_instance /multiset_dist_instance /=.
- done.
- intros n. split.
+ by intros X.
+ intros X1 X2 ?. done.
+ intros X1 X2 X3 ??. by etrans.
- intros n X1 X2. apply PermutationA_mono, dist_S.
Qed.
Canonical Structure multisetO := Ofe (multiset A) multiset_ofe_mixin.
Global Instance multiset_ofe_discrete : OfeDiscrete A → OfeDiscrete multisetO.
Proof.
intros HA [xs1] [xs2] Hxs n. revert Hxs. apply PermutationA_mono.
by intros x1 x2 ->%(discrete _).
Qed.
Lemma multiset_cmra_mixin : CmraMixin (multiset A).
Proof.
apply cmra_total_mixin; try by eauto.
- intros X n Y1 Y2 HY. by apply (PermutationA_app _).
- by intros n X1 X2.
- intros X1 X2 X3. admit. (* boring case *)
- intros X1 X2 n. apply (PermutationA_app_comm _).
- by intros X n.
- intros X1 X2 _. exists ε. by intros n.
- intros n [xs] [ys1] [ys2] _. rewrite /equiv /dist /op
/multiset_equiv_instance /multiset_dist_instance /multiset_op_instance /=.
(* Stuck here. The witness [PermutationA (dist n) xs (ys1 ++ ys2)] basically
says how the elements in [xs] are distributed over [ys1] and [ys2].
Intuitively, it says element 0 of [xs] goes to position [i0] in
[ys1 ++ ys2], element 1 of [xs] goes to position [i1] in ys1 ++ ys2 and so
on. *)
(* I would like to use the lemma [PermutationA_decompose], but that does
not work since it gives an [∃]. *)
(* I tried to prove it by induction on the list instead, but that seems
pointless. At some point I need to invert on the [PermutationA] witness,
which is not possible. *)
induction ys1 as [|y1 ys1 IH]; intros Hxs; simpl in *.
{ by exists (MultiSet []), (MultiSet xs). }
admit.
Admitted.
Canonical Structure multisetR := Cmra (multiset A) multiset_cmra_mixin.
Lemma multiset_ucmra_mixin : UcmraMixin (multiset A).
Proof. split; [done | | done]. by intros X n. Qed.
Canonical Structure multisetUR := Ucmra (multiset A) multiset_ucmra_mixin.
Global Instance multiset_cancelable X : Cancelable X.
Proof. Admitted.
Global Instance multiset_singleton_ne : NonExpansive (singleton (B:=multiset A)).
Proof. intros n x1 x2. by repeat constructor. Qed.
Global Instance multiset_singleton_proper :
Proper ((≡) ==> (≡)) (singleton (B:=multiset A)).
Proof. apply (ne_proper _). Qed.
Global Instance multiset_singleton_dist_inj n :
Inj (dist n) (dist n) (singleton (B:=multiset A)).
Proof. intros x1 x2. Admitted.
Global Instance multiset_singleton_inj :
Inj (≡) (≡) (singleton (B:=multiset A)).
Proof.
intros x1 x2 Hx. apply equiv_dist=> n. apply (inj singleton). by rewrite Hx.
Qed.
End multiset.
Global Arguments multisetO : clear implicits.
Global Arguments multisetR : clear implicits.
Global Arguments multisetUR : clear implicits.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/470Overeager simplification in 'iIntros' and 'iSplit'2022-07-19T15:06:26ZRalf Jungjung@mpi-sws.orgOvereager simplification in 'iIntros' and 'iSplit'Consider the following lemma:
```
Lemma lc_test n m :
£ (S n + m) -∗ £ (S n).
Proof.
iIntros "[Hlc1 Hlc2]".
```
I would expect the state after this script to be such that `Hlc1` is `£ (S n)`, such that `iExact "Hlc1"` finishe...Consider the following lemma:
```
Lemma lc_test n m :
£ (S n + m) -∗ £ (S n).
Proof.
iIntros "[Hlc1 Hlc2]".
```
I would expect the state after this script to be such that `Hlc1` is `£ (S n)`, such that `iExact "Hlc1"` finishes the proof. However, the state we actually get is this:
```
"Hlc1" : £ 1
"Hlc2" : £
((fix add (n0 m0 : nat) {struct n0} : nat :=
match n0 with
| 0 => m0
| S p => S (add p m0)
end) n m)
```
That is clearly terrible -- something in the IPM simplification machinery seems to be going wrong...
(The workaround is to `rewrite lc_split` so that simplification has no chance of kicking in.)https://gitlab.mpi-sws.org/iris/iris/-/issues/332Become part of Coq Platform?2022-07-15T12:06:16ZRalf 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/205Make notation for pure and plainly affine2022-06-12T19:28:08ZRalf 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/463Rename "head step"?2022-06-10T18:13:39ZRalf Jungjung@mpi-sws.orgRename "head step"?At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.At some point there was a discussion on Mattermost about people objecting to the term "head step" that we use in our HeapLang operational semantics. I think there were proposals for others names, but I forgot if there was any consensus.https://gitlab.mpi-sws.org/iris/iris/-/issues/461Universe problem: AU cannot use telescopes quantified at Iris level2022-06-08T13:45:51ZHai DangUniverse problem: AU cannot use telescopes quantified at Iris levelThis is a regression from `dev.2022-05-06.0.7b9f809f` to `dev.2022-05-06.1.1414d84`, by !781
The following snippet shows the problem. `AU_fail` is accepted in `dev.2022-05-06.0.7b9f809f` but not in `dev.2022-05-06.1.1414d84`.
I tried p...This is a regression from `dev.2022-05-06.0.7b9f809f` to `dev.2022-05-06.1.1414d84`, by !781
The following snippet shows the problem. `AU_fail` is accepted in `dev.2022-05-06.0.7b9f809f` but not in `dev.2022-05-06.1.1414d84`.
I tried putting `Unset Universe Minimization ToSet` in `bi.lib.atomic` as well as locally, but that didn't help.
```coq
Require Import stdpp.coPset.
Require Import iris.bi.telescopes.
Require Import iris.bi.lib.atomic.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
Definition AU_succeed (TA TB : tele) : Prop :=
⊢ ∀ (α : TA → PROP) (β Φ : TA → TB → PROP),
atomic_update Eo Ei α β Φ.
Fail Definition AU_fail : Prop :=
⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
atomic_update Eo Ei α β Φ.
End definition.
```
This is the error message:
```
In environment
PROP : bi
H : BiFUpd PROP
TA : tele
TB : tele
Eo, Ei : coPset
TA0 : tele
TB0 : tele
α : TA0 → PROP
β : TA0 → TB0 → PROP
Φ : TA0 → TB0 → PROP
The term "α" has type "forall _ : tele_arg@{tests.62} TA0, bi_car PROP"
while it is expected to have type
"forall _ : tele_arg@{iris.bi.lib.atomic.94} ?TA, bi_car ?PROP5".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/462iRewrite with a Coq-level equality gives bad error message2022-05-20T17:14:58ZRalf Jungjung@mpi-sws.orgiRewrite with a Coq-level equality gives bad error messageIn a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at le...In a lambdaRust proof, I tried `iRewrite tctx_hasty_val in "Ha''".`. I had forgotten that `iRewrite` is for internal equalities only. That shows this error:
```
Error: No matching clauses for match.
```
This error is always a bug, at least the tactic should tell me what is wrong. :)https://gitlab.mpi-sws.org/iris/iris/-/issues/369Document HeapLang2022-05-18T17:42:51ZRalf Jungjung@mpi-sws.orgDocument HeapLangThe HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently [my thesis](https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#figure.3.1) and the ["Future is Our...The HeapLang syntax, operational semantics, and lifted weakestpre rules should probably be stated in the Iris Documentation. Currently [my thesis](https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#figure.3.1) and the ["Future is Ours" paper](https://plv.mpi-sws.org/prophecies/paper.pdf#%5B%7B%22num%22%3A171%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C45.828%2C641.295%2Cnull%5D) describe overlapping but incomparable subsets of the operational semantics, and there are likely bits that are missing from both.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.