Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-10-03T10:02:54Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/353CHANGELOG should spell out what changed in auth due to views MR better2020-10-03T10:02:54ZTej Chajedtchajed@mit.eduCHANGELOG should spell out what changed in auth due to views MR better!516 makes some changes that aren't obvious. For example, `auth_validI` is gone because it used the projections, should now explicitly use `auth_auth_validI`, `auth_frag_validI`, or `auth_both_validI` as appropriate.!516 makes some changes that aren't obvious. For example, `auth_validI` is gone because it used the projections, should now explicitly use `auth_auth_validI`, `auth_frag_validI`, or `auth_both_validI` as appropriate.https://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/346Typeclass inference fails to trigger.2020-09-21T18:08:44ZArthur Azevedo de AmorimTypeclass inference fails to trigger.I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap num...I am trying to use `auth_acc`, but typeclass inference misses an apparently obvious instance that I have to provide by hand. Am I doing something wrong?
```
From stdpp Require Import base gmap.
From iris.algebra Require Import gmap numbers.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Import auth invariants.
Section Test.
Context `{!invG Σ, !authG Σ (gmapUR nat natR)}.
Implicit Types m : gmap nat nat.
Definition my_inv m : iProp Σ := True.
Goal ∀ γ, auth_ctx γ nroot id my_inv ={⊤}=∗ False.
iIntros (γ) "Hctx".
iMod (auth_empty γ) as "#Hinit".
iMod (auth_acc _ _ _ _ _ ε with "[Hctx Hinit]") as "Hinv"; try by eauto.
(* Inhabited (gmap nat nat) is now shelved... *)
Abort.
End Test.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/345Check for `options.v` should only consider files in _CoqProject2020-09-12T10:10:58ZRobbert KrebbersCheck for `options.v` should only consider files in _CoqProjectNow if I have random files in my theories folder, `make` will give errors.Now if I have random files in my theories folder, `make` will give errors.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/344Set Default Goal Selector2020-11-10T19:12:02ZRalf Jungjung@mpi-sws.orgSet Default Goal SelectorAs a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.As a follow-up to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/491, @tchajed suggested to add
```
Set Default Goal Selector "!".
```
To enforce that we properly use goal selectors.https://gitlab.mpi-sws.org/iris/iris/-/issues/343Make CI fail when proofs depend on auto-generated names2021-04-12T17:11:13ZRalf Jungjung@mpi-sws.orgMake CI fail when proofs depend on auto-generated namesWe already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.We already did it in std++, now [that this is fixed](https://github.com/coq/coq/issues/12944) it is time to do the same in Iris: make CI ensure that we do not use auto-generated names.https://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.