Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2019-06-18T17:44:46Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/118Notation `A -c> B` makes no sense2019-06-18T17:44:46ZRobbertNotation `A -c> B` makes no senseThe `c` goes back to the time we solely used COFEs, now that we use OFEs, this notation makes no sense whatsoever.The `c` goes back to the time we solely used COFEs, now that we use OFEs, this notation makes no sense whatsoever.Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/116A tactical for applying tactics to individual proof mode hypotheses2018-01-24T15:27:28ZRobbertA tactical for applying tactics to individual proof mode hypothesesFor example, so that you can perform a `rewrite` or `simpl` in just one proof mode hypothesis.
Ssreflect also has such a tactical.For example, so that you can perform a `rewrite` or `simpl` in just one proof mode hypothesis.
Ssreflect also has such a tactical.RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/-/issues/115Test2017-12-08T15:54:33ZRalf Jungjung@mpi-sws.orgTestThis is an issue to test the mattermost integration. Please ignore.This is an issue to test the mattermost integration. Please ignore.https://gitlab.mpi-sws.org/iris/iris/-/issues/114Possibly confusing naming: auth_own_valid.2019-06-06T11:06:35ZDan FruminPossibly confusing naming: auth_own_valid.I was wondering if anyone else found this a bit confusing.
The lemma `auth_own_valid` refers to two things:
- `base_logic.lib.auth.auth_own_valid` which states that `own γ (◯ a) ⊢ ✓ a`;
- `algebra.auth.auth_own_valid` which (roughly) states that `✓ (● a, ◯ b) → ✓ b`.
If you need both of those modules, then the order in which you import them is quite significant.
I guess the issue is that `auth_own` refers both to the *proposition of owning* the fragment part of the Auth algebra and to the actual fragment part of the algebra.I was wondering if anyone else found this a bit confusing.
The lemma `auth_own_valid` refers to two things:
- `base_logic.lib.auth.auth_own_valid` which states that `own γ (◯ a) ⊢ ✓ a`;
- `algebra.auth.auth_own_valid` which (roughly) states that `✓ (● a, ◯ b) → ✓ b`.
If you need both of those modules, then the order in which you import them is quite significant.
I guess the issue is that `auth_own` refers both to the *proposition of owning* the fragment part of the Auth algebra and to the actual fragment part of the algebra.RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/-/issues/113Do not run `simpl` on user-visible goals2017-12-02T00:07:12ZRalf Jungjung@mpi-sws.orgDo not run `simpl` on user-visible goalsThe proof mode, and in particular the `wp_*` tactics, currently sometimes run `simpl` on the user's goal. That can be annoying if `simpl` misbehaves. Ideally, we should avoid running `simpl` on user goals.The proof mode, and in particular the `wp_*` tactics, currently sometimes run `simpl` on the user's goal. That can be annoying if `simpl` misbehaves. Ideally, we should avoid running `simpl` on user goals.RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/-/issues/112Make invariants and slices closed under equivalence2018-02-08T10:43:12ZRalf Jungjung@mpi-sws.orgMake invariants and slices closed under equivalenceThis has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
```coq
Lemma inv_iff P Q :
later persistently (P <-> Q) -> inv P -> inv Q.
```
I think this may be worth it, *if* it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for `slice`, which requires either a separate closure in `slice` (so the one in `inv` does not help), or doing the same kind of closure in `saved_prop_own` (but then, do we also want the equivalent law for `saved_pred_own`?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.This has come up several times before. I think @jjourdan has proposed this previously and I have argued against it, but by now I feel like it may be worth a try. We could slightly change the definition of invariants so that the following holds:
```coq
Lemma inv_iff P Q :
later persistently (P <-> Q) -> inv P -> inv Q.
```
I think this may be worth it, *if* it means we can simplify the definition of the lifetime logic a little bit. However, that will only be the case if we manage to also get this law for `slice`, which requires either a separate closure in `slice` (so the one in `inv` does not help), or doing the same kind of closure in `saved_prop_own` (but then, do we also want the equivalent law for `saved_pred_own`?).
Also, I am not sure if we should do this before or after Iris 3.1. Either way, it is backwards-compatible.https://gitlab.mpi-sws.org/iris/iris/-/issues/111Proof mode only *mostly* works when it is transitively imported, not exported2017-11-20T14:47:41ZRalf Jungjung@mpi-sws.orgProof mode only *mostly* works when it is transitively imported, not exportedI was debugging some very strange behavior with @janno yesterday, which turned out to be the following: In iGPS, imports and exports are somewhat... messy. (To be fair, I feel that's a very common problem with Coq developments. I know no best practices.) In particular, there are files that do `From iris.proofmode Require Import tactics`, and then other files import that file. That's enough to get notations, because they are *always* imported, ignoring the usual reexport rules. (Should we report a Coq bug about that? It does not seem necessary.) However, every since @robbertkrebbers recently disabled `Automatic Coercions Imports`, this is *not* enough to get working coercions. So, most tactics worked, but some (e.g. `iCombine`) rely on coercions and did not work.
I think we should do one of two things:
1. Make the entire proofmode work when it is just re-imported, not re-exported.
2. Make `iStartProof` fail when the proof mode is just re-imported, not re-exported.
(1) would be somewhat nicer as it means the proofmode works "more often".I was debugging some very strange behavior with @janno yesterday, which turned out to be the following: In iGPS, imports and exports are somewhat... messy. (To be fair, I feel that's a very common problem with Coq developments. I know no best practices.) In particular, there are files that do `From iris.proofmode Require Import tactics`, and then other files import that file. That's enough to get notations, because they are *always* imported, ignoring the usual reexport rules. (Should we report a Coq bug about that? It does not seem necessary.) However, every since @robbertkrebbers recently disabled `Automatic Coercions Imports`, this is *not* enough to get working coercions. So, most tactics worked, but some (e.g. `iCombine`) rely on coercions and did not work.
I think we should do one of two things:
1. Make the entire proofmode work when it is just re-imported, not re-exported.
2. Make `iStartProof` fail when the proof mode is just re-imported, not re-exported.
(1) would be somewhat nicer as it means the proofmode works "more often".Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/110Import OCPL's heap_lang logic?2018-07-13T15:57:18ZDavid SwaseyImport OCPL's heap_lang logic?From !37:
> Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with the strictly more expressive OCPL, and adding the OCPL examples to heap_lang/lib and tests/.
Ralf asked if I have a git repo. Yes. I will create a merge request once we settle !37. (OCPL builds on !37.)From !37:
> Please take a look at the heap interface in Fig. 2 of my OCPL paper (off my home page) or, more informatively, at theories/heap_lang/heap.v in the OCPL Coq development. I propose replacing the current heap_lang logic with the strictly more expressive OCPL, and adding the OCPL examples to heap_lang/lib and tests/.
Ralf asked if I have a git repo. Yes. I will create a merge request once we settle !37. (OCPL builds on !37.)David SwaseyDavid Swaseyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/109Post-Iris 3.12018-06-05T08:05:48ZRalf Jungjung@mpi-sws.orgPost-Iris 3.1After Iris 3.1 is released:
* [x] Switching timing measurements to the Coq 8.7 build.
* [x] Drop support for Coq 8.6?
* [x] Enable `test_iIntros_pure`.
* [x] Drop opam dependency on ssreflect, use the one embedded in Coq instead.
Are there other work-arounds we can remove or new features we want to make use of?After Iris 3.1 is released:
* [x] Switching timing measurements to the Coq 8.7 build.
* [x] Drop support for Coq 8.6?
* [x] Enable `test_iIntros_pure`.
* [x] Drop opam dependency on ssreflect, use the one embedded in Coq instead.
Are there other work-arounds we can remove or new features we want to make use of?https://gitlab.mpi-sws.org/iris/iris/-/issues/108iIntros on pure implications stopped working2017-10-28T21:10:55ZRalf Jungjung@mpi-sws.orgiIntros on pure implications stopped workingThe following proof script used to work, but does not any more:
```
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
```
This is probably a regression of the typeclass-based iIntros?The following proof script used to work, but does not any more:
```
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
```
This is probably a regression of the typeclass-based iIntros?Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/107Reverting to old (stronger) definition of atomicity2017-10-29T14:58:25ZAmin TimanyReverting to old (stronger) definition of atomicityIn Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` is *stuck*.
The old definition was: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` *is a value*.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike ```WP``` do not guarantee safety, e.g., ```IC``` (if convergent predicates).In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` is *stuck*.
The old definition was: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` *is a value*.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike ```WP``` do not guarantee safety, e.g., ```IC``` (if convergent predicates).Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/106Iris 3.12018-01-09T15:55:25ZRalf Jungjung@mpi-sws.orgIris 3.1In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels of `_ ;; _` and `_ <- _ ;; _`
* [ ] Make sure all our CI'd reverse dependencies build with master.In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels of `_ ;; _` and `_ <- _ ;; _`
* [ ] Make sure all our CI'd reverse dependencies build with master.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/105Add some theory about the interaction of plainly and fancy updates2017-11-01T23:47:30ZRalf Jungjung@mpi-sws.orgAdd some theory about the interaction of plainly and fancy updates@amintimany has some theory there, we should get the reusable bits upstream.@amintimany has some theory there, we should get the reusable bits upstream.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/103Find a better name for iMod2017-11-24T15:57:13ZRalf Jungjung@mpi-sws.orgFind a better name for iModWe do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`. `iUpd` is my personal favorite. I know that the tactic supports other modalities, but 99,9% of the time it is used to eliminate some form of an update. The name is more informative than `iMod`, and not more wrong.
`iRun` is slightly less informative, but also less wrong: The tactic does bind in a monad, which can be seen as "running the computation".
Cc @robbertkrebbers @jjourdan
EDIT: All right, I stand corrected on the "wrong" part. Sorry for that. It is still uninformative.We do have at least one more badly named item: iMod. The name is both uninformative (what does it do with the modality?) and wrong (the tactic does nothing with the persistent and plain modalities).
Proposed alternatives: `iRun`, `iUpd`. `iUpd` is my personal favorite. I know that the tactic supports other modalities, but 99,9% of the time it is used to eliminate some form of an update. The name is more informative than `iMod`, and not more wrong.
`iRun` is slightly less informative, but also less wrong: The tactic does bind in a monad, which can be seen as "running the computation".
Cc @robbertkrebbers @jjourdan
EDIT: All right, I stand corrected on the "wrong" part. Sorry for that. It is still uninformative.https://gitlab.mpi-sws.org/iris/iris/-/issues/102`solve_proper` having troubles proving non-expansiveness2017-10-10T11:50:17ZDan Frumin`solve_proper` having troubles proving non-expansivenessIn the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simpl; f_equiv)` to automatically discharge the obligations.
Is there a reason why this simplification is not happening in `solve_proper_core`?
Is it for the performance reasons?
```coq
From iris.heap_lang Require Import lang proofmode tactics notation.
Section linkedlist.
Context `{heapG Σ}.
Program Definition pre_isLinkedList : (valC -n> iProp Σ) -n> (valC -n> iProp Σ) :=
λne P v, (⌜v = InjLV #()⌝
∨ ∃ (h t : val) (l : loc),
⌜v = InjRV (PairV h #l)⌝
∗ l ↦ t
∗ ▷ (P t))%I.
Solve Obligations with solve_proper_core ltac:(fun _ => simpl; f_equiv).
End linkedlist.
```In the snippet below`solve_proper` is not able to prove non-expansiveness of a higher-order predicate.
`solve_proper` is defined as `solve_proper_core ltac:(fun _ => f_equiv)`.
However, one can use `solve_proper_core ltac:(fun _ => simpl; f_equiv)` to automatically discharge the obligations.
Is there a reason why this simplification is not happening in `solve_proper_core`?
Is it for the performance reasons?
```coq
From iris.heap_lang Require Import lang proofmode tactics notation.
Section linkedlist.
Context `{heapG Σ}.
Program Definition pre_isLinkedList : (valC -n> iProp Σ) -n> (valC -n> iProp Σ) :=
λne P v, (⌜v = InjLV #()⌝
∨ ∃ (h t : val) (l : loc),
⌜v = InjRV (PairV h #l)⌝
∗ l ↦ t
∗ ▷ (P t))%I.
Solve Obligations with solve_proper_core ltac:(fun _ => simpl; f_equiv).
End linkedlist.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/101Make Iris run in jsCoq2017-11-30T09:53:53ZRalf Jungjung@mpi-sws.orgMake Iris run in jsCoqCurrent status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert already mentioned that he wanted to look into that.Current status according to @janno:
> I think I got all Iris dependencies to work. The only problem I encountered was the lack of vm_compute. However, that seems to be only necessary for generating fresh names for hypotheses. Robbert already mentioned that he wanted to look into that.https://gitlab.mpi-sws.org/iris/iris/-/issues/100Proof mode notation broken depending on import order2017-11-11T09:19:19ZRalf Jungjung@mpi-sws.orgProof mode notation broken depending on import orderIt is a long-standing issue that sometimes, depending on the order of re-exports and imports, the proof mode notation is broken. I finally decided to minimize this, and you can find the result in the [`ipm-notation-broken` branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/ipm-notation-broken). I first thought this is a Coq bug, but now I am not so sure anymore: We do have different notations in the same scope that lead to printing being ambiguous.
Namely, we have
```
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
(at level 99, Q at level 200, right associativity) : C_scope.
```
and
```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) ⊢ Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
```
We seem to be relying on a guarantee that if one notation is strictly more specific than another one, it will have higher priority. Does Coq claim to have such a guarantee?
Maybe one possible solution would be to move the proof mode notations into a different scope, and have `iStartProof` introduce that scope (i.e., turn the goal into `(...)%ProofMode`).It is a long-standing issue that sometimes, depending on the order of re-exports and imports, the proof mode notation is broken. I finally decided to minimize this, and you can find the result in the [`ipm-notation-broken` branch](https://gitlab.mpi-sws.org/FP/iris-coq/tree/ipm-notation-broken). I first thought this is a Coq bug, but now I am not so sure anymore: We do have different notations in the same scope that lead to printing being ambiguous.
Namely, we have
```
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
(at level 99, Q at level 200, right associativity) : C_scope.
```
and
```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(of_envs (Envs Γ Δ) ⊢ Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
```
We seem to be relying on a guarantee that if one notation is strictly more specific than another one, it will have higher priority. Does Coq claim to have such a guarantee?
Maybe one possible solution would be to move the proof mode notations into a different scope, and have `iStartProof` introduce that scope (i.e., turn the goal into `(...)%ProofMode`).Iris 3.1RobbertRobberthttps://gitlab.mpi-sws.org/iris/iris/-/issues/99iNext does not strip off later below existential2017-10-02T13:34:05ZRalf Jungjung@mpi-sws.orgiNext does not strip off later below existential```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below conjunctions, but not below existentials.```
Lemma test_strip_later (φ : M → uPred M) :
(∃ x, ▷ φ x) -∗ ▷ (∃ x, φ x).
Proof.
iIntros "H". iNext.
(* Now H is still (∃ x, ▷ φ x), I would have expected (∃ x, φ x). *)
done.
Qed.
```
Stripping off laters does happen below conjunctions, but not below existentials.https://gitlab.mpi-sws.org/iris/iris/-/issues/98`iIntros.` fails to introduce `True`2017-09-27T08:45:17ZRalf Jungjung@mpi-sws.org`iIntros.` fails to introduce `True````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
``````
Lemma push_atomic_spec (s: loc) (x: val) :
True -∗ (WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros "?".
```
shows an error:
```
Tactic failure: iIntro: nothing to introduce.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/97`iIntros.` should always enter proof mode2017-09-27T08:45:18ZRalf Jungjung@mpi-sws.org`iIntros.` should always enter proof mode```
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
``````
Lemma test (s: loc) (x: val) :
(WP ref InjR x {{ v, WP let: "s'" := v in #() {{ _, True }} }})%I.
Proof.
iIntros.
(* Now I should be in proof mode, but I am not. *)
```