Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-12-08T15:54:33Zhttps://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) s...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.Robbert KrebbersRobbert Krebbershttps://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 followi...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 n...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 th...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 t...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 a...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 o...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`...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 _ => simp...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 al...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...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.1Robbert KrebbersRobbert Krebbershttps://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 con...```
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. *)
```https://gitlab.mpi-sws.org/iris/iris/-/issues/96Spurious whitespace in proofmode notations2017-08-24T14:09:21ZRobbert KrebbersSpurious whitespace in proofmode notationsThis is probably a result of !59. For example:
```coq
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
```
Coq now displays:
```
_______________________________...This is probably a result of !59. For example:
```coq
Lemma test_iIntros_persistent P Q `{!PersistentP Q, !PersistentP R} :
(P → Q → R → P ∗ Q)%I.
Proof. iIntros "H1 H2 #H3".
```
Coq now displays:
```
______________________________________(1/1)
"H3" : R
--------------------------------------□
"H1" : P
"H2" : Q
--------------------------------------∗
P ∗ Q
```
So, as you can see, the printing of each context starts with a spurious whitespace.
I don't know whether this is a Coq bug, or a bug in our notation. @jung any idea?Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/95Introduce implication if premise is persistent2017-08-24T08:49:51ZRalf Jungjung@mpi-sws.orgIntroduce implication if premise is persistentCurrently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the g...Currently, proof mode refuses to introduce an implication if the spacial context is non-empty. We could relax this based on the fact that if the premise of the implication is persistent, wand and implication are equivalent. So if the goal is `box P -> Q`, introducing should be possible even for a non-empty spatial context.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/94iInv without Hclose2018-07-13T15:55:27ZRalf Jungjung@mpi-sws.orgiInv without HcloseI've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv...I've been talking about accessors today with @janno and @pythonsq. One place where having "actual" accessors might be useful is to avoid "Hclose"-style assumptions. I think we can prototype how that would look like by playing with iInv.
Particularly, I suggest that we get rid of the last parameter of iInv (the name of the "Hclose"), and instead have it add that as an obligation to the postcondition. So, if the goal starts out being `WP e {{ v, Q }}`, then when opening `inv N I` it becomes `WP e {{ v, \later I * Q }}`. Similar things happen when the goal is a view shift.
@robbertkrebbers @jjourdan what do you think? How hard would it be to implement this? We'd probably want a new typeclass generalizing things that can be in the goal when doing iInv. I fear that typeclass will be much like the infamous "frame shift assertions"...