Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2022-10-07T08:41:13Zhttps://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/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/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/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/459Inconsistency in weakening of modalities in `iApply`2022-04-20T14:59:17ZRobbert KrebbersInconsistency in weakening of modalities in `iApply````coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens...```coq
From iris.proofmode Require Import tactics.
Lemma test {PROP : bi} (P Q : PROP) :
(P -∗ <affine> Q) -∗ Q.
Proof.
iIntros "H".
Fail iApply "H". (* fails *)
iApply ("H" with "[]"). (* works *)
```
## Analysis
What happens is that the first (and failing) `iApply` directly attempts to find an `IntoWand` instance to match the conclusion of the wand with the goal. This fails because the only applicable `IntoWand` instance is:
```coq
Global Instance into_wand_wand p q P Q P' :
FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
```
There is no `FromAssumption` for `Q`, so no weakening of the conclusion is performed.
In the second attempt, `iApply` will first `iSpecialize` with the wand. As such, it tries to find an `IntoWand` instance where the conclusion can be unified with an evar. Then after that, it will use `iAssumption`, which uses `FromAssumption` to weaken the modality.
## Solution
We probably should add `FromAssumption` to instances like `into_wand_wand`. I do not know if this was just an omission, or there's a reason for that. Should try.https://gitlab.mpi-sws.org/iris/iris/-/issues/430iInduction does not work well for induction principles involving `Forall`2022-02-11T10:28:24ZRalf Jungjung@mpi-sws.orgiInduction does not work well for induction principles involving `Forall`Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind...Simuliris has an [interesting `IntoIH` instance](https://gitlab.mpi-sws.org/iris/simuliris/-/blob/884fec84a1a79605f7e4e8b2142395e6e39a7405/theories/stacked_borrows/log_rel_structural.v#L18) to support doing `iInduction ... using expr_ind`, where `expr_ind` is a custom induction principle that uses `Forall` to handle nested lists.
Here's a self-contained testcase:
```coq
Inductive tree (T : Type) := Tree : list (tree T) → tree T.
Arguments Tree {T}.
Lemma tree_ind' T (P : tree T → Prop) :
(∀ l, Forall P l → P (Tree l)) →
∀ t, P t.
Proof.
intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
induction l as [|t l IH].
{ constructor. }
constructor; last apply IH.
apply REC.
Qed.
Lemma test_iInduction_Forall (t : tree nat) (P : PROP) : ⊢ P.
Proof. iInduction t as [] "IH" using tree_ind'.
```
This shows a goal
```
PROP : bi
l : list (tree nat)
P : PROP
============================
"IH" : <pers> ?P
--------------------------------------□
P
```
An `unshelve` shows that the `IntoIH` simply was not resolved, which seems like a bug in its own right -- `iInduction` should fail in that case.
In fact this testcase is interesting in the sense that even adding the instance from Simuliris (even after getting rid of the `BiAffine` assumption) does not help:
```coq
Section tactics.
Import iris.bi.bi.
Import iris.proofmode.base environments classes modality_instances.
Import bi.
Import env_notations.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
Import coq_tactics.
Local Instance into_ih_Forall {A} (φ : A → Prop) (l : list A) Δ Φ :
(∀ x, x ∈ l → IntoIH (φ x) Δ (Φ x)) → IntoIH (Forall φ l) Δ (∀ x, ⌜x ∈ l⌝ → Φ x) | 2.
Proof.
rewrite /IntoIH Forall_forall => HΔ Hf. apply forall_intro=> x.
iIntros "Henv %Hl". iApply (HΔ with "Henv"); eauto.
Qed.
End tactics.
```Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/443Please create a tag for Coq 8.15 in Coq Platform 2022.022022-01-24T09:07:09ZMichael SoegtropPlease create a tag for Coq 8.15 in Coq Platform 2022.02The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an excep...The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.5.0) does not work with Coq 8.15.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
bb946806c5aa9bcb8184a8cb3bc1befecc0322a0 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.15, preferably before February 14, 2022?
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 January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.
The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/193Tej Chajedtchajed@gmail.comTej Chajedtchajed@gmail.comhttps://gitlab.mpi-sws.org/iris/iris/-/issues/351Decouple framing and IntoSep2022-01-17T02:16:40ZRalf Jungjung@mpi-sws.orgDecouple framing and IntoSepCurrently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disab...Currently, `IntoSep` does a few things that can be rather expensive, like `AsFractional` conversion. This is very useful for destruct patterns, but `IntoSep` is also used for framing, and there we want to be cheap. @tchajed already disabled some `IntoSep` instances in Perennial for this reason.
It might make sense to have a separate IntoSep for framing that is more optimized for performance and, for example, does not try to exploit fractional things.
This is somewhat similar to https://gitlab.mpi-sws.org/iris/iris/-/issues/186.
To avoid making a mess, probably we should figure out https://gitlab.mpi-sws.org/iris/iris/-/issues/139 first.https://gitlab.mpi-sws.org/iris/iris/-/issues/334Expand test coverage of proofmode2021-12-16T22:21:12ZTej Chajedtchajed@gmail.comExpand test coverage of proofmodeThe proof mode tests don't cover the following:
- [x] `iRename`
- [x] `iTypeOf`
- [x] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris...The proof mode tests don't cover the following:
- [x] `iRename`
- [x] `iTypeOf`
- [x] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.https://gitlab.mpi-sws.org/iris/iris/-/issues/415Tracking issue for append-only list RA2021-11-22T17:58:29ZRalf Jungjung@mpi-sws.orgTracking issue for append-only list RAThis is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Op...This is the tracking issue for the append-only list RA from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/661. A tracking issue is where we track and discuss what still needs to happen to make a module move to Iris proper.
## Open issues
* Do we really want notation for the mono_list algebra elements? The main "pro" reason here is that `dfrac` otherwise becomes somewhat painful. OTOH, mono_nat and gset_bij algebras do not have notation either. It'd be safe to start without notation
and add them on-demand.
* On the logic layer, should `mono_list_auth` take `Qp` or `dfrac`? Eventually we want to move everything to `dfrac` but again the concern is that (without good notation), this will make the library more annoying to use. This is discussed in more generality at https://gitlab.mpi-sws.org/iris/iris/-/issues/412.
* Do a solid review of the API surface.https://gitlab.mpi-sws.org/iris/iris/-/issues/435Please create a tag for Coq 8.14 in Coq Platform 2021.112021-11-14T18:33:05ZMichael SoegtropPlease create a tag for Coq 8.14 in Coq Platform 2021.11The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of di...The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.4.0) does not work with Coq 8.14+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
ee6a36b3e803ebec465bf44bb5bcbf9b19fe6b62 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag, or communicate us any existing tag that works with Coq branch v8.14, preferably before November 15, 2021?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/139https://gitlab.mpi-sws.org/iris/iris/-/issues/436opam package description is not helpful2021-10-26T21:59:09ZMichael Soegtropopam package description is not helpfulThe package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_l...The package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
```
The description should more elaborate on the question what this can be used for.
See (https://coq.inria.fr/opam/released/packages/coq-iris/coq-iris.3.4.0/opam)
See (https://coq.inria.fr/opam/released/packages/coq-iris-heap-lang/coq-iris-heap-lang.3.4.0/opam)
Please note that (afaik) it is no issue to change the description of opam packages without creating a new version.https://gitlab.mpi-sws.org/iris/iris/-/issues/437Typo in documentation2021-10-26T19:12:53ZAlexandre MoineTypo in documentationHi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two l...Hi,
There is a typo here: https://plv.mpi-sws.org/coqdoc/iris/iris.algebra.cmra.html#lab34, which shows:
![2021-10-19_09-35](/uploads/a590aa61f3327bb234d97e50b29cd31a/2021-10-19_09-35.png)
It comes from a section title spitted in two lines. This seems to be the only occurrencehttps://gitlab.mpi-sws.org/iris/iris/-/issues/432iApply "auto frame": bad error message2021-09-06T06:47:59ZRalf Jungjung@mpi-sws.orgiApply "auto frame": bad error messageThe following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable t...The following test shows a bad error message:
```
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ <affine> P -∗ Q -∗ R.
Proof. iIntros "H _ HQ". by iApply ("H" with "[$]"). Qed.
```
```
Error: No applicable tactic.
```
There is a `fail "iSpecialize: premise cannot be solved by framing"` in the tactic code but that does not seem to work.https://gitlab.mpi-sws.org/iris/iris/-/issues/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/314Argument to bi_pure should have argument at type_scope?2021-06-16T21:14:34ZGregory MalechaArgument to bi_pure should have argument at type_scope?The argument of `bi_pure` is marked as `stdpp` scope, which seems odd since it is a `Prop`? This works since all notations inside of stdpp have stdpp_scope, but it isn't nicely compatible with non stdpp notations.
If you already have a ...The argument of `bi_pure` is marked as `stdpp` scope, which seems odd since it is a `Prop`? This works since all notations inside of stdpp have stdpp_scope, but it isn't nicely compatible with non stdpp notations.
If you already have a `Open Scope stdpp_scope` in your file, you should already get access to notations in stdpp scope.https://gitlab.mpi-sws.org/iris/iris/-/issues/421Bad error message for failing iInduction2021-06-14T13:59:19ZRalf Jungjung@mpi-sws.orgBad error message for failing iInductionI am not sure what is going wrong with the following `iInduction`, and IPM's error doesn't tell me:
```
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t...I am not sure what is going wrong with the following `iInduction`, and IPM's error doesn't tell me:
```
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t v_s :
val_rel v_t v_s -∗ True.
Proof. iInduction v_t as [| |] "IH" forall v_s.
(* Error: No matching clauses for match. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/409Proposed change to naming convention for "dataful" `*G`s2021-06-03T09:08:26ZRalf Jungjung@mpi-sws.orgProposed change to naming convention for "dataful" `*G`sSome of our `*G` typeclasses are different than others: they contain not just `inG` but actual relevant data; usually a `gname` but in the case of `irisG` also some further information about how the Iris program logic is being instantiat...Some of our `*G` typeclasses are different than others: they contain not just `inG` but actual relevant data; usually a `gname` but in the case of `irisG` also some further information about how the Iris program logic is being instantiated. These dataful classes come with a `*PreG` that represent their `inG` (dataless) part.
Dataful `*G`s need to be treated differently, e.g. they have special initialization lemmas and they should not be bundled in library's `*G` as that leads to duplication of said data. So I propose to adjust our naming convention such that one can tell from the name whether a `*G` is dataful or not.
The new naming convention is up for bikeshedding; here are some proposals coming to my mind:
1. We call the dataful class `*DataG` and its `inG`-only part `*G`. So e.g. `heapG` → `heapDataG` and `heapPreG` → `heapG`.
2. We call the dataful class `*DataG` and its `inG`-only part `*PreG`. So e.g. `heapG` → `heapDataG`; `heapPreG` stays.
2. We call the dataful class `*DG` and its `inG`-only part `*PreG`. So e.g. `heapG` → `heapDG`; `heapPreG` stays.
I think I prefer (2) or (3) over (1) because it prevents confusion due to accidentally using the `inG`-only part, and also because it is easier for migration since we don't reuse an old name for a different purpose.
@robbertkrebbers @tchajed @jtassaro what do you think?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.org