Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2016-11-30T12:14:50Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/44Vague iRevert error messages2016-11-30T12:14:50ZJannoVague iRevert error messagesiRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)iRevert does not report why exactly it fails (e.g. because the variable is used in a spatial assumption). It should do that. :)
(Note: ltac's revert actually has somewhat useful error messages.)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/42Authoritative with fraction2019-06-06T11:07:12ZRalf Jungjung@mpi-sws.orgAuthoritative with fractionThe authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to...The authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow *more than one* authoritative state, that all have to be brought together to change it. I just realized that this could be supported by a fairly small change in the authoritative CMRA, namely to replace `Ex(M)` by `Frac * Ag(M)`:
```
Auth(M) := { (x, a) \in (Frac * Ag(M))^? * M | ...}
```
The interface would then change to allow a fraction in the `●` notation (and once we have an infrastructure for "assertions that can be split at a fraction", it could be registered there). What do you think?
Cc @janno @robbertkrebbers @jjourdanRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/41Rewrite unexpectedly failing (Nested below |-, *, \later, -*)2016-10-28T09:07:53ZRalf Jungjung@mpi-sws.orgRewrite unexpectedly failing (Nested below |-, *, \later, -*)The rewrite at <https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66> is unexpectedly failing.
The goal is of the shape
```
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
```
and I am ...The rewrite at <https://gitlab.mpi-sws.org/FP/iris-coq/blob/ralf/broken-rewrite/heap_lang/lifting.v#L66> is unexpectedly failing.
The goal is of the shape
```
▷ ownP σ ★ ▷ (ownP σ -★ Φ v) ⊢ ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v)
```
and I am trying to rewrite backwards with `P ⊢ |={E}=> P` to remove the fancy update (behind the linear view shift notation).
Cc @robbertkrebbers could you have a look at this?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/40iRewrite and internal equality on predicates2016-10-27T14:34:24ZJannoiRewrite and internal equality on predicatesConsider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
```
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iR...Consider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
```
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iRewrite "E".
Abort.
```
It seems to me that iRewrite should succeed here. Is there a logical reason for it to fail? (As opposed to an engineering reason.)
(We are using commit 9c5a95d3b271f4e0d0c657964dfa386070d0b322 in case that matters.)https://gitlab.mpi-sws.org/iris/iris/-/issues/39iIntros: bad error when trying to use a name that's already used2016-10-26T20:07:46ZRalf Jungjung@mpi-sws.orgiIntros: bad error when trying to use a name that's already usedIf there already is a variable `x` in the context, running `iIntros (x)` yields "No applicable tactic". That's not a very useful error, and it just took me a while to realize the actual problem. Is there a way to make this show the error...If there already is a variable `x` in the context, running `iIntros (x)` yields "No applicable tactic". That's not a very useful error, and it just took me a while to realize the actual problem. Is there a way to make this show the error generated by the underlying `intros`?Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/38Refactor bigops2017-04-01T19:10:03ZRalf Jungjung@mpi-sws.orgRefactor bigopsCurrently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick *one* operator to be use...Currently, bigops are tied to CMRAs. This is silly, because it means we have to show extension for e.g. uPred (which so far we can only do after picking a silly validity), and also because it restricts us to pick *one* operator to be used in bigops, whereas we may also want to use big conjunction.
Instead we should do sth. like ssreflect does, with a typeclass/canonical structure for this special purpose that's completely separate from the main algebraic hierarchy.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/37saved_prop for predicate2016-10-05T23:07:43ZGhost Usersaved_prop for predicateI have a `Q: val -> iProp`, now I want to save predicate `Q` just like the saved proposition. How to do that?I have a `Q: val -> iProp`, now I want to save predicate `Q` just like the saved proposition. How to do that?https://gitlab.mpi-sws.org/iris/iris/-/issues/36STSs: Consider changing the def. of frame-steps2019-11-01T13:16:11ZRalf Jungjung@mpi-sws.orgSTSs: Consider changing the def. of frame-stepsJeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification...Jeehoon wrote on the iris-club list:
> the definition of s \stackrel{T}{\rightarrow} s' involves the existential quantification of T1 and T2, and I think there exists an alternative definition that does not involve that quantification:
> $(\mathcal{L}(s') # T) /\ s \rightarrow s' .$
> This is obtained by letting T1 and T2 be (\mathcal{L}(s') \setminus \mathcal{L}(s)) and (\mathcal{L}(s) \setminus \mathcal{L}(s')).
We could change `frame_step` accordingly, maybe this simplifies some things a little.https://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/34Coq induction support in proof mode2016-09-30T10:31:09ZJacques-Henri JourdanCoq induction support in proof modeThere is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.There is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/33Confusing error msg for `iTimeless`2016-10-27T14:36:30ZGhost UserConfusing error msg for `iTimeless`For example,
```
Section demo.
Context `{!heapG Σ} (N: namespace).
Lemma foo (P: iProp Σ): inv N P ⊢ WP ref #1 {{ _, True%I }}.
Proof.
iIntros "#?".
iInv N as ">H" "Hclose".
```
Here, the error info will be
...For example,
```
Section demo.
Context `{!heapG Σ} (N: namespace).
Lemma foo (P: iProp Σ): inv N P ⊢ WP ref #1 {{ _, True%I }}.
Proof.
iIntros "#?".
iInv N as ">H" "Hclose".
```
Here, the error info will be
```
Toplevel input, characters 21-44:
Ltac call to "iInv" failed.
Error: Tactic failure: iTimeless: (▷ P)%I not timeless.
```
But this is confusing, because the concern is that `P` is not timeless, not `▷ P`.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/32Support framing pure/Coq hypotheses2016-09-19T19:18:18ZJacques-Henri JourdanSupport framing pure/Coq hypothesesIn the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True.
iIntros (P) "#HP". iFrame.In the following, iFrame does not have the expected behavior:
Lemma L `{irisG Λ Σ} : ∀ P:iProp Σ, □ P ⊢ P ★ True.
iIntros (P) "#HP". iFrame.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/30Make coqchk (make verify) work2016-08-19T10:00:16ZRalf Jungjung@mpi-sws.orgMake coqchk (make verify) workCurrently, `make verify` fails with a stack overflow while checking `iris.prelude.pretty.pretty_N_inj`. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/s...Currently, `make verify` fails with a stack overflow while checking `iris.prelude.pretty.pretty_N_inj`. We had a similar issue with another lemma in the same file, and Guillaume found a work-around for it (see https://coq.inria.fr/bugs/show_bug.cgi?id=4788). Can we find a similar work-around here?
Cc @robbertkrebbers https://gitlab.mpi-sws.org/iris/iris/-/issues/28docs: the universe $\cal U$ is used without definition2016-08-16T17:40:06ZJeehoon Kangjeehoon.kang@kaist.ac.krdocs: the universe $\cal U$ is used without definitionHere: https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/model.tex#L155
Without saying that $\cal U$ is the universe (in whatever sense), the sentence seems confusing to me..Here: https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/model.tex#L155
Without saying that $\cal U$ is the universe (in whatever sense), the sentence seems confusing to me..https://gitlab.mpi-sws.org/iris/iris/-/issues/27mathpartir.sty is missing2016-08-09T13:09:45ZJeehoon Kangjeehoon.kang@kaist.ac.krmathpartir.sty is missingI believe the intention of `\usepackage{\basedir mathpartir}` in `iris.tex` is using the local `mathpartir.sty` file in the same directory. But it is missing in the repository.I believe the intention of `\usepackage{\basedir mathpartir}` in `iris.tex` is using the local `mathpartir.sty` file in the same directory. But it is missing in the repository.https://gitlab.mpi-sws.org/iris/iris/-/issues/26heap-lang CAS capability2016-10-21T20:08:42ZGhost Userheap-lang CAS capabilityCurrently, CAS can be performed on all value type, including pair. But this is not normally what real machine can do.
(However this is prevalent in a lot of simplified models?)
cc @jung Currently, CAS can be performed on all value type, including pair. But this is not normally what real machine can do.
(However this is prevalent in a lot of simplified models?)
cc @jung https://gitlab.mpi-sws.org/iris/iris/-/issues/25iSplitL "persistent_hyp": Improve error2016-08-06T00:12:25ZRalf Jungjung@mpi-sws.orgiSplitL "persistent_hyp": Improve errorCurrently, if I say `iSplitL "H"` where `H` is persistent, it says that `H` has not been found. That's confusing, "H" exists -- but it looked in the spatial context only. The tactic should either accept persistent hypotheses or the error...Currently, if I say `iSplitL "H"` where `H` is persistent, it says that `H` has not been found. That's confusing, "H" exists -- but it looked in the spatial context only. The tactic should either accept persistent hypotheses or the error should say "... has not been found in the spatial context" or so.Robbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/24Find nice syntax for our "CPS" WP specifications2016-10-27T09:23:29ZRalf Jungjung@mpi-sws.orgFind nice syntax for our "CPS" WP specificationsIt would be nice to have "something" that makes our specs more readable to someone not familiar with our "CPS" style of writing specs with an arbitrary postcondition (Φ).
I believe @janno has been working on something like that... wha...It would be nice to have "something" that makes our specs more readable to someone not familiar with our "CPS" style of writing specs with an arbitrary postcondition (Φ).
I believe @janno has been working on something like that... what was the status of that again?https://gitlab.mpi-sws.org/iris/iris/-/issues/23iFrame should support conjunction2016-08-02T15:03:03ZGhost UseriFrame should support conjunctionas in line 235 of `tests/ticket_lock.v`, the goal is in form of `H1 /\ H2 /\ ...`, and hypothesis are all in the context.
Now what I am doing is `repeat (iSplit; first by auto)`. The same effect should be achieved by a simple `iFrame`...as in line 235 of `tests/ticket_lock.v`, the goal is in form of `H1 /\ H2 /\ ...`, and hypothesis are all in the context.
Now what I am doing is `repeat (iSplit; first by auto)`. The same effect should be achieved by a simple `iFrame` as well.
cc @jung Robbert KrebbersRobbert Krebbers