Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2017-11-20T14:47:41Zhttps://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.1https://gitlab.mpi-sws.org/iris/iris/-/issues/108iIntros on pure implications stopped working2017-10-28T21:10:55ZRalf Jungjung@mpi-sws.orgiIntros on pure implications stopped workingThe following proof script used to work, but does not any more:
```
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
```
This is probably a regression of the typeclass-based iIntros?The following proof script used to work, but does not any more:
```
Goal (⌜¬False⌝ : iProp)%I.
Proof. iIntros (?). done.
```
This is probably a regression of the typeclass-based iIntros?Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/107Reverting to old (stronger) definition of atomicity2017-10-29T14:58:25ZAmin TimanyReverting to old (stronger) definition of atomicityIn Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` is *stuck*.
The old definition was: ```e``` is a...In Iris 3.0 the definition of atomicity was changed to its new definition, i.e., roughly: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` is *stuck*.
The old definition was: ```e``` is atomic if for any ```e'``` such that ```e``` reduces to ```e'``` we have that ```e'``` *is a value*.
These two definition differ (the new version is strictly weaker) in cases where we are reasoning about facts that unlike ```WP``` do not guarantee safety, e.g., ```IC``` (if convergent predicates).Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/106Iris 3.12018-01-09T15:55:25ZRalf Jungjung@mpi-sws.orgIris 3.1In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels o...In addition to what we have in the [milestone](https://gitlab.mpi-sws.org/FP/iris-coq/milestones/2), the following was suggested:
* [x] Complete the changelog.
* [x] Update the appendix.
* [x] Come to a conclusion wrt. notation levels of `_ ;; _` and `_ <- _ ;; _`
* [ ] Make sure all our CI'd reverse dependencies build with master.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/105Add some theory about the interaction of plainly and fancy updates2017-11-01T23:47:30ZRalf Jungjung@mpi-sws.orgAdd some theory about the interaction of plainly and fancy updates@amintimany has some theory there, we should get the reusable bits upstream.@amintimany has some theory there, we should get the reusable bits upstream.Iris 3.1https://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/81Let iAlways clear the spatial context2017-10-27T12:33:40ZRalf Jungjung@mpi-sws.orgLet iAlways clear the spatial contextRight now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is simil...Right now, `iAlways` complains about the spatial context being non-empty. Same for `iIntros "!#"`. IMHO it would be nice to have a way to say "please make the context empty if it isn't". I suggest for `iAlways` to do that.
This is similar to the difference between `iIntros "!>"` and `iNext` -- the latter may affect the context, the former will not. Furthermore, this is backwards compatible because iAlways will now only succeed in strictly more cases.Iris 3.1https://gitlab.mpi-sws.org/iris/iris/-/issues/59Stronger Invariant Allocation Rules2017-01-11T09:49:16ZJannoStronger Invariant Allocation RulesAllocating Iris invariants currently combines allocating and closing the invariant. I see no reason to do that other than it being somewhat convenient for 80% of the use cases. Here's a stronger invariant allocation rule that we need for...Allocating Iris invariants currently combines allocating and closing the invariant. I see no reason to do that other than it being somewhat convenient for 80% of the use cases. Here's a stronger invariant allocation rule that we need for our GPS work. This is not (yet) a pull request for - just a copy of my local file. But I wanted to dump this here so that you guys can discuss if you want it in Iris.
```
From iris.base_logic.lib Require Export own wsat.
From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
From iris.base_logic.lib Require Export fancy_updates namespaces.
From iris.base_logic.lib Require Import wsat invariants.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Section wsat.
Import invG.
Context `{invG Σ}.
Implicit Types P : iProp Σ.
Lemma ownI_alloc_strong φ P :
(∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
Proof.
iIntros (Hfresh) "Hw". iDestruct "Hw" as (I) "[? HI]".
iMod (own_empty (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "HD") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
intros E. destruct (Hfresh (E ∪ dom _ I))
as (i & [? HIi%not_elem_of_dom]%not_elem_of_union & ?); eauto. }
iDestruct "HD" as (X) "[Hi HD]"; iDestruct "Hi" as %(i & -> & HIi & ?).
iMod (own_update with "Hw") as "[Hw HiP]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ i (invariant_unfold P)); last done.
by rewrite /= lookup_fmap HIi. }
iModIntro; iExists i; iSplit; [done|]. rewrite /ownI; iFrame "HiP".
rewrite -/(ownD _). iFrame "HD".
iIntros "HE". iExists (<[i:=P]>I); iSplitL "Hw".
{ by rewrite fmap_insert insert_singleton_op ?lookup_fmap ?HIi. }
iApply (big_sepM_insert _ I); first done.
iFrame "HI". by iRight.
Qed.
End wsat.
Section invariants.
Import uPred.
Context `{invG Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
Lemma ownE_proper : Proper ((≡) ==> (≡)) ownE.
Proof.
rewrite /ownE => ? ? Eq. f_equiv. f_equiv. by apply leibniz_equiv.
Qed.
Lemma inv_alloc_strong N E P : ↑N ⊆ E → True ={E, E∖↑N}=∗ inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
rewrite inv_eq /inv_def fupd_eq /fupd_def.
iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_strong (∈ ↑ N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
- intros Ef. exists (coPpick (↑ N ∖ coPset.of_gset Ef)).
rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
apply coPpick_elem_of=> Hfin.
eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
apply of_gset_finite.
- iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
{ rewrite -?ownE_op; [|set_solver|set_solver]. rewrite ownE_proper; [done|].
rewrite assoc. rewrite <-!union_difference; set_solver. }
iModIntro. rewrite /uPred_except_0. iRight. iFrame.
iSplitL "Hw HEi".
+ by iApply "Hw".
+ iSplitL "Hi"; [eauto|].
iIntros "HP [Hw HE\N]".
iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
iModIntro. iRight. iFrame. iSplitL; [|done].
iCombine "HEi" "HEN\i" as "HEN".
iCombine "HEN" "HE\N" as "HE".
rewrite -?ownE_op; [|set_solver|set_solver].
rewrite ownE_proper; [done|].
rewrite <-!union_difference; set_solver.
Qed.
End invariants.
```Iris 3.0Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/56iAssert ... as %X should get all assumptions2017-01-03T13:28:17ZRalf Jungjung@mpi-sws.orgiAssert ... as %X should get all assumptionsWhen I write `iAssert ... as %X`, it is syntactically clear that I am proving sth. persistent (even pure). Still, I have to add `with [#]` to be allowed to use all assumptions. Wouldn't it make sense to do that automatically? IIRC we ar...When I write `iAssert ... as %X`, it is syntactically clear that I am proving sth. persistent (even pure). Still, I have to add `with [#]` to be allowed to use all assumptions. Wouldn't it make sense to do that automatically? IIRC we are doing sth. like that with ´iDestruct ... as %X`.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/55iNext unfolds things (more than simpl) even when there is no later to strip2018-02-20T00:50:15ZRalf Jungjung@mpi-sws.orgiNext unfolds things (more than simpl) even when there is no later to stripSee <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40>: The context goas from
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : elctx_interp E qE
"HL" ...See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/02ef8176f01f8de0563a2f5a8e1444bb9ee01b6d/theories/typing/cont.v#L40>: The context goas from
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : elctx_interp E qE
"HL" : llctx_interp L1 1
"HT" : tctx_interp tid (T' args)
```
to
```
"HC" : elctx_interp E qE -∗ cctx_interp tid C
"HE" : [∗ list] k↦x ∈ E, (λ (_ : nat) (x0 : elctx_elt), elctx_elt_interp x0 qE) k x
"HL" : [∗ list] k↦x ∈ L1, (λ (_ : nat) (x0 : llctx_elt), llctx_elt_interp x0 1) k x
"HT" : [∗ list] k↦x ∈ T' args, (λ (_ : nat) (x0 : tctx_elt), tctx_elt_interp tid x0) k x
```
but no later is removed. Not even simpl unfolds these definitions.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/54iIntros fails to introduce Coq-level and Iris-level universal quantifiers at ...2016-12-21T19:01:39ZRalf Jungjung@mpi-sws.orgiIntros fails to introduce Coq-level and Iris-level universal quantifiers at onceSee for example <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ca917d76e1318fb3a6e0aa0c61f777a2e62ac8d0#51956c642cbeef54a2f1728f704193c7e23720f3_97_98>: `iIntros (HTsat HEsat). iIntros (tid qE) "#LFT HE HL HC".` works but `iIntros ...See for example <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ca917d76e1318fb3a6e0aa0c61f777a2e62ac8d0#51956c642cbeef54a2f1728f704193c7e23720f3_97_98>: `iIntros (HTsat HEsat). iIntros (tid qE) "#LFT HE HL HC".` works but `iIntros (HTsat HEsat tid qE) "#LFT HE HL HC".` does not.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/52iMod and evar instantiation2019-06-17T07:54:22ZRalf Jungjung@mpi-sws.orgiMod and evar instantiationSee <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391>: `iMod ... as [$ ?]` fails even though `iMod ... as [H ?]; iFrame "H"` works fine.
@jjourdan suggests it may be related to C...See <https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/acddfae5355a5e7540010c7ea6f423a892f9e887#note_17391>: `iMod ... as [$ ?]` fails even though `iMod ... as [H ?]; iFrame "H"` works fine.
@jjourdan suggests it may be related to Coq lazily propagating instantiated evars, and adding a magic tactic that does the propagation in the right point of executing the `iMod` could help.Iris 3.0Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/50`contains` is named the wrong way around2017-01-14T21:53:11ZRalf Jungjung@mpi-sws.org`contains` is named the wrong way around``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.``l1 `contains` l2`` confusing expresses that `l2` contains `l1`. Either the order of arguments should be changed, or the notation should be changed to e.g. `contained`.Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/47Use opam-based CI2016-12-14T13:19:40ZRalf Jungjung@mpi-sws.orgUse opam-based CII'd like to use the same opam-based CI setup that we also use for lambdaRust. This will also make it trivial for us to run the CI with both Coq 8.5 and 8.6, and to change Coq versions in the future (no changes in the CI image needed for ...I'd like to use the same opam-based CI setup that we also use for lambdaRust. This will also make it trivial for us to run the CI with both Coq 8.5 and 8.6, and to change Coq versions in the future (no changes in the CI image needed for this any more, yay :D ).
However, to make that work, we have to stop importing `.` in `_CoqProject`. So like in lambdaRust, I'd like to move everything into a subfolder `theories/`.
This will break all merge requests, so we should get at least some of them in. !30 will hang around for a while, so whatever. But I'd like to wait until we get at least !25 or !22 in.Iris 3.0Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/iris/-/issues/35Renaming things2016-11-09T12:42:38ZRalf Jungjung@mpi-sws.orgRenaming thingsThere are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
* `◇`: After a lot of discussion about `except_last` vs. `except_now`, we agreed that depending on whether y...There are some names some of us are not happy with. This issue is just meant to track the latest status in these discussions.
* `◇`: After a lot of discussion about `except_last` vs. `except_now`, we agreed that depending on whether you look at the adequacy theorem or the state at some point of the proof, either may make sense. We all agreed that `except_0` would be acceptable.
* `≡`: I still plan to rename this from `uPred_eq` to `uPred_internal_eq`.
* The lowest-level view shift... my latest suggestion was
```
|=u=> Q update modality
|={E1,E2}=> Q view modality
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
or
```
|=s=> Q state update (modality)
|={E1,E2}=> Q view update (modality)
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
I couldn't find JH's last proposal. Robbert expressed that he liked Derek's:
```
|=p=> Q primitive shift
|={E1,E2}=> Q primitive view shift
P ={E1,E2}=> Q view shift
P ={E1,E2}=★ Q linear view shift
```
However, my concern here is that it becomes hard to say that we want a
"primitive non-view shift". Also, the "primitive view shift" is not
primitive...
* Filenames:
```
base_logic/upred [just the definition, metric space, functors]
base_logic/primitive [primitive connectives and proofs in the model]
base_logic/base_logic or base_logic/logic [upred + primitive + derived connectives/rules]
```Iris 3.0https://gitlab.mpi-sws.org/iris/iris/-/issues/569Add some sort of rule for `own ∧ own`2024-03-24T14:54:23ZRalf Jungjung@mpi-sws.orgAdd some sort of rule for `own ∧ own`The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v)...The leaf paper has this:
![image](/uploads/0beb1bc5d161b30abf37f549c5b0841f/image.png)
(Coq formalization [here](https://github.com/secure-foundations/leaf/blob/a51725deedecc88294057ac1502a7c7ff2104a69/src/guarding/conjunct_own_rule.v).)
Amin suggested [something similar](https://mattermost.mpi-sws.org/iris/pl/tcsex43cn7d5ij5qwkk39ftd7h) a long time ago.
Not sure which formulation works best, but we should have something like that. :)
Whatever the rule is, it should be strong enough to prove things like
```
Lemma pointsto_and_sep (l1 l2:loc) (v1 v2:val) :
l1 ≠ l2 ->
l1 ↦ v1 ∧ l2 ↦ v2 -∗
l1 ↦ v1 ∗ l2 ↦ v2.
Lemma pointsto_and_eq l x y :
l ↦ x ∧ l ↦ y -∗ ⌜x = y⌝
```https://gitlab.mpi-sws.org/iris/iris/-/issues/568[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-18T16:04:50ZRomain Tetley[coq-iris-heap-lang] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.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 appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.
Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.19, **preferably before March 31st, 2024**?
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 March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
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/405https://gitlab.mpi-sws.org/iris/iris/-/issues/567[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.012024-03-19T16:06:15ZRomain Tetley[coq-iris] Please create a tag for Coq 8.19 in Coq Platform 2024.01The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be...The Coq team released Coq `8.19.0` on January 24th, 2024.
The corresponding Coq Platform release `2024.01` should be released before **April 30th, 2024**.
It can be delayed in case of difficulties until May 15th, 2024, but this should be an exception.
This issue is to inform you that to our (possibly a few days old) best knowledge the latest released version of your project (4.1.0) **does not work** with Coq `8.19.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
7c5ce0d556f4e03f27ddc6463462bf4040f5103d 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.19, **preferably before March 31st, 2024**?
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 March 31st, 2024, it will be included in an early Coq Platform beta release of the for Coq 8.19.0.
The working branch of Coq Platform, can be found here [main](https://github.com/coq/platform/tree/main).
It contains package pick [`~8.19~2024.01+beta1`](https://github.com/coq/platform/tree/main/package_picks/package-pick-8.19~2024.01+beta1.sh) which already supports Coq version `8.19.0` and contains already working (possibly patched / commit pinned) Coq Platform packages.
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/405https://gitlab.mpi-sws.org/iris/iris/-/issues/566Frame instance for multiset union can interact badly with instantiating exist...2024-03-06T12:32:05ZIke MulderFrame instance for multiset union can interact badly with instantiating existential quantifiersThis is problematic:
```coq
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail ...This is problematic:
```coq
From iris.proofmode Require Import proofmode.
Section test.
Context {PROP : bi}.
Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
Proof.
iIntros "HP".
Fail Timeout 2 iFrame "HP".
Abort.
End test.
```
This happens because there is the following frame instance for framing inside a multiset union:
```coq
Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.
```
In our `multiset_problem` example, this instance will instantiate the evar `?X` with a union `?X1 ⊎ ?X2`. After two more steps, we encounter almost the same goal, and `Frame` instance search will loop.
The instances for `[∗ list]` do not suffer from this problem, since they are guarded by an `IsCons` or `IsApp` typeclass with proper `Hint Mode`s.
To fix this, we could use the same approach: guard `frame_big_sepMS_disj_union` with a new class `IsUnion`.
Encountered by @janno @lepigrehttps://gitlab.mpi-sws.org/iris/iris/-/issues/565Unsound instantiation of existentials by `iFrame` on persistent facts2024-03-05T17:01:36ZRodolphe LepigreUnsound instantiation of existentials by `iFrame` on persistent facts@janno and I found that the new support for existential instantiation in `iFrame` (from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Repr...@janno and I found that the new support for existential instantiation in `iFrame` (from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1017) can sometimes instantiate existential quantifiers too eagerly for persistent facts.
Reproducing example:
```coq
Require Import iris.bi.interface.
Require Import iris.proofmode.proofmode.
Goal ∀ (PROP : bi) (P : nat -> PROP),
□ P 0 ⊢ P 0 ∗ (∀ n : nat, P n -∗ ∃ n, P n ∗ ⌜n = 1⌝).
Proof.
iIntros (??) "#$".
(*
PROP : bi
P : nat → PROP
============================
_ : P 0
--------------------------------------□
∀ x : nat, P x -∗ ⌜0 = 1⌝
*)
Abort.
```