Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-07-21T18:01:10Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/332Become part of Coq Platform?2020-07-21T18:01:10ZRalf Jungjung@mpi-sws.orgBecome part of Coq Platform?We should consider making iris part of the [Coq Platform](https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md).
Quoting Michael Soegtrop:
> So if IRIS becomes part of the platform, the platform takes care that there is a reliable, fast and fool proof way to install Coq including IRIS on Windows, OSX and - maybe a bit less fool proof - Linux. This should make it easier for teachers and interested explorers to install IRIS. On the other hand you agree to do your best to deliver a working release of IRIS for any major Coq release (like 8.12, 8.13) within at most 3 months, better 1 month.We should consider making iris part of the [Coq Platform](https://github.com/MSoegtropIMC/coq-platform/blob/master/charter.md).
Quoting Michael Soegtrop:
> So if IRIS becomes part of the platform, the platform takes care that there is a reliable, fast and fool proof way to install Coq including IRIS on Windows, OSX and - maybe a bit less fool proof - Linux. This should make it easier for teachers and interested explorers to install IRIS. On the other hand you agree to do your best to deliver a working release of IRIS for any major Coq release (like 8.12, 8.13) within at most 3 months, better 1 month.https://gitlab.mpi-sws.org/iris/iris/-/issues/331simpl breaks error checking of `iNext (S i)`2020-07-14T08:21:09ZPaolo G. Giarrussosimpl breaks error checking of `iNext (S i)`I'd expect `iNext (S i)` to introduce exactly `S i` later, and fail otherwise. However, after e.g. `simpl` turns `▷^(S i) P` into `▷ ▷^i P`, that will sometimes introduce _one_ later, as shown below.
```coq
From iris.proofmode Require Import tactics.
Lemma foo i {PROP} P : P ⊢@{PROP} ▷^(S i) P.
Proof.
iIntros "H".
Fail iNext 2.
iNext (S i).
Fail iNext i.
Fail iNext.
iExact "H".
Restart.
iIntros "H /=".
Fail iNext 2.
iNext (S i).
iNext i. (* !!! *)
Abort.
```
### Iris version
```
$ opam show coq-iris -f version
dev.2020-05-24.2.af5e50e7
```
with Coq 8.11.1.I'd expect `iNext (S i)` to introduce exactly `S i` later, and fail otherwise. However, after e.g. `simpl` turns `▷^(S i) P` into `▷ ▷^i P`, that will sometimes introduce _one_ later, as shown below.
```coq
From iris.proofmode Require Import tactics.
Lemma foo i {PROP} P : P ⊢@{PROP} ▷^(S i) P.
Proof.
iIntros "H".
Fail iNext 2.
iNext (S i).
Fail iNext i.
Fail iNext.
iExact "H".
Restart.
iIntros "H /=".
Fail iNext 2.
iNext (S i).
iNext i. (* !!! *)
Abort.
```
### Iris version
```
$ opam show coq-iris -f version
dev.2020-05-24.2.af5e50e7
```
with Coq 8.11.1.https://gitlab.mpi-sws.org/iris/iris/-/issues/330Consider adding `iEnough` variants of `iAssert` ?2020-06-26T07:35:15ZPaolo G. GiarrussoConsider adding `iEnough` variants of `iAssert` ?Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first last.
```
The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?Something like:
```coq
Tactic Notation "iEnough" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssert Q with Hs as pat; first last.
Tactic Notation "iEnough" open_constr(Q) "as" constr(pat) :=
iAssert Q as pat; first last.
```
The point is just readability, and adding all the overloads is probably not worth it, but maybe this would change with an Ltac2 proofmode?https://gitlab.mpi-sws.org/iris/iris/-/issues/329Iris Website Reform2020-09-29T15:48:56ZRalf Jungjung@mpi-sws.orgIris Website ReformWe had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* We'd like to split the website into sub-pages, as the list of papers is getting too long.
* We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
* In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
* We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).
I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.We had a long discussion on Mattermost today discussing potential improvements to the website. Some of the take-aways include:
* We'd like to move to a static site generator (Jekyll, or something else if someone makes a good pitch).
* We'd like to split the website into sub-pages, as the list of papers is getting too long.
* We'd like to have the website repo public for contributors. I think it would make sense to have it in the Iris organization here on MPI's GitLab.
* In terms of content, the concern that triggered this discussion was along the lines of "(some) people think Iris is just for academic/toy/ML-like languages". We should probably put the fact that Iris is very flexible front and center, maybe by picking a few papers to display on the front page that use Iris for various models of real-world definitely-not-toy languages (RustBelt for Rust, runST for Haskell, DOT for Scala, "Non-Determinism in C Expressions" for C, Goose for Go, and once that paper exists RefinedC for C).
* We could also highlight the different kinds of properties people verify in Iris (type system soundness, refinement, verification of concurrent algorithms, non-interference, ...).
I expect I will take the lead on setting up the infrastructure for wiring up GitLab with Jekyll and GH pages, and @robbertkrebbers offered to take the lead on the content side of things.https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-10-20T09:21:24ZPaolo G. GiarrussoMake `contractive_proper` into a lemma, or control other instances that make it costly.Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?Successful typeclass searches for `contractive_proper` take 0.1s — as shown by replacing `contractive_proper _` with `_`. So it should maybe be disabled like `ne_proper` (see 6df6c641aadd50cd9808035f77e41048a99e6600).
Logs like https://gist.github.com/Blaisorblade/541416169b97729e60bb80fb0f259b7d reveal that the problem is that `proper_reflexive` is tried first, and then search diverges. Finding a way to blacklist certain instances for `Reflexive (equiv ==> equiv)%signature` would be useful — maybe removing them and replacing them with `Hint Extern`?https://gitlab.mpi-sws.org/iris/iris/-/issues/320λne should use %I for body — or add a variant using `%I`.2020-07-14T08:20:05ZPaolo G. Giarrussoλne should use %I for body — or add a variant using `%I`.For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).For unbundled functions, I've used for a while a lambda notation that places the body automatically in `bi_scope`:
```coq
(** * Notation for functions in the Iris scope. *)
Notation "'λI' x .. y , t" := (fun x => .. (fun y => t%I) ..)
(at level 200, x binder, y binder, right associativity,
only parsing) : function_scope.
```
Similarly, needing both `λne` and `%I` is annoying, what about:
```coq
Notation "'λneI' x .. y , t" :=
(@OfeMor _ _ (λ x, .. (@OfeMor _ _ (λ y, t)%I _) ..) _)
(at level 200, x binder, y binder, right associativity).
```
I'd even consider placing that annotation in `λne` itself – `algebra.ofe` could import `bi.notation`; but many non-expansive functions aren't predicates :-).Paolo G. GiarrussoPaolo G. Giarrussohttps://gitlab.mpi-sws.org/iris/iris/-/issues/317Use `byte` based strings for proof mode2020-05-16T19:16:11ZRobbert KrebbersUse `byte` based strings for proof modeNewer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction of `byte` based strings does not exist in the Coq stdlib but can be defined as:
```
From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.
Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.
Definition foo : bytes := "foo".
```Newer versions of Coq have a type `byte` with 256 constructors. We could use strings based on `byte` in the proofmode. Maybe that gives a significant speed up compared to the current `ascii` based strings.
@tchajed said the construction of `byte` based strings does not exist in the Coq stdlib but can be defined as:
```
From Coq Require Import Init.Byte.
Record bytes := bytes_from_list { bytes_to_list : list byte }.
Declare Scope bytestring_scope.
Open Scope bytestring_scope.
String Notation bytes bytes_from_list bytes_to_list : bytestring_scope.
Definition foo : bytes := "foo".
```https://gitlab.mpi-sws.org/iris/iris/-/issues/316Explore use of `#[local]`/`Local` definitions2020-10-02T11:44:42ZRalf Jungjung@mpi-sws.orgExplore use of `#[local]`/`Local` definitionsI recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, [consider these](https://gitlab.mpi-sws.org/iris/iris/-/blob/701b533c8be530a69e605ee5443a089146d5701f/theories/base_logic/lib/gen_heap.v#L136-164).
`Local Definition` is supported in Coq 8.9 (and maybe older) so we can start using it any time.I recently learned that in Coq, we can [mark a definition as not being imported with `Import`/`Export`](https://github.com/coq/coq/pull/12162#issuecomment-625186261). I think we should explore the option of using this to mark definitions that are internal to a module and should not be used by clients -- those then don't need the C-style namespacing of prefixing everything.
As a random example for such definitions, [consider these](https://gitlab.mpi-sws.org/iris/iris/-/blob/701b533c8be530a69e605ee5443a089146d5701f/theories/base_logic/lib/gen_heap.v#L136-164).
`Local Definition` is supported in Coq 8.9 (and maybe older) so we can start using it any time.https://gitlab.mpi-sws.org/iris/iris/-/issues/312Fix setoid rewriting for function application in Iris2021-07-25T11:37:33ZPaolo G. GiarrussoFix setoid rewriting for function application in IrisSome of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.Some of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called [Yannick Zakowski](https://coq.discourse.group/t/confused-with-a-failure-of-a-generalized-rewrite/783?u=blaisorblade) discovered a fix by reading rewrite's error message, and I adapted this to Iris:
```coq
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
```
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.https://gitlab.mpi-sws.org/iris/iris/-/issues/308Automatically enforce use of Unicode → instead of ASCII ->2020-04-16T19:10:02ZTej Chajedtchajed@mit.eduAutomatically enforce use of Unicode → instead of ASCII ->Iris can check (at least approximately) for new uses of -> in a pre-commit hook to enforce this style. This should save @robbertkrebbers several hours of writing "Please use Unicode →" in MRs.
Here's my attempt at this. To install, you need to copy this file to `.git/hooks/pre-commit` and make it executable.
This was tested on macOS with BSD grep, but it should be cross-platform.
```sh
#!/bin/bash
set -e
# redirect stdout to stderr
exec 1>&2
error() {
echo -e "\033[31m$1\033[0m"
}
## Check for adding ASCII -> instead of Unicode →
# first filter to Coq files not containing "ascii"
if find . -name '*.v' -and -not -name '*ascii*' -print0 |\
xargs -0 git diff --staged --unified=0 -- |\
# only check additions, not deletions
grep '^\+.*->' |\
# skip lines that legitimately use -> in Ltac
grep -v '\b(rewrite|destruct|iDestruct|iMod)\b.*->'
then
error "Please use Unicode [→] instead of [->]."
exit 1
fi
```
Note that this doesn't need to be perfect. You can always override the check with `git commit --no-verify`.
I can also add checks for `\bexists\b`, `\bforall\b`, and `\bfun\b` that should be replaced with their Unicode variants `∃`, `∀`, and `λ`.Iris can check (at least approximately) for new uses of -> in a pre-commit hook to enforce this style. This should save @robbertkrebbers several hours of writing "Please use Unicode →" in MRs.
Here's my attempt at this. To install, you need to copy this file to `.git/hooks/pre-commit` and make it executable.
This was tested on macOS with BSD grep, but it should be cross-platform.
```sh
#!/bin/bash
set -e
# redirect stdout to stderr
exec 1>&2
error() {
echo -e "\033[31m$1\033[0m"
}
## Check for adding ASCII -> instead of Unicode →
# first filter to Coq files not containing "ascii"
if find . -name '*.v' -and -not -name '*ascii*' -print0 |\
xargs -0 git diff --staged --unified=0 -- |\
# only check additions, not deletions
grep '^\+.*->' |\
# skip lines that legitimately use -> in Ltac
grep -v '\b(rewrite|destruct|iDestruct|iMod)\b.*->'
then
error "Please use Unicode [→] instead of [->]."
exit 1
fi
```
Note that this doesn't need to be perfect. You can always override the check with `git commit --no-verify`.
I can also add checks for `\bexists\b`, `\bforall\b`, and `\bfun\b` that should be replaced with their Unicode variants `∃`, `∀`, and `λ`.https://gitlab.mpi-sws.org/iris/iris/-/issues/304Direction of _op lemmas is inconsistent with _(p)core, _valid, _included2020-04-06T18:50:12ZRalf Jungjung@mpi-sws.orgDirection of _op lemmas is inconsistent with _(p)core, _valid, _includedSee the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
```
However, most of our `_op` lemmas push the named operation "out":
```coq
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
```
Moreover, even with one "group" of lemmas, not all are consistent: `singleton_op`, `discrete_fun_singleton_op`, `list_singleton_op` push "in", while `cmra_morphism_(p)core` push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the `_op` lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/303, so this starts to look like we are just going back and forth...See the discussion at https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/403#note_47448: our `_(p)core`, `_valid`, `_included` lemmas generally push the named operation "in", e.g.
```coq
Lemma pair_valid (a : A) (b : B) : ✓ (a, b) ↔ ✓ a ∧ ✓ b.
Lemma pair_core `{!CmraTotal A, !CmraTotal B} (a : A) (b : B) :
core (a, b) = (core a, core b).
```
However, most of our `_op` lemmas push the named operation "out":
```coq
Lemma pair_op (a a' : A) (b b' : B) : (a ⋅ a', b ⋅ b') = (a, b) ⋅ (a', b').
```
Moreover, even with one "group" of lemmas, not all are consistent: `singleton_op`, `discrete_fun_singleton_op`, `list_singleton_op` push "in", while `cmra_morphism_(p)core` push "out" (and there might be more).
At the very least, we should make all lemmas within a "group" consistent. So, the minimal fix for this is to swap the 5 lemmas named in the last paragraph. However, we might also want to fix the larger inconsistency that the `_op` lemmas are going the other way, compared to the rest of them. The thing is, we already swapped half of them https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/303, so this starts to look like we are just going back and forth...https://gitlab.mpi-sws.org/iris/iris/-/issues/303Canonical structures have major performance impact2020-05-11T18:22:36ZRobbert KrebbersCanonical structures have major performance impactAs I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.As I mentioned on [Mattermost](https://mattermost.mpi-sws.org/iris/pl/49pr68ips3yuifgbd9qow6u81o), I had a [fun experiment](https://gitlab.mpi-sws.org/iris/iris/-/commit/294ef2ef2df5478db81065f6cd5edc1d831419a1) collapsing the `sbi` and `bi` canonical structures.
- [37.40% overall on lambdarust-weak](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=masters%2Fweak_mem&var-commit1=bcc7c0be5ba2def0989d727c97d94a8492b9e40b&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi_weak&var-commit2=4ea92744abcd644f385696c398206a20a2cab7cf&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 72.22%.
- [23.28% overall on Iron](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iron&var-branch1=master&var-commit1=4dcc142742d846037be4cd94678ff8759465e6c1&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=37f90dd22db3ca477377d16ae72d761cb617412c&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 38.13%.
- [3.8% overall on Iris](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=9b2ad256fbf948933cdbf6c313eb244fd2439bf3&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=294ef2ef2df5478db81065f6cd5edc1d831419a1&var-config2=build-coq.8.11.0&var-group=().*&var-metric=instructions), with improvements for individual files up to 13.16%.
- [5.2% overall on lamdarust master](https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=lambda-rust&var-branch1=master&var-commit1=fe35f4cd910f3f3235fd3c6b6c46fc142d3ce13f&var-config1=build-coq.8.11.0&var-branch2=ci%2Frobbert%2Fmerge_sbi&var-commit2=bea9f4a02efe48a38894fe1286add7ab25a2d2de&var-config2=build-iris.dev&var-group=().*&var-metric=instructions), with improvements for individual files up to 10.18%.
These differences are major, especially for the projects that use BI formers (monPred in lambdarust-weak and fracPred in Iron)! So it looks like there is really something we should investigate.https://gitlab.mpi-sws.org/iris/iris/-/issues/300vs doesn't use FUpd2020-03-30T09:38:01ZGregory Malechavs doesn't use FUpdIs there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `monPred x (iProp _)` even though all of the other notation (that are conceptually very simple) do work at `monPred`.Is there a reason that the definition of `vs` explicitly mentions `iProp`? In practice it means that its notation can not be used in lifted logics such as `monPred`. For example, writing `P ==> Q` works at `iProp`, but doesn't work at `monPred x (iProp _)` even though all of the other notation (that are conceptually very simple) do work at `monPred`.https://gitlab.mpi-sws.org/iris/iris/-/issues/298Guide typeclass search via more specialized typeclasses2020-06-17T16:51:55ZMichael SammlerGuide typeclass search via more specialized typeclassesFind places where a general typeclass (like `SetUnfold` before) can be split into more specialized typeclasses (like `SetUnfoldElemOf`) such that typeclass search is always guided by the head symbol. https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/66 applied this optimization to `SetUnfold`.
cc @robbertkrebbersFind places where a general typeclass (like `SetUnfold` before) can be split into more specialized typeclasses (like `SetUnfoldElemOf`) such that typeclass search is always guided by the head symbol. https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/66 applied this optimization to `SetUnfold`.
cc @robbertkrebbershttps://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/295Have iApply introduce equalities for subterms that cannot be unified directly2020-08-08T21:57:49ZArmaël GuéneauHave iApply introduce equalities for subterms that cannot be unified directlyThe initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 = z⌝
```
without relying explicitly on the names `x4` and `z`.
I'm not sure what would be the most general form of such a tactic, or what its user interface would be, though. I think it would be nice to have it as an instance of `iApply`, if that's possible. (having it in `iFrame` as well is perhaps possible but risky, for instance in the case of mapsto it should at least be restricted to mapsto with the same syntactic location...).The initial motivation is to be able to go from a proof-mode goal of the form:
```
"H" : r ↦ (x, x0, x1, x2, x4)
--------------------------------------∗
r ↦ (x, x0, x1, x2, z)
```
to
```
--------------------------------------∗
⌜x4 = z⌝
```
without relying explicitly on the names `x4` and `z`.
I'm not sure what would be the most general form of such a tactic, or what its user interface would be, though. I think it would be nice to have it as an instance of `iApply`, if that's possible. (having it in `iFrame` as well is perhaps possible but risky, for instance in the case of mapsto it should at least be restricted to mapsto with the same syntactic location...).https://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 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).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/289Documentation for installation on Windows2020-02-06T16:07:24ZRalf Jungjung@mpi-sws.orgDocumentation for installation on WindowsWe have very few Windows users, but every now and then the question comes up and we are rather clueless about what is the best way to use Iris on Windows. It would be good to document some best practices. (This is a sister issue to https://gitlab.mpi-sws.org/iris/iris/issues/280.)
Cc @codyroux @quarkbeast @blaisorbladeWe have very few Windows users, but every now and then the question comes up and we are rather clueless about what is the best way to use Iris on Windows. It would be good to document some best practices. (This is a sister issue to https://gitlab.mpi-sws.org/iris/iris/issues/280.)
Cc @codyroux @quarkbeast @blaisorbladehttps://gitlab.mpi-sws.org/iris/iris/-/issues/287iApply strips some modalities, but not monotonically2020-02-01T13:06:32ZPaolo G. GiarrussoiApply strips some modalities, but not monotonicallyHere's a minimized inconsistent behavior and a possible fix via an instance. I suspect *that* instance is missing by design, but I can't tell what the design is, even tho I can read `Hint Mode` — see #139.
(I also realize that such instances must appear for either all or none of the monotonic modalities).
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
(* Here [iApply] works. *)
Lemma foo0 P : □ P -∗ P.
Proof. iIntros "H". iApply "H". Qed.
(* But here it fails! *)
Lemma foo1 P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". Fail iApply "H". iNext. iApply "H". Qed.
(* Here's a possible fix, but I'm unsure whether it respects the interplay of
FromAssumption, KnownLFromAssumption and KnownRFromAssumption,
as it is not fully documented.
Should I add this for both KnownLFromAssumption and KnownRFromAssumption? *)
Global Instance from_assumption_later_later p P Q :
FromAssumption p P Q → FromAssumption p (▷ P) (▷ Q)%I.
Proof.
rewrite /KnownRFromAssumption /FromAssumption
later_intuitionistically_if_2 => ->. exact: later_mono.
Qed.
Lemma foo P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". iApply "H". Qed.
End sbi_instances.
```Here's a minimized inconsistent behavior and a possible fix via an instance. I suspect *that* instance is missing by design, but I can't tell what the design is, even tho I can read `Hint Mode` — see #139.
(I also realize that such instances must appear for either all or none of the monotonic modalities).
```coq
From iris.proofmode Require Import tactics.
From iris.bi Require Import bi.
Import bi.
Section sbi_instances.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
(* Here [iApply] works. *)
Lemma foo0 P : □ P -∗ P.
Proof. iIntros "H". iApply "H". Qed.
(* But here it fails! *)
Lemma foo1 P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". Fail iApply "H". iNext. iApply "H". Qed.
(* Here's a possible fix, but I'm unsure whether it respects the interplay of
FromAssumption, KnownLFromAssumption and KnownRFromAssumption,
as it is not fully documented.
Should I add this for both KnownLFromAssumption and KnownRFromAssumption? *)
Global Instance from_assumption_later_later p P Q :
FromAssumption p P Q → FromAssumption p (▷ P) (▷ Q)%I.
Proof.
rewrite /KnownRFromAssumption /FromAssumption
later_intuitionistically_if_2 => ->. exact: later_mono.
Qed.
Lemma foo P : ▷ □ P -∗ ▷ P.
Proof. iIntros "H". iApply "H". Qed.
End sbi_instances.
```https://gitlab.mpi-sws.org/iris/iris/-/issues/286Address the STS encodings lack of usefulness2020-01-30T21:32:04ZJonas KastbergAddress the STS encodings lack of usefulnessThe current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.The current encoding of [STS's](https://gitlab.mpi-sws.org/iris/iris/blob/master/theories/base_logic/lib/sts.v) has a bad reputation. On several occurances it has happened that newcomers use them and are then told not to, as they are "very painful to use in Coq, and we never actually use them in practice".
Whether this is inherent to the abstraction or if its the current iteration of the encoding is to be figured out.
Going forward we should do either of the following:
- Include a disclaimer discouraging people from using them
- Remove the encoding from the repository
- Update the implementation to be more user-friendly
I suggest doing either of the first two short-term and then possibly look into the third long-term.
It might make most sense to do the disclaimer to maintain correspondence with the formal documentation.