Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-10-20T15:11:03Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/355Break dependency of algebra on base_logic2020-10-20T15:11:03ZRalf Jungjung@mpi-sws.orgBreak dependency of algebra on base_logicCurrently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separ...Currently, parts of algebra depend on base_logic for the "internalized" equality and validity lemmas. That is rather annoying as it means many things need to be recompiled to work on those parts of algebra. It also prevents us from separating the base_logic and program_logic folders into a separate package, should we ever want to do that.
The plan is to instead add a file like `base_logic/algebra.v` and prove those lemmas there, thus fixing the dependency inversion.https://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/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/333Iris Library Best Practices2020-08-06T16:37:12ZRalf Jungjung@mpi-sws.orgIris Library Best PracticesWe should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered for...We should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @blaisorblade pointed out that it is non-obvious that specs should not contain `own` but instead wrap those things in their own definitions that depend on `libG` instead of `inG`.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/327Add RA for auth max_nat2020-10-27T19:49:24ZRobbert KrebbersAdd RA for auth max_natAs @tchajed pointed out, this RA is quite commonly used. While porting developments as a consequence of !461 I noticed it's also used in ReLoC.
So, concretely, there are the following uses:
- Iris: https://gitlab.mpi-sws.org/iris/iris/...As @tchajed pointed out, this RA is quite commonly used. While porting developments as a consequence of !461 I noticed it's also used in ReLoC.
So, concretely, there are the following uses:
- Iris: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/heap_lang/lib/counter.v#L16
- ReLoC: https://gitlab.mpi-sws.org/iris/reloc/-/blob/7dca8f9472290626ac5174d5789512234ce115e9/theories/examples/symbol.v#L49
- Perennial: https://github.com/mit-pdos/perennial/blob/master/src/algebra/fmcounter.v
Would be good to add it to `algebra/lib` so people don't reprove the same stuff all the time.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?