Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-07-07T11:02:38Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/426Notation `≼@{A}` is missing2021-07-07T11:02:38ZRobbert KrebbersNotation `≼@{A}` is missingWe are probably missing such notations for more relations. It would be good to do a sweep.We are probably missing such notations for more relations. It would be good to do a sweep.https://gitlab.mpi-sws.org/iris/iris/-/issues/229Odd Behavior for Substitution2020-03-12T21:08:39ZDaniel GratzerOdd Behavior for SubstitutionHello,
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
```
Definition tryset ...Hello,
Simon noticed a somewhat odd occurrence with substitution today. Apparently values are no longer required to be closed (?) but defining a value which is open seems to break substitution in a confusing way?
```
Definition tryset : val :=
λ: "n",
CAS "x" NONE (SOME "n").
Definition check : val :=
λ: <>,
let: "y" := !"x" in λ: <>,
match: "y" with
NONE => #()
| SOME "n" =>
match: !"x" with
NONE => assert: #false
| SOME "m" => assert: "n" = "m"
end
end.
Definition mk_oneshot : val := λ: <>,
let: "x" := ref NONE in (tryset, check).
```
With this example program we have separated out `tryset` and `check` even though they both depend on `"x"`. However, when proving some properties about `mk_oneshot` substituting `"x"` for a new location `#l` does not replace `"x` in either.
This behavior is demonstrated by the attached file: [oneshot.v](/uploads/cc01dea007082db718057bb66ad87c88/oneshot.v). Am I missing something obvious here?https://gitlab.mpi-sws.org/iris/iris/-/issues/436opam package description is not helpful2021-10-26T21:59:09ZMichael Soegtropopam package description is not helpfulThe package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_l...The package description for the coq-iris and coq-iris-heaplang opam packages is not helpful:
```
This package provides the iris.heap_lang Coq module.
This package provides the following Coq modules:niris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_logic, iris.program_logic.
```
The description should more elaborate on the question what this can be used for.
See (https://coq.inria.fr/opam/released/packages/coq-iris/coq-iris.3.4.0/opam)
See (https://coq.inria.fr/opam/released/packages/coq-iris-heap-lang/coq-iris-heap-lang.3.4.0/opam)
Please note that (afaik) it is no issue to change the description of opam packages without creating a new version.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/349Parameterize WP (and more) by the notion of fancy update2020-09-22T07:47:46ZRalf Jungjung@mpi-sws.orgParameterize WP (and more) by the notion of fancy updateFor Perennial, @jtassaro developed a notion of "fancy updates" that satisfies all the laws we have in Iris, plus way more. Unfortunately this means we cannot directly use anything from `base_logc/lib` and above, even though all these pro...For Perennial, @jtassaro developed a notion of "fancy updates" that satisfies all the laws we have in Iris, plus way more. Unfortunately this means we cannot directly use anything from `base_logc/lib` and above, even though all these proofs do go through unchanged.
This change is likely not canonical enough to be upstreamable, and I see no way to make our notion of fancy updates itself general enough that @jtassaro's update are an instance of them. The design space is very wide open here.
It would thus be useful if we could parameterize the definition of WP by the notion of fancy update, and similar for some of the things in `base_logic/lib` -- everything that mentions fancy updates, basically (or at least anything useful; I don't think it is worth doing this with STS and auth). Maybe some things can be changed to use basic updates instead of fancy updates, which would avoid the need for parameterization.
Even semantic invariants themselves can be defined generally for any fancy update; the only thing that each update would need to prove is the allocation lemma(s).
@robbertkrebbers what do you think?https://gitlab.mpi-sws.org/iris/iris/-/issues/297Persistent (and other BI class) instances missing for telescopes2020-03-05T18:44:04ZRobbert KrebbersPersistent (and other BI class) instances missing for telescopeshttps://gitlab.mpi-sws.org/iris/iris/-/issues/242Planning the Iris 3.2 release2019-11-01T12:31:44ZRalf Jungjung@mpi-sws.orgPlanning the Iris 3.2 releaseI have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I...I have finally gotten around to update the documentation for the Iris 3.2 changes. Turns out that wasn't actually that much work as heap_lang is not part of the formal documentation.
That removes the last blocker for a new release! So I think we should make that release soon-ish. Are there any issues or MRs that you think should be included? Let's collect them in [this milestone](https://gitlab.mpi-sws.org/iris/iris/milestones/4).
We might consider doing the release after the POPL deadline so that our Iris-using POPL submissions (if any) can claim to be compatible with Iris 3.2. But honestly I don't think that is a big factor, the artifacts should anyway bundle the right version of Iris -- and I'd rather avoid extra coordination overhead if possible.
After the release:
* [ ] Drop support for Coq 8.7, and enable the `sigT`-functor notation (at the bottom of `ofe.v`).Iris 3.2https://gitlab.mpi-sws.org/iris/iris/-/issues/435Please create a tag for Coq 8.14 in Coq Platform 2021.112021-11-14T18:33:05ZMichael SoegtropPlease create a tag for Coq 8.14 in Coq Platform 2021.11The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of di...The Coq team released Coq 8.14+rc1 on September 17, 2021 and plans to release Coq 8.14.0 before October 31, 2021.
The corresponding Coq Platform release 2021.11 should be released before November 30, 2021.
It can be delayed in case of difficulties until January 31, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.4.0) does not work with Coq 8.14+rc1.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
ee6a36b3e803ebec465bf44bb5bcbf9b19fe6b62 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag, or communicate us any existing tag that works with Coq branch v8.14, preferably before November 15, 2021?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
The working branch of Coq Platform, which already supports Coq version 8.14+rc1, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/139https://gitlab.mpi-sws.org/iris/iris/-/issues/443Please create a tag for Coq 8.15 in Coq Platform 2022.022022-01-20T19:17:09ZMichael SoegtropPlease create a tag for Coq 8.15 in Coq Platform 2022.02The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an excep...The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (3.5.0) does not work with Coq 8.15.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.
Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI is currently testing commit
bb946806c5aa9bcb8184a8cb3bc1befecc0322a0 on repository https://gitlab.mpi-sws.org/iris/iris
https://gitlab.mpi-sws.org/iris/examples - which likely means that this commit does work in Coq CI.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.15, preferably before February 14, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.
In case the tag and opam package are available before January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.
The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.
Please **don't** close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.
In any case, Coq Platform won't be released before this issue is closed!
Thanks!
P.S.: this issue has been created automatically based on CI status.
CC: https://github.com/coq/platform/issues/193Tej Chajedtchajed@mit.eduTej Chajedtchajed@mit.eduhttps://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-22T19:06:03ZDan FruminPolymorphic equality for HeapLangIt would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.It would be nice to have polymorphic equality testing, like in OCaml or StandardML.
Current equality testing is used both for CmpXchng and for `=`, so it only operates on unboxed values.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/290Possible redesign of handling of persistent/intuitionistic propositions in in...2020-02-11T17:35:16ZRalf Jungjung@mpi-sws.orgPossible redesign of handling of persistent/intuitionistic propositions in intro patternsAt https://gitlab.mpi-sws.org/iris/iris/merge_requests/370#note_43784 we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when `#` is needed and when not) with the goal of being mor...At https://gitlab.mpi-sws.org/iris/iris/merge_requests/370#note_43784 we had some discussion about possible re-designs of the handling of persistent/intuitionistic propositions (when `#` is needed and when not) with the goal of being more consistent. That was put on hold for now due to being too much work and likely also breaking many things; the issue here tracks possibly doing at least some of that in the future if we want to improve the situation around the `#` pattern (and its opt-out version, whatever that will be).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/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/442Potentially add Frame instances for all our Fractional instances2022-01-17T02:02:14ZRalf Jungjung@mpi-sws.orgPotentially add Frame instances for all our Fractional instancesIn https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
...In https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/739 we have removed the general `frame_fractional` instance and replaced it by connection-specific framing instances such as:
```
Global Instance frame_mapsto p l v q1 q2 RES :
FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
```
This is useful since it matches on the head symbol of the framed expression, which is a lot more efficient than `frame_fractional`.
However, we have more `Fractional` instances in the codebase, which for now do not support framing any more:
* `Fractional (λ q, mono_nat_auth_own γ q n)`
* `Fractional (λ q, gset_bij_own_auth γ (DfracOwn q) L)`
* `Fractional (λ q, k ↪[γ]{#q} v)` (for `ghost_map`)
* `Fractional (λ q, ghost_map_auth γ q m)`
* `Fractional (λ q, ghost_var γ q a)`
* `Fractional (cinv_own γ)`
If the need comes up, we should add them back. Also, if it was easier to add them (e.g. with some kind of macro), there'd be less hesitation to add these instances everywhere.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/85Proof mode goals in empty context cannot be distinguished from Coq goals2017-05-19T15:20:29ZRobbert KrebbersProof mode goals in empty context cannot be distinguished from Coq goals@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We...@jung noted this problem somewhere in lambdarust, see below for a simple example:
```coq
From iris Require Import proofmode.tactics.
Goal forall M (P : uPred M), P ⊣⊢ P.
Proof.
intros; iSplit.
(* Goals look like `P → P` *)
```
We could add some special symbol to the proof mode notation with the empty context? Any suggestions?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/43Proof mode intro pattern lexer: _ should be allowed as part of varianme names2016-11-24T08:27:45ZRalf Jungjung@mpi-sws.orgProof mode intro pattern lexer: _ should be allowed as part of varianme names`A_B` is a fine variable name. It is parsed as `A _ B`.`A_B` is a fine variable name. It is parsed as `A _ B`.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://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/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.1