Iris issueshttps://gitlab.mpi-sws.org/iris/iris/-/issues2021-03-24T11:03:52Zhttps://gitlab.mpi-sws.org/iris/iris/-/issues/404Make string-ident a standard part of Iris2021-03-24T11:03:52ZLennard GäherMake string-ident a standard part of IrisSince support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this would have the benefits of
* not having to explicitly require the user to install the plugin in developments using Iris,
* and thus be beneficial to overall code quality of developments using Iris (since there would be a clear argument for using the new intro pattern instead of using auto-generated names).
@jung suggested I create an issue for this.Since support for Coq 8.10 has been dropped for a while now and 8.11 is required, the `string-ident` plugin could be integrated into Iris master so that the named `%H` intro pattern becomes available in the IPM by default.
Mainly, this would have the benefits of
* not having to explicitly require the user to install the plugin in developments using Iris,
* and thus be beneficial to overall code quality of developments using Iris (since there would be a clear argument for using the new intro pattern instead of using auto-generated names).
@jung suggested I create an issue for this.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/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/327Add RA for auth max_nat2020-10-27T19:49:24ZRobbert KrebbersAdd 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/235Documentation for the algebra folder2019-11-01T11:10:11ZRobbert KrebbersDocumentation for the algebra folderIt would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical structures are used.It would be good if we have a file `Algebra.md` that:
- Describes which algebraic structures can be found where
- What instances of these structures are available
- Describes things like `-n>` v.s. `-c>`
- How type classes and canonical structures are used.https://gitlab.mpi-sws.org/iris/iris/-/issues/410Modality for `Timeless`2021-04-19T07:51:21ZRalf Jungjung@mpi-sws.orgModality for `Timeless`We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.We have long been looking for a modality corresponding to `Timeless`. @simonspies recently made a proposal, which I am trying to recall (please correct me of this is wrong^^):
```
<timeless> P := ▷ False → P
Timeless P := <timeless> P ⊢ P
```
Unlike prior attempts, this is a *monadic* modality, i.e. it is easy to introduce but hard to eliminate. That makes it less useful -- I was hoping that `<timeless> P` would be *stronger* than `P` and basically say that the proof only requires timeless resources (restriction of the context, and thus comonadic); instead, here `<timeless> P` is *weaker* than `P`, it basically says "I have a proof of `P` at step-index 0".
The existing `later_false_em` can now be written as `▷ P ⊢ ▷ False ∨ <timeless> P` (or `▷ P ⊢ ◇ <timeless> P`).
But this could still be interesting and useful in other situations we have not considered yet, so it is worth exploring. One open question is which primitive laws we need to derive all the properties of `Timeless` that we currently have. For the record, this is the current definition of `Timeless`:
```
Timeless' P := ▷ P ⊢ ▷ False ∨ P
(* or *)
Timeless' P := ▷ P ⊢ ◇ P
```
By `later_false_em`, we have `Timeless P → Timeless' P` (so the new class is at least as strong). I am not sure about the other direction.https://gitlab.mpi-sws.org/iris/iris/-/issues/403Iris 3.42021-03-06T12:22:13ZRalf Jungjung@mpi-sws.orgIris 3.4There was a Coq 8.13 release, so following our promise for the Coq Platform, we should make a compatible release ASAP (the Coq release was already more than a month ago).
[Milestone with potential release blockers](https://gitlab.mpi-sws.org/iris/iris/-/milestones/6)There was a Coq 8.13 release, so following our promise for the Coq Platform, we should make a compatible release ASAP (the Coq release was already more than a month ago).
[Milestone with potential release blockers](https://gitlab.mpi-sws.org/iris/iris/-/milestones/6)https://gitlab.mpi-sws.org/iris/iris/-/issues/402iFrame performance issues2021-02-17T08:50:16ZRalf Jungjung@mpi-sws.orgiFrame performance issuesThere are some situations where iFrame is rather slow.
For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.There are some situations where iFrame is rather slow.
For example [here](https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/43#note_60969) it seems to backtrack a lot on the disjunctions. Maybe it should just not descend into disjunctions at all by default?
Also, @tchajed noticed that `iFrame` is doing a lot of `AsFractional` everywhere, which might also be a too expensive default -- this is tracked separately in https://gitlab.mpi-sws.org/iris/iris/-/issues/351.
Cc https://gitlab.mpi-sws.org/iris/iris/-/issues/183 for the general "power vs performance" tradeoff in `iFrame`.https://gitlab.mpi-sws.org/iris/iris/-/issues/392Masks in step-taking fupd notation2020-12-10T13:37:03ZRalf Jungjung@mpi-sws.orgMasks in step-taking fupd notationEarlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?Earlier this year, I have changed the step-taking fupd notation (https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/462). I think this made things better, but I think there's still room for improvement -- in particular with https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/595 finally making the more-than-1-step case actually useful in Iris proper.
The current notation is
```coq
(** * Step-taking fancy updates. *)
(** These have two masks, but they are different than the two masks of a
mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
mask") holds at the beginning and the end; the second mask [Ei] ("inner
mask") holds around each ▷. This is also why we use a different notation
than for the two masks of a mask-changing updates. *)
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=> ▷ |={Ei,Eo}=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E}[E]▷=> Q)%I : bi_scope.
(** For the iterated version, in principle there are 4 masks: "outer" and
"inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
that could potentially differ from [Eo]. The latter can be obtained from
this notation by adding normal mask-changing update modalities: [
|={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]▷=> P) Q)%I : bi_scope.
Notation "|={ E }▷=>^ n Q" := (|={E}[E]▷=>^n Q)%I : bi_scope.
```
Now it turns out that an n-step update that opens and closes things at each step is basically never useful (or at least that is what things look like so far). So the iterated step-taking update should really open some masks once, then do a bunch of steps with updates, and then close some masks again: [rj1]
```coq
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
For `n=1` this is equivalent, but for larger `n` it is not (unless `Ei=Eo`). Since this is not just strictly iterating the single-step update any more, maybe the notation should be slightly different to reflect this, such as [rj1']
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={Ei}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
And then, to make things even stranger, @jjourdan started using this kind of update in !595:
```coq
|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P
```
I thought quite a bit about this update the last few days... the empty set makes it look like no invariants can be used "while counting down the steps", but that is not so: when considering masks as resources/tokens (which under the hood they are), this update lets us grab the tokens for `E1\E2` in the beginning, use them throughout the update in any way we please, and give them back in the end. We don't have good proof rules for this general case though. We do have rules for the easier case where `E2=∅`: then one can use `mask_fupd_intro'` to introduce the `|={E1,∅}=>` modality while obtaining `|={∅,E1}=> emp` that can be kept around, and can be used when the goal starts with `|={∅}=>`. In other words:
```coq
|={E1,∅}=> |={∅}▷=>^n |={∅,E1}=> P
----------------------------------
|={E1}=> |={E1}▷=>^n |={E1}=> P
```
So from this it looks like maybe we want to define the iterated step-taking update as [jh]
```coq
Notation "|={ Eo } [ Ei ]▷^ n => Q" := (|={Eo,Ei}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={Ei,Eo}=> Q)))%I : bi_scope.
```
But we need to come up with better proof rules to actually make this conveniently usable, so maybe it's not worth it having such a flexible notation, and we should just have [rj2] (basically the special case of [rj1] where the inner mask is empty, which coincides with [jh] where the inner mask is empty)
```coq
Notation "|={ Eo }▷^ n => Q" := (|={Eo,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,Eo}=> Q)))%I : bi_scope.
```
or maybe we take inspiration from some recent work by @simonspies and go for [simon]
```coq
Notation "|={ E1 , E2 }▷^ n => Q" := (|={E1,∅}=> (Nat.iter n (λ P, |={∅}▷=> P) (|={∅,E2}=> Q)))%I : bi_scope.
```
There's just too many variants that could make sense.^^ (We could also have variants of some earlier notations where the pre- and post-masks are different, but having a notation with three masks seems a bit unwieldy...)
My current thinking is that it's not worth to expose the full power of @jjourdan's theorem (we have no known user that requires it, I think, but we should check in RustBelt), so we can go with one of the last two and exploit that `|={E1,E2}=> |={∅}▷=>^n |={E2,E1}=> P` is implied by the easier-to-use `|={E1\E2,∅}=> |={∅}▷=>^n |={∅,E1\E2}=> P` (I am just a bit worried about how well `solve_nidjs` will be able to handle these masks).
The one thing that is clear is that the current multi-mask multi-step notation is not useful enough to justify its existence -- since there is no way to use it to state the new lemma in !595. That is the one design constraint I have identified so far: have a notation such that we can use it to state a many-step-fupd-lemma that is actually useful (and by this I mean use *just* this notation, not composing it with some pre- and post-updates like @jjourdan did). All of the above fit this condition to some extend, but [rj1] results in a very weak statement that we probably do not want. [jh] will be hard to write good rules for I think (but maybe I am wrong about this), which pushes me towards [rj2]; generalizing that to [simon] means we can even use this notation to define WP (even the WP in !595, where `={∅}▷=∗^(S $ steps_per_step stepcnt) |={∅,E}=>` could become `={∅,E}▷^(S $ steps_per_step stepcnt)=∗`).
That was lots of rambling... any thoughts?https://gitlab.mpi-sws.org/iris/iris/-/issues/388Dropping support for Coq 8.102020-12-16T12:17:28ZTej Chajedtchajed@mit.eduDropping support for Coq 8.10At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the `"%H"` intro pattern without any additional work from the user.
- Custom entries [had some bugs](https://github.com/coq/coq/pull/11530) that seem to block their use in !554; in Coq 8.11 and forward we can give good notation for dfracs.
We should probably release Iris 3.4 before dropping support. Before that out of the current MRs I think !572 is the most important, to avoid releasing the mnat library and then immediately renaming it.At some point we should drop support for Coq 8.10.
The benefits are:
- Ltac2 is available starting with Coq 8.11. This would let us integrate https://gitlab.mpi-sws.org/iris/string-ident into Iris and support the `"%H"` intro pattern without any additional work from the user.
- Custom entries [had some bugs](https://github.com/coq/coq/pull/11530) that seem to block their use in !554; in Coq 8.11 and forward we can give good notation for dfracs.
We should probably release Iris 3.4 before dropping support. Before that out of the current MRs I think !572 is the most important, to avoid releasing the mnat library and then immediately renaming it.https://gitlab.mpi-sws.org/iris/iris/-/issues/380iDestruct does not handle some patterns that it probably could2020-11-11T16:57:53ZTej Chajedtchajed@mit.eduiDestruct does not handle some patterns that it probably couldThe pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though that could be processed as `iDestruct ... as H; done`. It does handle `H /=` (by running `simpl` after the destruct).The pattern match in `iDestructHypGo` misses a handful of patterns that perhaps it could process. For example `IDone` could probably be given a sensible interpretation.
Similarly `iDestructHypFindPat` complains about `H //` even though that could be processed as `iDestruct ... as H; done`. It does handle `H /=` (by running `simpl` after the destruct).https://gitlab.mpi-sws.org/iris/iris/-/issues/333Iris Library Best Practices2020-08-06T16:37:12ZRalf Jungjung@mpi-sws.orgIris Library Best PracticesWe should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @blaisorblade pointed out that it is non-obvious that specs should not contain `own` but instead wrap those things in their own definitions that depend on `libG` instead of `inG`.We should, as part of our documentation, have a document describing "iris library best practices" -- how to write a re-usable Iris module (think: cinv, na_inv, boxes, ...). Some of that is already in our proof guide, but in scattered form. Other aspects are not mentioned; @blaisorblade pointed out that it is non-obvious that specs should not contain `own` but instead wrap those things in their own definitions that depend on `libG` instead of `inG`.https://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/310Choose syntax and implement destructuring existentials with pure components, ...2021-03-24T12:42:23ZPaolo 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 `λ`.https://gitlab.mpi-sws.org/iris/iris/-/issues/296Use Coq deprecation attribute to implement deprecations2020-07-15T10:35:39ZTej Chajedtchajed@mit.eduUse Coq deprecation attribute to implement deprecationsNow that Iris only supports Coq 8.9+, we can use the [`#[deprecated]` attribute](https://coq.github.io/doc/master/refman/language/gallina-specification-language.html#coq:attr.deprecated) on any deprecated tactics or definitions. Deprecation warnings are nice because they can be either suppressed with `-w -deprecated` or turned into an error with `-w +deprecated`.
This immediately applies to:
- `iAlways`
- `algebra/deprecated.v`'s `cofeT` and `dec_agree` (`dec_agree` may need to be wrapped in a notation first)
Iris also has a few dynamic deprecations that Coq currently doesn't support. The IPM can detect these but currently (due to Coq limitations) has no way to raise a user-level deprecation warning.
- The deprecated `!#` intro pattern is parsed as `TIntuitionisticIntro` but then treated the same as `TModalIntro`.
- The `*` specialization pattern is deprecated and triggers a deprecation message using `idtac`.Now that Iris only supports Coq 8.9+, we can use the [`#[deprecated]` attribute](https://coq.github.io/doc/master/refman/language/gallina-specification-language.html#coq:attr.deprecated) on any deprecated tactics or definitions. Deprecation warnings are nice because they can be either suppressed with `-w -deprecated` or turned into an error with `-w +deprecated`.
This immediately applies to:
- `iAlways`
- `algebra/deprecated.v`'s `cofeT` and `dec_agree` (`dec_agree` may need to be wrapped in a notation first)
Iris also has a few dynamic deprecations that Coq currently doesn't support. The IPM can detect these but currently (due to Coq limitations) has no way to raise a user-level deprecation warning.
- The deprecated `!#` intro pattern is parsed as `TIntuitionisticIntro` but then treated the same as `TModalIntro`.
- The `*` specialization pattern is deprecated and triggers a deprecation message using `idtac`.Iris 3.3https://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/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.https://gitlab.mpi-sws.org/iris/iris/-/issues/283big_sepM2_fmap and friends only work for nat keys2019-12-20T15:28:54ZMichael Sammlerbig_sepM2_fmap and friends only work for nat keysIris version: dev.2019-11-22.2.a979391c
`big_sepM2_fmap`, `big_sepM2_fmap_l` and `big_sepM2_fmap_r` only work for maps with `nat` keys, but I don't see a fundamental reason for this. The problem is that they use `(Φ : nat → A' → B' → PROP)` instead of `(Φ : K → A' → B' → PROP)`. Let me know if I should open a PR which fixes this.Iris version: dev.2019-11-22.2.a979391c
`big_sepM2_fmap`, `big_sepM2_fmap_l` and `big_sepM2_fmap_r` only work for maps with `nat` keys, but I don't see a fundamental reason for this. The problem is that they use `(Φ : nat → A' → B' → PROP)` instead of `(Φ : K → A' → B' → PROP)`. Let me know if I should open a PR which fixes this.https://gitlab.mpi-sws.org/iris/iris/-/issues/280Documentation for installation on OS X2020-02-06T16:07:27ZJules JacobsDocumentation for installation on OS XPerhaps there could be an Install.md that describes the installation process to install Coq, Iris, and an IDE for Coq on OS X (and other platforms). Not everything works well on OS X. CoqIDE is extremely slow, for instance, and the main Coq extension for VS code does not work well, and OS X has an old version of Make that fails sometimes. VS Code + the maximedenes.vscoq for Coq + oijaz.unicode-latex for unicode input works reasonably well. What I eventually did was something like:
```
/usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
brew update
brew install make
brew install opam
opam init
eval $(opam env)
opam install coq
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-iris
brew install visual-studio-code
code --install-extension maximedenes.vscoq
code --install-extension oijaz.unicode-latex
```
A complete recipe like that might save new people a lot of time.Perhaps there could be an Install.md that describes the installation process to install Coq, Iris, and an IDE for Coq on OS X (and other platforms). Not everything works well on OS X. CoqIDE is extremely slow, for instance, and the main Coq extension for VS code does not work well, and OS X has an old version of Make that fails sometimes. VS Code + the maximedenes.vscoq for Coq + oijaz.unicode-latex for unicode input works reasonably well. What I eventually did was something like:
```
/usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
brew update
brew install make
brew install opam
opam init
eval $(opam env)
opam install coq
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam install coq-iris
brew install visual-studio-code
code --install-extension maximedenes.vscoq
code --install-extension oijaz.unicode-latex
```
A complete recipe like that might save new people a lot of time.