Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2024-03-24T14:54:23Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/569Add some sort of rule for `own ∧ own`2024-03-24T14:54:23ZRalf Jungjung@mpi-sws.orgAdd some sort of rule for `own ∧ own`The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v)...The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v).)
Amin suggested [something similar](https://mattermost.mpi-sws.org/iris/pl/tcsex43cn7d5ij5qwkk39ftd7h) a long time ago.
Not sure which formulation works best, but we should have something like that. :)
Whatever the rule is, it should be strong enough to prove things like
```
Lemma pointsto_and_sep (l1 l2:loc) (v1 v2:val) :
l1 ≠ l2 ->
l1 ↦ v1 ∧ l2 ↦ v2 -∗
l1 ↦ v1 ∗ l2 ↦ v2.
Lemma pointsto_and_eq l x y :
l ↦ x ∧ l ↦ y -∗ ⌜x = y⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/568[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-18T16:04:50ZRomain Tetley[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.0`.
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 appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
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.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
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/405https://gitlab.mpi-sws.org/iris/iris/-/issues/567[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-19T16:06:15ZRomain Tetley[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.0`.
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
7c5ce0d556f4e03f27ddc6463462bf4040f5103d 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 and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
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.
In case the tag and opam package are available before March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
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/405https://gitlab.mpi-sws.org/iris/iris/-/issues/566Frame instance for multiset union can interact badly with instantiating exist...2024-03-06T12:32:05ZIke MulderFrame instance for multiset union can interact badly with instantiating existential quantifiersThis is problematic:
```coq
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail ...This is problematic:
```coq
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail Timeout 2 iFrame "HP".
Abort.
End test.
```
This happens because there is the following frame instance for framing inside a multiset union:
```coq
Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
```
In our `multiset_problem` example, this instance will instantiate the evar `?X` with a union `?X1 ⊎ ?X2`. After two more steps, we encounter almost the same goal, and `Frame` instance search will loop.
The instances for `[∗ list]` do not suffer from this problem, since they are guarded by an `IsCons` or `IsApp` typeclass with proper `Hint Mode`s.
To fix this, we could use the same approach: guard `frame_big_sepMS_disj_union` with a new class `IsUnion`.
Encountered by @janno @lepigrehttps://gitlab.mpi-sws.org/iris/iris/-/issues/565Unsound instantiation of existentials by `iFrame` on persistent facts2024-03-05T17:01:36ZRodolphe LepigreUnsound instantiation of existentials by `iFrame` on persistent facts@janno and I found that the new support for existential instantiation in `iFrame` (from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Repr...@janno and I found that the new support for existential instantiation in `iFrame` (from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Reproducing example:
```coq
Require Import iris.bi.interface.
Require Import iris.proofmode.proofmode.
Goal ∀ (PROP : bi) (P : nat -> PROP),
□ P 0 ⊢ P 0 ∗ (∀ n : nat, P n -∗ ∃ n, P n ∗ ⌜n = 1⌝).
Proof.
iIntros (??) "#$".
(*
PROP : bi
P : nat → PROP
============================
_ : P 0
--------------------------------------□
∀ x : nat, P x -∗ ⌜0 = 1⌝
*)
Abort.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/564Make iFrame also instantiate telescopic existential quantifiers2024-02-19T09:40:25ZIke MulderMake iFrame also instantiate telescopic existential quantifiersFollow up on !1017: it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications `∃.. x`.
The initial attempt worked partly:
```
Global Instance frame_texist {TT : t...Follow up on !1017: it should be possible to extend the technique for instantiating existential quantifiers to also work on telescopic quantifications `∃.. x`.
The initial attempt worked partly:
```
Global Instance frame_texist {TT : tele@{bi.Quant}} p R (Φ : TT → PROP)
(C : tele@{bi.Quant}) (g : C → TT) (Ψ : C → PROP) Q :
(∀ c, FrameExistRequirements p R Φ (g c) (Ψ c)) →
TCCbnSimplTele (∃.. c, Ψ c)%I Q →
Frame p R (∃.. x, Φ x) Q.
Proof.
move=> H HQ. rewrite /FrameTExists /Frame (bi_texist_exist Φ).
by eapply frame_exist.
Qed.
```
but this turns a telescopic quantifier into a regular one whenever things get framed beneath it.
We did not yet figure out a nice way to fix this.https://gitlab.mpi-sws.org/iris/iris/-/issues/563Add QuickPersistent and use it in frame_impl (and maybe elsewhere)2024-03-02T09:13:20ZRalf Jungjung@mpi-sws.orgAdd QuickPersistent and use it in frame_impl (and maybe elsewhere)Generally in framing we try to avoid typeclasses that walk the entire term, like `Affine` or `Absorbing`. We have `Quick*` variants of these typeclasses instead.
However, we don't have `QuickPersistent`, and `frame_impl` uses `Persisten...Generally in framing we try to avoid typeclasses that walk the entire term, like `Affine` or `Absorbing`. We have `Quick*` variants of these typeclasses instead.
However, we don't have `QuickPersistent`, and `frame_impl` uses `Persistent`. We should fix that.https://gitlab.mpi-sws.org/iris/iris/-/issues/562Repeatedly failing `Affine` typeclass search can slow down `iFrame`2024-02-14T15:06:17ZIke MulderRepeatedly failing `Affine` typeclass search can slow down `iFrame`During patching iron for !1017, I ran into a situation similar to this (exaggerated to make effect more visible):
```
Lemma test_iFrame_affinely_3 P Q :
let i := 50 in (* controls amount of [Affine] searches *)
let j := 50 in (* con...During patching iron for !1017, I ran into a situation similar to this (exaggerated to make effect more visible):
```
Lemma test_iFrame_affinely_3 P Q :
let i := 50 in (* controls amount of [Affine] searches *)
let j := 50 in (* controls hardness of an individual [Affine] search*)
let rep :=
fun n R T =>
([∗ list] P ∈ ((repeat R n) ++ [T]), P)%I
in
rep j (<affine> Q) Q ⊢ rep i (<affine> P) (<affine> P) ∗ rep j (<affine> Q) Q.
Proof.
iIntros (i j rep) "Hrep".
time iFrame "Hrep". (* 3.2 seconds *)
Undo 1.
time (iSplitR; last iFrame). (* 0.005 seconds *)
Abort.
```
The problematic `Frame` instance is [`frame_affinely`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/proofmode/class_instances_frame.v?ref_type=heads#L202), which attempts to show that the framed hypothesis is `Affine` whenever the `<affine>` modality occurs in the goal. One possible solution is to replace the `Affine` condition with `QuickAffine` in `frame_affinely`:
```
Lemma frame_affinely_alt p R P Q Q' :
TCOr (TCEq p true) (classes_make.QuickAffine R) →
Frame p R P Q → classes_make.MakeAffinely Q Q' →
Frame p R (<affine> P) Q'. (* Default cost > 1 *)
Proof.
rewrite /classes_make.QuickAffine.
case; apply _.
Qed.
Remove Hints class_instances_frame.frame_affinely : typeclass_instances.
Existing Instance frame_affinely_alt.
(* speeds up the first iFrame to 0.3 seconds *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/561Use `#[local] field ::` to make `inG` instances local2024-02-05T17:23:10ZRobbert KrebbersUse `#[local] field ::` to make `inG` instances localNow that support for Coq 8.17 has been dropped, we can make use of `#[local] field ::` in `Class` declarations ~~which by default appears to be `Local`~~. This would be a better fix for https://gitlab.mpi-sws.org/iris/iris/-/merge_reques...Now that support for Coq 8.17 has been dropped, we can make use of `#[local] field ::` in `Class` declarations ~~which by default appears to be `Local`~~. This would be a better fix for https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/780
See also https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1030https://gitlab.mpi-sws.org/iris/iris/-/issues/560Fix the future-coercion-class-field warnings2024-02-06T08:38:06ZRalf Jungjung@mpi-sws.orgFix the future-coercion-class-field warningsWe are getting tons of these, and I expect even more in our reverse dependencies. It might be worth having a script for that.
The following little script by Tej that we used to add all the missing `Global` might be a good starting point...We are getting tons of these, and I expect even more in our reverse dependencies. It might be worth having a script for that.
The following little script by Tej that we used to add all the missing `Global` might be a good starting point:
```
#!/usr/bin/env python3
import sys
import re
error_re = re.compile(r"""^File "(?P<file>[^"]*)", line (?P<line>[0-9]+), characters .*:""")
for line in map(str.rstrip, sys.stdin):
m = error_re.match(line)
if m:
file, line = m.group("file"), m.group("line")
print(f"sed -i '{line}s/^/Global /' '{file}'")
```https://gitlab.mpi-sws.org/iris/iris/-/issues/559iApply applies lemmas without resolving typeclass constraints2024-01-10T15:37:42ZRalf Jungjung@mpi-sws.orgiApply applies lemmas without resolving typeclass constraintsConsider this example:
```
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG...Consider this example:
```
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
Local Existing Instance lock_tokG.
Definition spin_lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_spin_lockΣ {Σ} : subG spin_lockΣ Σ → spin_lockG Σ.
Proof. solve_inG. Qed.
Lemma test `{!spin_lockG Σ} (P Q : iProp Σ) :
P -∗ P -∗ Q.
Proof. Admitted.
Lemma test2 {Σ} (P Q : iProp Σ) :
P -∗ Q.
Proof.
iIntros "HP".
iApply (test with "HP").
```
I would expect the `iApply` to fail, since the `test` lemma needs `spin_lockG` which is not present. Instead, it succeeds and creates a shelved goal. This is a pretty bad user experience since the shelved goal is easy to miss, so it is likely that one will continue in this proof not realizing that one has applied an impossible lemma. This can also cause very strange follow-on effects since the unresolved evar can cause unification failures and other hard-to-diagnose issues.https://gitlab.mpi-sws.org/iris/iris/-/issues/558wp_apply: bad errors when the term is not found or the lemma is used wrong2024-01-09T12:16:04ZRalf Jungjung@mpi-sws.orgwp_apply: bad errors when the term is not found or the lemma is used wrongConsider this test case:
```
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.inva...Consider this test case:
```
From iris.algebra Require Import excl frac_auth numbers.
From iris.proofmode Require Import proofmode.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Import lib.token lib.invariants lib.own.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation adequacy lib.par.
From iris.prelude Require Import options.
Definition newlock : val. Admitted.
Definition acquire : val. Admitted.
Definition release : val. Admitted.
Section test.
Context `{!heapGS_gen hlc Σ}.
Notation iProp := (iProp Σ).
Context (newlock_spec : ∀ R, {{{ R }}} newlock #() {{{ RET #(); True }}}).
Context (acquire_spec : ∀ R, {{{ R }}} acquire #() {{{ RET #(); True }}}).
Lemma test (P : iProp) :
P -∗ WP newlock #() {{ _, True }}.
Proof.
iIntros "HP".
Fail wp_apply acquire_spec.
Fail wp_apply (newlock_spec True%I with "HP").
```
Both of these `wp_apply` fail by just saying "No applicable tactic", which is a pretty bad user experience.
The first should fail saying something about "acquire" not having been found in the goal.
The second should fail the same way `iApply (newlock_spec True%I with "HP")` fails in that situation:
> `iSpecialize: cannot instantiate (True -∗ ▷ (True -∗ ?Goal #()) -∗ WP newlock #() {{ v, ?Goal v }})%I with P.`https://gitlab.mpi-sws.org/iris/iris/-/issues/554This is a test2023-11-20T13:53:59ZRalf Jungjung@mpi-sws.orgThis is a testjust ignore mejust ignore mehttps://gitlab.mpi-sws.org/iris/iris/-/issues/553This is a test2023-11-20T13:53:23ZRalf Jungjung@mpi-sws.orgThis is a testjust ignore mejust ignore mehttps://gitlab.mpi-sws.org/iris/iris/-/issues/552Consider merging "examples" into this repository2023-11-20T13:53:20ZRalf Jungjung@mpi-sws.orgConsider merging "examples" into this repositoryWe now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one reposito...We now have the setup to be able to merge iris/examples into this repository. But do we want to?
Advantages:
- When prototyping changes in Iris we very quickly get some feedback on the impact on reverse dependencies.
- It's one repository less that Robbert and me have to port changes to.
- People trying to fix Coq CI have one repository less to worry about.
Downsides:
- `make` will require Autosubst to fully work
- `make` in Iris will take quite a bit longer
- CI will take longer before a package is published in opam
I don't have a very strong opinion on this. Very rarely I make changes that break something in iris/examples in subtle ways and debugging that would be much easier in a mono repo. But most of the time the overhead from having two repositories is not so bad, and it's nice that people don't have to install Autosubst to make `make` work.https://gitlab.mpi-sws.org/iris/iris/-/issues/551`iSpecialize` fails on `bi_forall` without eta expansion2024-02-16T16:30:51ZRobbert Krebbers`iSpecialize` fails on `bi_forall` without eta expansion```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- wit...```coq
From iris Require Import proofmode.tactics.
(* works --- with eta expansion *)
Lemma foo {PROP : bi} {A} (P : A → PROP) x :
bi_forall (λ x, P x) ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
done.
Qed.
(* fails -- without eta expansion *)
Lemma bar {PROP : bi} {A} (P : A → PROP) x :
bi_forall P ⊢ P x.
Proof.
iIntros "H". iSpecialize ("H" $! x).
(* Tactic failure: iSpecialize: cannot instantiate (∀ y, P y)%I with x. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/550Prevent iFrame from unfolding definitions?2023-11-13T10:09:58ZRalf Jungjung@mpi-sws.orgPrevent iFrame from unfolding definitions?Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding `tc_opaque`, but many people don't know to do that and experience large `iFrame` slowdowns when piling up...Currently, iFrame unfolds at least some definitions. One can opt-out of that by making the definitions typeclasses opaque or adding `tc_opaque`, but many people don't know to do that and experience large `iFrame` slowdowns when piling up abstractions.
It'd be good to investigate whether we can somehow make definition-unfolding for `iFrame` be opt-in rather than opt-out.
One possibility is to use `Hint Extern`, [like `SetUnfold`](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/sets.v#L145). However, that does not allow users to opt-in.
Another possibility would be to use a different hint database where constants are by default opaque.
Either way this is a massive breaking change and would have to be carefully evaluated.https://gitlab.mpi-sws.org/iris/iris/-/issues/549Seal HeapLang points-to2023-11-11T09:36:07ZRobbert KrebbersSeal HeapLang points-toHeapLang defines a notation for the `gen_heap` points-to. This notation has two purposes (1) use `Some` for the value and (2) fix the arguments to the HeapLang `val` so that type inference and scopes work better.
It's currently quite ea...HeapLang defines a notation for the `gen_heap` points-to. This notation has two purposes (1) use `Some` for the value and (2) fix the arguments to the HeapLang `val` so that type inference and scopes work better.
It's currently quite easy to accidentally break abstraction. It's also easy to forget to lift a `gen_heap` lemma because it might work accidentally for the notation.
We thus should make the HeapLang points-to a definition and seal it.
See also the discussion in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98626https://gitlab.mpi-sws.org/iris/iris/-/issues/548How many kinds of `updateP` lemmas do we want?2023-11-10T12:37:43ZJohannes HostertHow many kinds of `updateP` lemmas do we want?Context: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98523
There currently are two ways of specifying the `updateP` behavior of our resource algebras.
For example, for `prod`, the lemma characterizing `updateP` [are t...Context: https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/960#note_98523
There currently are two ways of specifying the `updateP` behavior of our resource algebras.
For example, for `prod`, the lemma characterizing `updateP` [are the following](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/algebra/updates.v#L218):
```
Lemma prod_updateP P1 P2 (Q : A * B → Prop) x :
x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
Lemma prod_updateP' P1 P2 x :
x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
```
Basically, we have the "explicit" style of `prod_updateP'`, where the set of potential update target values is explicitly stated, and we have the "Texan" style of `prod_updateP`, which has built-in weakening and looks more predicate-transformery. We also note that either is easily proven from the other (one direction uses weakening, the other just directly chooses `Q := λ y, P1 (y.1) ∧ ..`).
The question is: Do we always want both? Perhaps, one of these laws is barely used and can be removed, so that in future, only one of these laws needs to be maintained. And then, this law should be consistently used everywhere.https://gitlab.mpi-sws.org/iris/iris/-/issues/547`IsOp` classes are poorly named, fulfill two functions, yet they will be used...2023-11-10T12:26:10ZIke Mulder`IsOp` classes are poorly named, fulfill two functions, yet they will be used differently after !930We noticed in !1004 that the `IsOp`, `IsOp'` and `IsOpLR` classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like `IntoOp` is imo more descriptive of what `IsOpLR` does).
Secondly, `IsOp` is used b...We noticed in !1004 that the `IsOp`, `IsOp'` and `IsOpLR` classes are somewhat problematic.
Firstly, their names are somewhat confusing (something like `IntoOp` is imo more descriptive of what `IsOpLR` does).
Secondly, `IsOp` is used both for merging (`iCombine`ing owns) and splitting (`iSplit`/`iDestruct`ing owns) ops.
This usually saves some lines of code for clients, but complicates things in other cases.
This could be fixed, but these classes will also be used somewhat differently once !930 lands.
After !930, there will be an `IsValidOp` class responsible for `iCombine`ing.
The current proposal for !930 would still rely on `IsOp`---but only for some `cmra`s (those with trivial validity),
and only for `cmra`s that occur as 'leaves' in a term (so not for `cmra`s constructed with combinators).