Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-01-07T13:58:38Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/195Always qualify Instance with Local or Global2021-01-07T13:58:38ZRalf Jungjung@mpi-sws.orgAlways qualify Instance with Local or GlobalSince you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? Fo...Since you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? For the same reason that we should always use qualifiers, `sed` cannot know whether we are inside a section.
I can do the `sed`, but I'm not sure how to do the review if any of these should be `Local`. Also, let's do this after merging some MRs because this will cause plenty of conflicts.https://gitlab.mpi-sws.org/iris/iris/-/issues/194coq-speed: Measure using performance counters2018-06-22T22:02:37ZRalf Jungjung@mpi-sws.orgcoq-speed: Measure using performance counters@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?https://gitlab.mpi-sws.org/iris/iris/-/issues/192Document `iRewrite -...` in `ProofMode.md`2019-01-11T10:13:31ZDan FruminDocument `iRewrite -...` in `ProofMode.md`I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```https://gitlab.mpi-sws.org/iris/iris/-/issues/191Printing of the sequence operator `;;`2018-06-13T10:08:33ZMarianna RapoportPrinting of the sequence operator `;;`The [first](https://gitlab.mpi-sws.org/FP/iris-examples/blob/f9bee86a91025f7d727a1765a2d9ad98fbd10c9f/theories/lecture_notes/coq_intro_example_1.v) Coq example that comes with the Iris [lecture notes]() shows how to prove a lemma with th...The [first](https://gitlab.mpi-sws.org/FP/iris-examples/blob/f9bee86a91025f7d727a1765a2d9ad98fbd10c9f/theories/lecture_notes/coq_intro_example_1.v) Coq example that comes with the Iris [lecture notes]() shows how to prove a lemma with the following proof goal:
`{{{ ℓ ↦ #n }}} (incr ℓ) ||| (incr ℓ) ;; !#ℓ {{{m, RET #m; ⌜n ≤ m⌝ }}}`
However, in the interactive proof mode, the goal is displayed as
`{{{ ℓ ↦ #n }}} (Lam <> ! #ℓ) (incr ℓ ||| incr ℓ) {{{ (m : Z), RET #m; ⌜n ≤ m⌝}}}`
I.e. Coq automatically desugars the `;;` notation.https://gitlab.mpi-sws.org/iris/iris/-/issues/190Framing persistent hypotheses under a later in the goal2018-07-13T08:40:31ZHai DangFraming persistent hypotheses under a later in the goalI have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.I have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.https://gitlab.mpi-sws.org/iris/iris/-/issues/189Tests do not compile on MacOS2018-05-31T16:30:05ZLéon GondelmanTests do not compile on MacOSI've tried to compile iris 3bed085d035f199518707472be59d18e5bbf8342 on the branch gen_proofmode and the tests did not manage to compile.
```
COQC [test] tests/algebra.v
COQC [test] tests/heap_lang.v
COQC [test] tests/ipm_paper.v
COQC [...I've tried to compile iris 3bed085d035f199518707472be59d18e5bbf8342 on the branch gen_proofmode and the tests did not manage to compile.
```
COQC [test] tests/algebra.v
COQC [test] tests/heap_lang.v
COQC [test] tests/ipm_paper.v
COQC [test] tests/list_reverse.v
/bin/sh: tempfile: command not found
/bin/sh: tempfile: command not found
/bin/sh: tempfile: command not found
make[2]: *** [tests/heap_lang.vo] Error 127
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [tests/ipm_paper.vo] Error 127
make[2]: *** [tests/algebra.vo] Error 127
/bin/sh: tempfile: command not found
make[2]: *** [tests/list_reverse.vo] Error 127
make[1]: *** [all] Error 2
make: *** [all] Error 2
```https://gitlab.mpi-sws.org/iris/iris/-/issues/188eauto very slow when there is a chain of Iris quantifiers2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgeauto very slow when there is a chain of Iris quantifiersSteps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e...Steps to reproduce:
* Change the `iIntros` hints in `ltac_tactics.v` to `iIntros (?).` and `iIntros "?".`.
* Compile `ectx_lifting.v`
`wp_lift_atomic_head_step_no_fork` takes forever:
```
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None →
(∀ σ1, state_interp σ1 ={E}=∗
⌜head_reducible e1 σ1⌝ ∗
▷ ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
⊢ WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step. done.
(* now it gets slow *) eauto.
```
Something seems to be exponential in the number of quantifiers. We currently use `iIntros.` to introduce them all at once but that's more of a work-around. I can't even really figure out what is taking so long, but I can definitely see tons of `FromAssumption` in the trace.
Cc @robbertkrebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/187Support framing in `iCombine`.2018-07-13T08:40:31ZDan FruminSupport framing in `iCombine`.I wish that the `iCombine` tactic would support framing: `iCombine "H1 H2" as "$"`.I wish that the `iCombine` tactic would support framing: `iCombine "H1 H2" as "$"`.https://gitlab.mpi-sws.org/iris/iris/-/issues/186iAssert without any spatial assumptions should produce a persistent result2020-09-29T11:15:49ZRalf Jungjung@mpi-sws.orgiAssert without any spatial assumptions should produce a persistent resultThe following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```...The following proof script should work:
```
Lemma test_persistent_assert `{!BiBUpd PROP} P :
□ P -∗ □ |==> P.
Proof.
iIntros "#HP".
iAssert (|==> P)%I as "#HPupd". (* FAIL! *)
{ iIntros "!> !> !>". done. }
iAssumption.
Qed.
```
It currently fails because the update is not persistent -- however, this is an iAssert which is not provided any spatial assertions, so whatever it produces can always be put into the persistent context.https://gitlab.mpi-sws.org/iris/iris/-/issues/185"iApply ... with" unifies with assumptions before taking goal into account2019-11-01T13:45:51ZRalf Jungjung@mpi-sws.org"iApply ... with" unifies with assumptions before taking goal into accountThe following test case fails:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```
This is fairly an...The following test case fails:
```coq
Lemma test_apply_unification_order {A : Type}
(Φ : (A → PROP) → PROP)
(HΦ : forall f x, f x -∗ Φ f) f x :
id (f x) -∗ Φ f.
Proof. iIntros "Hf". iApply (HΦ with "Hf"). Qed.
```
This is fairly annoying when working with higher-order lemmas, for example it came up in the logically atomic context when trying to apply
```coq
Lemma astep_intro Eo Em α P β Φ x :
α x -∗
((α x ={Eo}=∗ P) ∧ (∀ y, β x y ={Eo}=∗ Φ x y)) -∗
atomic_step Eo Em α P β Φ.
```
where `α : A -> PROP`. Now `iApply (astep_intro with "foo")` fails to apply in most cases because it infers the wrong `α`.https://gitlab.mpi-sws.org/iris/iris/-/issues/184`wp_binop` is not very useful for comparing arbitrary values2018-05-03T13:06:04ZDan Frumin`wp_binop` is not very useful for comparing arbitrary valuesConsider the following piece of code:
```
From iris.heap_lang Require Export proofmode notation.
Lemma wut `{heapG Σ} (v1 v2 : val) :
(WP if: (v1 = v2) then #0 else #0 {{ _, True }})%I.
Proof.
wp_binop.
Abort.
```
The goal that I ...Consider the following piece of code:
```
From iris.heap_lang Require Export proofmode notation.
Lemma wut `{heapG Σ} (v1 v2 : val) :
(WP if: (v1 = v2) then #0 else #0 {{ _, True }})%I.
Proof.
wp_binop.
Abort.
```
The goal that I expected after executing `wp_binop`:
```
WP if: #(bool_decide (v1 = v2)) then #0 else #0 {{ _, True }}
```
Instead I got two goals:
- `bin_op_eval EqOp v1 v2 = Some ?Goal0`
- `WP if: ?Goal0 then #0 else #0 {{ _, True }}`
This is not very helpful, as it is pretty annoying to get a boolean value for ?Goal0.
I believe this is due to the way that `bin_op_eval` is defined:
it first matches `v1` and `v2` for specific types of values (integers or booleans), and only then considers the case of generalized equality checks.
Since we have generalized/dynamic equality checks in heap_lang, why not first match on the type of the operation, and only then match on the values in `bin_op_eval`?
Best
-Danhttps://gitlab.mpi-sws.org/iris/iris/-/issues/183Stronger/Weaker iFrame2022-12-06T22:37:13ZRalf Jungjung@mpi-sws.orgStronger/Weaker iFrameIn a situation like
```
H1: R
H2: P
----------------------*
R * (P /\ Q)
```
calling `iFrame` will turn the goal into
```
----------------------*
Q
```
This is too aggressive: Frequently, I will need `P` to prove `Q`.In a situation like
```
H1: R
H2: P
----------------------*
R * (P /\ Q)
```
calling `iFrame` will turn the goal into
```
----------------------*
Q
```
This is too aggressive: Frequently, I will need `P` to prove `Q`.https://gitlab.mpi-sws.org/iris/iris/-/issues/182done when goal is evar picks unnecessarily strong2018-07-13T08:40:31ZRalf Jungjung@mpi-sws.orgdone when goal is evar picks unnecessarily strongWhen the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spa...When the goal is an evar (and that evar does not appear otherwise in the current goal), like in
```
_ : inv nroot (∃ x' : Z, l ↦ #x')%I
--------------------------------------□
?P
```
then doing `done` will pick a persistent (or spatial, I guess) hypothesis instead of just `True` or `emp`.
Maybe we should add `bi.True_intro` with high priority to the database?https://gitlab.mpi-sws.org/iris/iris/-/issues/181wp_apply instantiates evars too far2018-07-13T08:51:26ZRalf Jungjung@mpi-sws.orgwp_apply instantiates evars too far```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s;...```coq
Lemma wp_apply_evar e :
(∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
Proof.
iIntros "H". wp_apply "H".
```
The goal is now
```
============================
--------------------------------------∗
WP ?e @ ?s; ?E {{ v, ?Φ v }}
```
but it should be
```
============================
--------------------------------------∗
?Q
```
This is in the generalized proofmode branch.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/180Explore performance implications of gen_proofmode2019-11-01T12:49:47ZRalf Jungjung@mpi-sws.orgExplore performance implications of gen_proofmodea74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> y...a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search) made lambdaRust noticeably slower.
Also see the conversation following <https://mattermost.mpi-sws.org/iris/pl/btp695ny3prqjdqzojw9sj5i9w>. In particular:
> yeah, the bottelneck is definitely notypeclasses refine: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/-/jobs/9346 took 29:47 user time
> btw we also have a 1min regression in this range: https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/8799209d9c00f825e9ac059b3b864119e34f9aec...00b0c7704278028c4a73c9f0686a9070e92d3a06
> and ~30sec over https://gitlab.mpi-sws.org/FP/LambdaRust-coq/compare/474f82283e423b03ccf0adeb367e36eb68346a29...8799209d9c00f825e9ac059b3b864119e34f9aec
Looking at the [performance graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1516679125714&to=now), the two commit ranges with the most sustained impact are LambdaRust-coq@c2c2b874eea8...00b0c7704278 and LambdaRust-coq@00b0c7704278...158d46797c99. They correspond to iris-coq@aa5b93f6319b9cb2d17a1c9f61947233b4033484...1a092f96b1350896c3801edb90b453f5b4d2a4cf and iris-coq@1a092f96b1350896c3801edb90b453f5b4d2a4cf...a74b8077f199e2d21ff49e91b5af0dfdcee362ff in Iris. The latter is just a74b8077f199e2d21ff49e91b5af0dfdcee362ff (more control over typeclass search), but the former is just a whole bunch of commits that, altogether, seem to have made things slower by 40sec in LambdaRust.
There is also some variation in [this part of the graph](https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&var-project=lambda-rust&var-branch=ci%2Fgen_proofmode&var-config=All&from=1518563995005&to=1520160053680) but I am not sure if that's real or just noise.https://gitlab.mpi-sws.org/iris/iris/-/issues/179Strengthen strong allocation lemmas to work for any infinite set2019-02-17T18:14:30ZRalf Jungjung@mpi-sws.orgStrengthen strong allocation lemmas to work for any infinite setNow that std++ has https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/blob/master/theories/infinite.v, we should be able to provide stronger versions of `own_alloc_strong` and similar lemmas.Now that std++ has https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/blob/master/theories/infinite.v, we should be able to provide stronger versions of `own_alloc_strong` and similar lemmas.https://gitlab.mpi-sws.org/iris/iris/-/issues/178`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviors2019-11-01T12:50:05ZJacques-Henri Jourdan`MIEnvIsEmpty` and `MIEnvTransform` have inconsistent behaviorsIn an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.In an affine logic, `MIEnvTransform` will clear the hypotheses that fail to be transformed, while `MIEnvIsEmpty` would fail if the environment is not empty. This is inconsistent.
The same remark applies to `MIEnvForall`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/175Replace booleans in proofmode typeclasses by a more informative type2019-11-01T12:51:13ZRalf Jungjung@mpi-sws.orgReplace booleans in proofmode typeclasses by a more informative typeWe have booleans in some of the proofmode typeclasses, which makes them pretty hard to read. We should use more informative types.
Right now, we seem to use booleans several times for the conditional intuitionistic modality, once for c...We have booleans in some of the proofmode typeclasses, which makes them pretty hard to read. We should use more informative types.
Right now, we seem to use booleans several times for the conditional intuitionistic modality, once for conditional affinity, and once for something completely different in `IntoLaterN`.https://gitlab.mpi-sws.org/iris/iris/-/issues/174Confusing result by `wp_op`2018-04-22T18:08:36ZRobbert KrebbersConfusing result by `wp_op`As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(W...As reported in private by @birkedal:
```coq
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
wp_op.
```
This gives
```coq
bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}
```
Pre !97 this used to work because `bin_op_eval` used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.https://gitlab.mpi-sws.org/iris/iris/-/issues/173Ambiguous reference to eqb in coq_tactics.v2018-03-12T13:17:31ZGhost UserAmbiguous reference to eqb in coq_tactics.vWhile preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theor...While preparing [Coq PR #6948](https://github.com/coq/coq/pull/6948), we noticed a little issue with `Bool.eqb` in your development. Indeed, after this PR introducing `Ascii.eqb` and `String.eqb` in the standard library, your file `theories/proofmode/coq_tactics.v` fails to compile due to 2 unqualified references to `eqb` not been seen as `Bool.eqb` anymore.
This issue can be fixed in a straightforward (and backward-compatible) way : replace the two occurrence of `eqb` in this file (lines 95 and 288) by `Bool.eqb` (or alternatively, add an `Import Bool` at the end of this file's header).
Sorry for not proposing a pull request directly, but apparently I do not have enough permission to fork on your gitlab.
For this fix to be correctly taken in account by our travis testing infrastructure, could you please update the `opam` file of repository `LambdaRust-coq.git` to mention a fixed version of `iris-coq` ? Currently it points to `iris-coq` version `dev.2018-02-23.0`, leading to commit `db735a4558ad`.
Thanks!
Pierre Letouzey