Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-09-10T17:45:28Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/342Missing {u,}rFunctors and conversions2020-09-10T17:45:28ZPaolo G. GiarrussoMissing {u,}rFunctors and conversionsSome missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable throu...Some missing utilities I noticed:
- there's no conversion function from `urFunctor` (COFE -> uCMRA) to an `rFunctor` (COFE -> CMRA), and an `rFunctor` to an `oFunctor` (COFE -> OFE)
- `gmapRF` does not exist and should be definable through the above conversion, and @jung suggests that's an oversight; OTOH, that alerted me to a bug; I only needed it because I tried writing `GFunctor (gmapRF ...)`, which does not seem useful
- `listRF` does not exist (which I noticed while grepping)https://gitlab.mpi-sws.org/iris/iris/-/issues/337Weird automatically generated names2020-08-12T16:46:47ZRobbert KrebbersWeird automatically generated namesAfter @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatic...After @tchajed's !479 the following happens:
```coq
Lemma foo {PROP : bi} : ⊢@{PROP} ∃ _ : True, ⌜ 0 = 0 ⌝.
Proof. by iExists I. Qed.
Lemma bar {PROP : bi} : ⊢@{PROP} True.
Proof. iDestruct foo as (?) "?".
```
This names the automatically generated hypothesis `x`.
```
1 subgoal
PROP : bi
x : True
______________________________________(1/1)
_ : ⌜0 = 0⌝
--------------------------------------□
True
```
I don't understand where the name `x` comes from, but it's very annoying. The `∃ _ : ..., ...` pattern is often used for `inG`, and the `inG` being called `x` is very annoying. It prevents one from using `x` for other variables.
Obviously, in this case I could use `iDestruct foo as (name_for_my_inG) "?"`, but I really don't want to name that hypothesis.https://gitlab.mpi-sws.org/iris/iris/-/issues/336Use user-supplied names in iIntros (?)2020-08-12T16:46:47ZTej Chajedtchajed@mit.eduUse user-supplied names in iIntros (?)Similar to !479, the proof mode should preserve user names in binders in `iIntros (?)`.
This depends on !479 since there's some common infrastructure for representing and threading identifiers through typeclasses.Similar to !479, the proof mode should preserve user names in binders in `iIntros (?)`.
This depends on !479 since there's some common infrastructure for representing and threading identifiers through typeclasses.https://gitlab.mpi-sws.org/iris/iris/-/issues/334Expand test coverage of proofmode2021-12-16T22:21:12ZTej Chajedtchajed@mit.eduExpand 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/328Add RA for auth of a heap2020-10-12T15:45:22ZRalf Jungjung@mpi-sws.orgAdd RA for auth of a heap`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in I...`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in Iris. ;)
The only open question for me is, what is `Y`? (`X` is any countable type.)
* We probably should have fractions, so that would be `Y := frac * agree T`. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives `False`).
* @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with `Y := agree T`, or we could do the strictly more powerful thing (subsuming both of the above) and do `Y := (frac * agree T) + agree T`. I *think* with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.https://gitlab.mpi-sws.org/iris/iris/-/issues/325iSpecialize with "[% //]" does not report an error if done fails2020-06-26T10:51:38ZTej Chajedtchajed@mit.eduiSpecialize with "[% //]" does not report an error if done failsiSpecialize on `SPureGoal true` does not report an error message.
```coq
From iris Require Import proofmode.tactics.
Theorem test {PROP: bi} (P: PROP) :
(⌜False⌝ -∗ P) -∗
P.
Proof.
iIntros "Hwand".
iSpecializePat_go "Hwand" [sp...iSpecialize on `SPureGoal true` does not report an error message.
```coq
From iris Require Import proofmode.tactics.
Theorem test {PROP: bi} (P: PROP) :
(⌜False⌝ -∗ P) -∗
P.
Proof.
iIntros "Hwand".
iSpecializePat_go "Hwand" [spec_patterns.SPureGoal true] (* with "[% //]" *).
Abort.
```
The reason is that this match is failing: https://gitlab.mpi-sws.org/iris/iris/-/blob/11f9d567c2a8b1f52d00e562d5cc39262463cf9e/theories/proofmode/ltac_tactics.v#L849. It should have another case that prints the normal Coq goal rather than the IPM goal.https://gitlab.mpi-sws.org/iris/iris/-/issues/324Add "nat+min" RA2020-06-18T11:20:17ZRalf Jungjung@mpi-sws.orgAdd "nat+min" RAWe have an RA `mnat` for `nat` with "max" as composition. But we don't have one with "min". It would probably make sense to add that.
But how should we name things? `mnat` isn't great as `m` could be min or max...We have an RA `mnat` for `nat` with "max" as composition. But we don't have one with "min". It would probably make sense to add that.
But how should we name things? `mnat` isn't great as `m` could be min or max...https://gitlab.mpi-sws.org/iris/iris/-/issues/322Operator precedence in heap lang is wrong2020-05-28T13:50:42ZDmitry KhalanskiyOperator precedence in heap lang is wrongThe Iris version is dev.2020-05-18.2.fdda97e8.
Given the definition
```
Definition v: expr := #true || #false = #false.
```
I expect it to read the same as in most other languages: "Either `true` is true or `false` is equal to `false`"....The Iris version is dev.2020-05-18.2.fdda97e8.
Given the definition
```
Definition v: expr := #true || #false = #false.
```
I expect it to read the same as in most other languages: "Either `true` is true or `false` is equal to `false`". However, `Print v` shows:
```
v = ((if: #true then #true else #false) = #false)%E
: expr
```
In other words, `||` has higher precedence than comparisons. I'm not familiar with how exactly notations in Coq are specified, but, looking at `notation.v`, it seems that precedence for common operators is not specified explicitly but is instead inherited from other notations that are known to Coq, and in vanilla Coq `=` has low precedence, given its role.https://gitlab.mpi-sws.org/iris/iris/-/issues/319Fix "omega is deprecated" warnings by switching to lia2020-05-16T17:14:49ZTej Chajedtchajed@mit.eduFix "omega is deprecated" warnings by switching to liaOn Coq v8.12+alpha there are a few new warnings from uses of `omega`, which should be replaced with `lia`. This might be a little annoying to make compatible with Coq v8.9, since `lia` has gotten progressively more powerful.On Coq v8.12+alpha there are a few new warnings from uses of `omega`, which should be replaced with `lia`. This might be a little annoying to make compatible with Coq v8.9, since `lia` has gotten progressively more powerful.https://gitlab.mpi-sws.org/iris/iris/-/issues/318Drop support for Coq 8.9?2020-08-24T08:47:06ZRalf Jungjung@mpi-sws.orgDrop support for Coq 8.9?Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`...Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`)
* `change_no_check` (to stop using deprecated `convert_concl_no_check`)
* `Declare Scope` (to fix deprecated use of undeclared scopes)
Is there more?https://gitlab.mpi-sws.org/iris/iris/-/issues/315Port HeapLang tactics to more efficient style2020-07-15T19:27:00ZRobbert KrebbersPort HeapLang tactics to more efficient styleThe heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248The heaplang tactics do not use the `match` trick to avoid additional proof mode context arguments. They should be rewritten in the style in https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/248https://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/313Add deallocation operation to HeapLang2020-05-25T16:01:10ZRalf Jungjung@mpi-sws.orgAdd deallocation operation to HeapLangIt would be great if HeapLang would also support deallocation, to enable reasoning about programs that perform explicit deallocation. To support the `meta` mechanism we have to ensure that locations never get reused but that seems fine -...It would be great if HeapLang would also support deallocation, to enable reasoning about programs that perform explicit deallocation. To support the `meta` mechanism we have to ensure that locations never get reused but that seems fine -- we do not have ptr-int-casts.
We *do* have ptr equality tests though. I am not sure if we are willing to demand that locations must not have been deallocated yet for them to be comparable -- that makes ptr equality a memory-dependent operation, which is quite the pain. Maybe it is okay to not be super realistic in this regard?https://gitlab.mpi-sws.org/iris/iris/-/issues/311Document side-effects of importing Iris2020-09-29T16:33:55ZRalf Jungjung@mpi-sws.orgDocument side-effects of importing IrisIris should have something [like std++ has](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects) where we document its global, Coq-level side-effects.Iris should have something [like std++ has](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects) where we document its global, Coq-level side-effects.https://gitlab.mpi-sws.org/iris/iris/-/issues/309Fix name duplication `elem_of_list_singleton` in Iris and std++2020-07-15T09:36:22ZRobbert KrebbersFix name duplication `elem_of_list_singleton` in Iris and std++See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47923See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47923Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/307`iIntros "%"` no longer works with universal quantification2020-04-07T15:39:37ZRalf Jungjung@mpi-sws.org`iIntros "%"` no longer works with universal quantificationThis test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebber...This test used to pass until yesterday, but got broken by !400:
```
Section tests.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Lemma test_iIntros_forall_pure P :
⊢ ∀ x : nat, P.
Proof. iIntros "%". Abort.
```
Cc @robbertkrebbers @tchajedhttps://gitlab.mpi-sws.org/iris/iris/-/issues/306Iris 3.3 release planning2020-07-15T16:05:09ZRalf Jungjung@mpi-sws.orgIris 3.3 release planningWhat needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed s...What needs to happen for the release:
* [x] Add things we want to do to [the milestone](https://gitlab.mpi-sws.org/iris/iris/-/milestones/5).
* [x] Do all the things in the milestone.
* [x] Complete the CHANGELOG
* [x] Complete the sed script in the CHANGELOG.
* [x] Release a matching std++.
* [x] Write announcement.
* [x] Release opam packages on coq opam registry.
* [x] Send out announcements.Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/305Update `proof_mode.md` for !4002020-04-07T15:59:09ZRobbert KrebbersUpdate `proof_mode.md` for !400Iris 3.3https://gitlab.mpi-sws.org/iris/iris/-/issues/302Notation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` broken2020-05-24T12:55:45ZRobbert KrebbersNotation `(⊢@{PROP})` and `(⊣⊢@{PROP} )` brokenSee https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/396#note_46604
Apparently https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/384 did break these notations...
Minimized example. The following works:
```coq
Notation "(⊢@{ P...See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/396#note_46604
Apparently https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/384 did break these notations...
Minimized example. The following works:
```coq
Notation "(⊢@{ PROP } )" := (eq (A:=PROP)) (only parsing).
Definition test PROP := (⊢@{PROP}).
```
But the following doesn't:
```coq
Notation "('⊢@{' PROP } )" := (eq (A:=PROP)) (only parsing).
Definition test PROP := (⊢@{PROP}).
(* Syntax Error: Lexer: Undefined token *)
```
/cc @Blaisorblade @gmalechahttps://gitlab.mpi-sws.org/iris/iris/-/issues/301`iExists` ignores `Opaque`2020-03-30T11:52:39ZPaolo G. Giarrusso`iExists` ignores `Opaque`Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Defi...Probably a WONTFIX, but this is new (presumably from !372), and Robbert asked for an example.
```coq
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import iprop.
Section foo.
Context `(Σ : gFunctors).
Definition foo : iProp Σ := ∃ (x : nat), x ≡ 0.
End foo.
Opaque foo.
Lemma bar Σ : ⊢ foo Σ .
Proof.
by iExists 0. Restart.
iStartProof.
eapply coq_tactics.tac_exist.
Fail apply (class_instances_bi.from_exist_exist _).
(* The Hint Extern from !372: *)
notypeclasses refine (class_instances_bi.from_exist_exist _).
(* apply: (class_instances_bi.from_exist_exist _). (* Also works *) *)
by eexists 0.
Qed.
```