Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2020-08-13T12:23:55Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/340Polymorphic equality for HeapLang2020-08-13T12:23:55ZDan 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/339Add "reservation map" CMRA2020-08-07T14:39:07ZRalf Jungjung@mpi-sws.orgAdd "reservation map" CMRAFor the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?For the Rust GhostCell paper, we designed and @pythonsq implemented a "reservation map" RA that is useful when one needs to synchronously reserve two equal names in two different abstractions.
1. The reservation map lets you reserve an infinite amount of names in a first frame-preserving update.
2. Next you can use that infinite set to reserve a particular name in some other abstraction, with the usual "strong allocation" lemma that picks the new name from any infinite set.
3. Finally you can take that one name you got, and since it is in the infinite set you reserved, you may now own that name in the reservation map after a second frame-preserving update.
The code for this is at https://gitlab.mpi-sws.org/FP/ghostcell/-/blob/master/theories/typing/lib/gsingleton.v. @pythonsq do you think you will have time to clean this up and make it into an MR?https://gitlab.mpi-sws.org/iris/iris/-/issues/338Missing unseal tactic for siProp2020-08-13T06:41:48ZPaolo G. GiarrussoMissing unseal tactic for siProp
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl.
(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
```
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.
Here's what I've used:
```coq
(* XXX Taken from uPred.unseal / monPred.unseal, since this logic is missing for siLogic. *)
Ltac unseal_prepare := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp,
monPred_upclosed, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl.
(* Should be siProp.unseal. *)
Ltac siProp_unseal := unseal_prepare; siProp_primitive.unseal.
```
The second part is easy, but the first not (tho it was worse before the bi-sbi merge), and deserves to be abstracted.https://gitlab.mpi-sws.org/iris/iris/-/issues/335iris.sty incompatible with acmart2020-07-15T12:25:40ZRalf Jungjung@mpi-sws.orgiris.sty incompatible with acmartThe `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.The `\nequiv` macro in `iris.sty` clashes with something that is import by the `acm` template. In our own papers, we work around this by undefining `\nequiv` locally, but that's not great.
We should either always overwrite whatever the existing `\nequiv` is, or else change the name of our macro.https://gitlab.mpi-sws.org/iris/iris/-/issues/334Expand test coverage of proofmode2020-07-14T07:13:05ZTej Chajedtchajed@mit.eduExpand test coverage of proofmodeThe proof mode tests don't cover the following:
- [ ] `iRename`
- [ ] `iTypeOf`
- [ ] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.The proof mode tests don't cover the following:
- [ ] `iRename`
- [ ] `iTypeOf`
- [ ] `iInduction`'s ability to freshen the inductive hypothesis
I have tests for the first two on my [bytes-ident](https://gitlab.mpi-sws.org/tchajed/iris-coq/-/tree/bytes-ident) branch.https://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-06-25T21:39:26ZRalf 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/328Add RA for auth of a heap2020-08-07T18:02:31ZRalf Jungjung@mpi-sws.orgAdd RA for auth of a heap`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in Iris. ;)
The only open question for me is, what is `Y`? (`X` is any countable type.)
* We probably should have fractions, so that would be `Y := frac * agree T`. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives `False`).
* @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with `Y := agree T`, or we could do the strictly more powerful thing (subsuming both of the above) and do `Y := (frac * agree T) + agree T`. I *think* with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.`auth (gmap X Y)` is a very frequently reoccurring RA, and finding all the right lemmas to compose for it can be challenging. After I saw people use `gen_heap` when really they want this RA, I am now convinced that we should have it in Iris. ;)
The only open question for me is, what is `Y`? (`X` is any countable type.)
* We probably should have fractions, so that would be `Y := frac * agree T`. Even if you don't need fractions, just making it always "1" should not be hard to use (we should just make sure to have a lemma that from owning the "1" fraction twice, derives `False`).
* @tchajed mentioned they also need something with agreement in a few places. So we could either also have a version with `Y := agree T`, or we could do the strictly more powerful thing (subsuming both of the above) and do `Y := (frac * agree T) + agree T`. I *think* with the right surface-level definitions, this is actually not harder to use than either of the two more specialized heaps.https://gitlab.mpi-sws.org/iris/iris/-/issues/327Add RA for auth max_nat2020-08-05T18:22:40ZRobbertAdd RA for auth max_natAs @tchajed pointed out, this RA is quite commonly used. While porting developments as a consequence of !461 I noticed it's also used in ReLoC.
So, concretely, there are the following uses:
- Iris: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/heap_lang/lib/counter.v#L16
- ReLoC: https://gitlab.mpi-sws.org/iris/reloc/-/blob/7dca8f9472290626ac5174d5789512234ce115e9/theories/examples/symbol.v#L49
- Perennial: https://github.com/mit-pdos/perennial/blob/master/src/algebra/fmcounter.v
Would be good to add it to `algebra/lib` so people don't reprove the same stuff all the time.As @tchajed pointed out, this RA is quite commonly used. While porting developments as a consequence of !461 I noticed it's also used in ReLoC.
So, concretely, there are the following uses:
- Iris: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/heap_lang/lib/counter.v#L16
- ReLoC: https://gitlab.mpi-sws.org/iris/reloc/-/blob/7dca8f9472290626ac5174d5789512234ce115e9/theories/examples/symbol.v#L49
- Perennial: https://github.com/mit-pdos/perennial/blob/master/src/algebra/fmcounter.v
Would be good to add it to `algebra/lib` so people don't reprove the same stuff all the time.https://gitlab.mpi-sws.org/iris/iris/-/issues/321Make `contractive_proper` into a lemma, or control other instances that make ...2020-07-14T08:20:29ZPaolo 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/318Drop support for Coq 8.9?2020-08-12T13:56:28ZRalf Jungjung@mpi-sws.orgDrop support for Coq 8.9?Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`)
* `change_no_check` (to stop using deprecated `convert_concl_no_check`)
* `Declare Scope` (to fix deprecated use of undeclared scopes)
Is there more?Should we drop support for Coq 8.9? Let us collect what we would get by requiring Coq 8.10.
* https://gitlab.mpi-sws.org/iris/iris/-/issues/317 requires 8.10 I think.
* [non-canonical projections](`https://github.com/coq/coq/pull/10076`)
* `change_no_check` (to stop using deprecated `convert_concl_no_check`)
* `Declare Scope` (to fix deprecated use of undeclared scopes)
Is there more?https://gitlab.mpi-sws.org/iris/iris/-/issues/317Use `byte` based strings for proof mode2020-05-16T19:16:11ZRobbertUse `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-08-07T17:57:53ZRalf 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 Iris2020-04-22T22:59:30ZPaolo 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/311Document side-effects of importing Iris2020-07-04T13:34:25ZRalf Jungjung@mpi-sws.orgDocument side-effects of importing IrisIris should have something [like std++ has](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects) where we document its global, Coq-level side-effects.Iris should have something [like std++ has](https://gitlab.mpi-sws.org/iris/stdpp/#side-effects) where we document its global, Coq-level side-effects.https://gitlab.mpi-sws.org/iris/iris/-/issues/310Choose syntax and implement destructuring existentials with pure components, ...2020-07-22T02:53:46ZPaolo G. GiarrussoChoose syntax and implement destructuring existentials with pure components, following !400It'd be nice to support something like `iDestruct "H" as "∃[%x HP]"` on `"H": ∃ x, P` (where the `∃[ipat ipat]` syntax is a strawman), mapping that introduction pattern to `iExistsDestruct`. The killer feature is support for nested existentials, which require multiple iDestruct calls today.
In discussion on [!400](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/400#note_45911), I and @tchajed considered supporting that with pattern `[%x HP]`, but that pattern is already mapped to `iAndDestruct`, and unlike in Coq the two methods are very different.
Steps:
1. [ ] bikeshed a syntax
2. [ ] any other discussion on the specification, if needed
3. [ ] implement this.It'd be nice to support something like `iDestruct "H" as "∃[%x HP]"` on `"H": ∃ x, P` (where the `∃[ipat ipat]` syntax is a strawman), mapping that introduction pattern to `iExistsDestruct`. The killer feature is support for nested existentials, which require multiple iDestruct calls today.
In discussion on [!400](https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/400#note_45911), I and @tchajed considered supporting that with pattern `[%x HP]`, but that pattern is already mapped to `iAndDestruct`, and unlike in Coq the two methods are very different.
Steps:
1. [ ] bikeshed a syntax
2. [ ] any other discussion on the specification, if needed
3. [ ] implement this.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 `λ`.