Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2018-08-24T16:40:02Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/208Import Coq.Strings.Ascii before using ascii notations2018-08-24T16:40:02ZGhost UserImport Coq.Strings.Ascii before using ascii notationsI don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/5...I don't know how to fork a repo on gitlab (the button is grayed out), and I don't know how to make a merge request here from a branch on github, so I'm creating an issue instead for merging https://github.com/JasonGross/iris-coq/commit/57743dd702b4c09b6e8d7cd171c0d7852d1da39a / https://github.com/JasonGross/iris-coq/compare/fix-for-8064
Import prim token notations before using them
This is required for compatibility with
coq/coq#8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.
c.f. coq/coq#8064 (comment)
All changes were made via
https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-pyhttps://gitlab.mpi-sws.org/iris/iris/-/issues/207Rule "Res-Alloc" in documentation is stronger than the Coq version2019-03-06T09:54:29ZJoseph TassarottiRule "Res-Alloc" in documentation is stronger than the Coq versionIn the rule "Res-alloc" on page 26 of the documentation (see https://plv.mpi-sws.org/iris/appendix-3.1.pdf, or https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/ghost-state.tex#L211) the set for the new ghost name is allowed to be ...In the rule "Res-alloc" on page 26 of the documentation (see https://plv.mpi-sws.org/iris/appendix-3.1.pdf, or https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/docs/ghost-state.tex#L211) the set for the new ghost name is allowed to be an arbitrary infinite set.
However, what's proved here (https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/base_logic/lib/own.v#L116) in the Coq code is a little bit weaker -- you only get that the new name must be in the complement of a finite set.
The stronger rule should be true though. As @robbertkrebbers points out, basically one first needs to port something like `gset_disj_alloc_updateP_strong` to `gmap`, and then the stronger result follows.https://gitlab.mpi-sws.org/iris/iris/-/issues/206Missing error message with `iDestruct ... as "#..."`2019-01-23T09:20:00ZRalf Jungjung@mpi-sws.orgMissing error message with `iDestruct ... as "#..."`Testcase:
```coq
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".
```
Prints
```
No matching clauses for match.
```
That's never an acceptable ...Testcase:
```coq
Lemma test {PROP: bi} {P Q : PROP} `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ Q ∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP".
```
Prints
```
No matching clauses for match.
```
That's never an acceptable error message, obviously.https://gitlab.mpi-sws.org/iris/iris/-/issues/205Make notation for pure and plainly affine2022-06-12T19:28:08ZRalf Jungjung@mpi-sws.orgMake notation for pure and plainly affineI think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.I think the notation for embedded Coq assertions and for plainly should include an affinely modality -- that way, one can just always use `*` and `-*` even when working in linear Iris.https://gitlab.mpi-sws.org/iris/iris/-/issues/204Support `iInduction .. using ...`2018-08-29T09:48:58ZRobbert KrebbersSupport `iInduction .. using ...`Like `induction ... using ...`; so one can more easily use custom induction principle like `map_ind`.
Requested by @dfruminLike `induction ... using ...`; so one can more easily use custom induction principle like `map_ind`.
Requested by @dfruminRobbert KrebbersRobbert Krebbershttps://gitlab.mpi-sws.org/iris/iris/-/issues/203Seal off local and frame-preserving update2019-11-01T12:50:04ZRalf Jungjung@mpi-sws.orgSeal off local and frame-preserving updateThat might solve `apply` diverging all the time.That might solve `apply` diverging all the time.https://gitlab.mpi-sws.org/iris/iris/-/issues/202Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent2020-11-06T14:42:49ZRobbert KrebbersUse of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistentSee the discussion here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/159#note_28898See the discussion here: https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/159#note_28898https://gitlab.mpi-sws.org/iris/iris/-/issues/201Improve "... not found" error messages2019-01-11T09:44:12ZRalf Jungjung@mpi-sws.orgImprove "... not found" error messagesCurrently, the message says `(INamed "HQ") not found.`. Can we improve that to `"HQ" not found.`?Currently, the message says `(INamed "HQ") not found.`. Can we improve that to `"HQ" not found.`?https://gitlab.mpi-sws.org/iris/iris/-/issues/200Framing: Make* classes lead to suboptimal results2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgFraming: Make* classes lead to suboptimal resultsFraming uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_la...Framing uses `Make*` classes to turn terms into a certain form, e.g. a leading `▷^n`. However, those classes require the original term to be *equivalent* with the converted one. This leads to situations such as
```
Lemma test_iFrame_later_rel (P : PROP) :
▷ P -∗ (▷ (P ∧ P)).
Proof. iIntros "?". iFrame.
(* Now the goal is [▷ emp] *)
```
I would expect the goal to become `emp` (and hence `iFrame` closing the goal), and indeed that would be sound (`emp` implies `▷ emp`) but it doesn't happen.https://gitlab.mpi-sws.org/iris/iris/-/issues/199iSplitL no longer checks if assumptions are spatial2018-06-10T20:13:10ZRalf Jungjung@mpi-sws.orgiSplitL no longer checks if assumptions are spatialThe following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```The following used to fail with an error saying that `"HP"` is not a spatial assumption, now it just succeeds but still puts `"HP"` on both sides:
```
Lemma iSplit_intuitionistic P :
□ P -∗ P ∗ P.
Proof. iIntros "#HP". iSplitL "HP".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/198iAlways fails without a proper error message2018-07-13T08:51:27ZRalf Jungjung@mpi-sws.orgiAlways fails without a proper error messageThe following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last ca...The following script
```
Lemma test_iAlways_emp : emp ⊢@{PROP} □ emp.
Proof.
iIntros "H". iAlways. done.
Qed.
```
Fails at `iAlways` saying
```
Error:
In nested Ltac calls to "iAlways", "iModIntro" and
"iModIntro (uconstr)", last call failed.
No matching clauses for match.
```
It should either give a proper error or empty the spatial context.https://gitlab.mpi-sws.org/iris/iris/-/issues/197iFrame sometimes needs to be called twice2018-06-14T11:41:14ZRalf Jungjung@mpi-sws.orgiFrame sometimes needs to be called twiceConsider the following proof (written in the context of `tests/proofmode_monpred.v`):
```
Program Definition monPred_id (R : monPred) : monPred :=
MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
Lemma test_iFr...Consider the following proof (written in the context of `tests/proofmode_monpred.v`):
```
Program Definition monPred_id (R : monPred) : monPred :=
MonPred (λ V, R V) _.
Next Obligation. intros ? ???. eauto. Qed.
Lemma test_iFrame_monPred_id (P Q R : monPred) i :
(P i) ∗ (Q i) ∗ (R i) -∗ (P ∗ Q ∗ monPred_id R) i.
Proof.
iIntros "(? & ? & ?)". iFrame. iFrame.
Qed.
```
Notice that I need to call `iFrame` twice. That should not be necessary.
This lead to a bunch of additional rewrites being introduced when fixing the fallout from https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/154 because the `[$]` specialization pattern stopped working (it does `iFrame` just once, it seems).https://gitlab.mpi-sws.org/iris/iris/-/issues/196Extend `iApply` to deal with pure goals2019-11-01T12:50:03ZGlen MévelExtend `iApply` to deal with pure goalsIf I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Pr...If I have a pure Coq lemma `A → B`, I would like to be able to use it in the proof-mode to prove an Iris goal `⌜B⌝` (under an Iris context). Currently `iApply` does not support this. Here is an example.
```coq
Lemma test {Σ} (A B : Prop) (P : iProp Σ) :
(A → B) → (P -∗ ⌜A⌝) → (P -∗ ⌜B⌝).
Proof.
iIntros (ab pa) "p".
(* what I would like to write directly: *)
Fail iApply ab. (* Tactic failure: iPoseProof: not a uPred. *)
(* what I need to write instead: *)
iApply (uPred.pure_mono _ _ ab).
iApply pa.
iExact "p".
Qed.
```
(tested with coq-iris dev.2018-04-10.0)https://gitlab.mpi-sws.org/iris/iris/-/issues/195Always qualify Instance with Local or Global2021-01-07T13:58:38ZRalf Jungjung@mpi-sws.orgAlways qualify Instance with Local or GlobalSince you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? Fo...Since you can't see whether you are inside a section, that's needed to even see whether this is a local or global instance.
The trouble is, we have 444 occurrences of unqualified `Instance`. Can we rely on all of them being `Global`? For the same reason that we should always use qualifiers, `sed` cannot know whether we are inside a section.
I can do the `sed`, but I'm not sure how to do the review if any of these should be `Local`. Also, let's do this after merging some MRs because this will cause plenty of conflicts.https://gitlab.mpi-sws.org/iris/iris/-/issues/194coq-speed: Measure using performance counters2018-06-22T22:02:37ZRalf Jungjung@mpi-sws.orgcoq-speed: Measure using performance counters@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?@janno suggested that instead/in addition to raw time, we could measure some performance counter statistics which should be less noisy.
@janno which counter did you suggest we measure, and how does one go about measuring that?https://gitlab.mpi-sws.org/iris/iris/-/issues/193Remove or fix `base_logic/deprecated.v`2018-07-13T08:51:26ZRobbert KrebbersRemove or fix `base_logic/deprecated.v`It currently contains:
```
(*
FIXME
...
*)
```It currently contains:
```
(*
FIXME
...
*)
```Generalized Proofmode Mergerhttps://gitlab.mpi-sws.org/iris/iris/-/issues/192Document `iRewrite -...` in `ProofMode.md`2019-01-11T10:13:31ZDan FruminDocument `iRewrite -...` in `ProofMode.md`I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```I would like to be able to say something like `iRewrite <- "Heq"` so that it would transform the goal
```
"Heq": R ≡ Q
-------------*
Q
```
into
```
-------------*
R
```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/190Framing persistent hypotheses under a later in the goal2018-07-13T08:40:31ZHai DangFraming persistent hypotheses under a later in the goalI have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.I have
```
"H": P
-------------□
▷ P ∗ Q
```
`iFrame "H"` gives me back `▷ emp ∗ Q`. I was working with an affine BI.
@jtassaro suggests to generalize `make_sep_emp_l`.https://gitlab.mpi-sws.org/iris/iris/-/issues/189Tests do not compile on MacOS2018-05-31T16:30:05ZLéon GondelmanTests do not compile on MacOSI've tried to compile iris 3bed085d035f199518707472be59d18e5bbf8342 on the branch gen_proofmode and the tests did not manage to compile.
```
COQC [test] tests/algebra.v
COQC [test] tests/heap_lang.v
COQC [test] tests/ipm_paper.v
COQC [...I've tried to compile iris 3bed085d035f199518707472be59d18e5bbf8342 on the branch gen_proofmode and the tests did not manage to compile.
```
COQC [test] tests/algebra.v
COQC [test] tests/heap_lang.v
COQC [test] tests/ipm_paper.v
COQC [test] tests/list_reverse.v
/bin/sh: tempfile: command not found
/bin/sh: tempfile: command not found
/bin/sh: tempfile: command not found
make[2]: *** [tests/heap_lang.vo] Error 127
make[2]: *** Waiting for unfinished jobs....
make[2]: *** [tests/ipm_paper.vo] Error 127
make[2]: *** [tests/algebra.vo] Error 127
/bin/sh: tempfile: command not found
make[2]: *** [tests/list_reverse.vo] Error 127
make[1]: *** [all] Error 2
make: *** [all] Error 2
```