stdpp merge requestshttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests2021-12-01T07:42:29Zhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/341Add bool_to_Z2021-12-01T07:42:29ZMichael SammlerAdd bool_to_ZThis MR adds `bool_to_Z` which has been used as `Z_of_bool` in both RefinedC and [RustBelt](https://gitlab.mpi-sws.org/search?search=Z_of_bool&group_id=1795&project_id=178&scope=&search_code=true&snippets=false&repository_ref=master&nav_...This MR adds `bool_to_Z` which has been used as `Z_of_bool` in both RefinedC and [RustBelt](https://gitlab.mpi-sws.org/search?search=Z_of_bool&group_id=1795&project_id=178&scope=&search_code=true&snippets=false&repository_ref=master&nav_source=navbar).
There is not much theory for it as most of the time one can reason about it by computation.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/340Lemmas for lookup on mjoin2021-11-26T09:48:47ZMichael SammlerLemmas for lookup on mjoinhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/10Add monadic `;;` and change level of the do-notation to 1002021-11-25T13:17:03ZRobbert KrebbersAdd monadic `;;` and change level of the do-notation to 100While trying to port some of the IPM tactics from Ltac to Mtac2 (formerly MetaCoq) I ran into the issue that `_ ;; _` was used at a different level in both Iris and Mtac2, making it impossible to combine both projects. The current levels...While trying to port some of the IPM tactics from Ltac to Mtac2 (formerly MetaCoq) I ran into the issue that `_ ;; _` was used at a different level in both Iris and Mtac2, making it impossible to combine both projects. The current levels are as follows:
| | `_ ;; _` | `_ <- _; _` |
|------------------|----------------|--------------|
| std++ | not present | 65 |
| Iris's heap_lang | 100 | not present |
| Mtac2 | 81 | 81 |
As you can see, the levels are all different!
Some notes:
- I think `_ ;; _` and `_ <- _; _` should be at the same level.
- The notation `_ ;; _` is not present in stdpp, but it should be there:
```coq
Notation "x ;; z" := (x ≫= λ _, z).
```
- If we currently add this notation, using the same level as `_ <- _; _`, namely 65, it will currently Iris.
This MR changes the level of `_ <- _; _` in std++ into 100, which is consistent with Iris. When we accept this MR, a one line fix for Iris is needed.
The main consequence of this MR is how these notations will interact with equality. Consider:
```
m1 = m2 ;; m3
```
Should that be parsed as:
1. `(m1 = m2) ;; m3` (now)
2. `m1 = (m2 ;; m3)` (before)
I'd say that when the notation is used for an imperative programming language, like Iris's `heap_lang`, it should definitely be (1). However, in the case of monadic code, (1) makes very little sense (at least for equality, but maybe it makes sense for other relations), as it will never type check.
Note that many other relations like setoid equality and inequality of numbers are also at level 70.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/337Upstreaming a small collection of lemmas2021-11-25T02:33:50ZMichael SammlerUpstreaming a small collection of lemmasThis MR upstreams a small collection of lemmas from Islaris.This MR upstreams a small collection of lemmas from Islaris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/338Add reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_Some2021-11-24T20:50:26ZMichael SammlerAdd reverse_lookup, reverse_lookup_Some and alternative version of sublist_lookup_SomeThis MR adds `reverse_lookup`, `reverse_lookup_Some` and an alternative version of `sublist_lookup_Some`This MR adds `reverse_lookup`, `reverse_lookup_Some` and an alternative version of `sublist_lookup_Some`https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/336Fix coq-lint.sh on macOS2021-11-23T20:43:21ZTej Chajedtchajed@gmail.comFix coq-lint.sh on macOSFixes the build on macOS. Once this is merged I'll make the same fix to Iris.Fixes the build on macOS. Once this is merged I'll make the same fix to Iris.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/335Add lemma `map_subseteq_inv`.2021-11-22T15:12:14ZRobbert KrebbersAdd lemma `map_subseteq_inv`.As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing
It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the p...As pointed out by @swils in https://mattermost.mpi-sws.org/iris/pl/wzsucg5swtrttqhsawdd8pzama this lemma is missing
It's all the way down the file since I need properties of ∖. If someone knows a (short) proof without, we can move the property up, closer towards other properties on the order.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/334normalize for Fail printing locations2021-11-13T02:07:06ZRalf Jungjung@mpi-sws.orgnormalize for Fail printing locationsAdjusts test suite for https://github.com/coq/coq/pull/15174Adjusts test suite for https://github.com/coq/coq/pull/15174https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/333std++ 1.6.0 release notes2021-11-05T17:28:26ZTej Chajedtchajed@gmail.comstd++ 1.6.0 release notesCreating a new std++ release will fix #119, and allow us to release Iris 3.5.0.
This is a pretty big release, with over 400 commits from 14 authors!
I got the author list with `git shortlog --summary coq-stdpp-1.5.0..HEAD | gsed -E 's/...Creating a new std++ release will fix #119, and allow us to release Iris 3.5.0.
This is a pretty big release, with over 400 commits from 14 authors!
I got the author list with `git shortlog --summary coq-stdpp-1.5.0..HEAD | gsed -E 's/[ \\t]+/ /g' | cut -d' ' -f3-100`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/327countable.v: prove choose_proper2021-11-05T17:07:35ZPaolo G. Giarrussocountable.v: prove choose_proper~~Needs the misplaced `Acc_rect_max`.~~
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.~~Needs the misplaced `Acc_rect_max`.~~
Add missing properness lemma for choose.
Very first step towards "Pragmatic quotients" (haven't done the others yet), but meaningful on its own.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/332base.v: fix typo in comment about MonadSet, and extend2021-10-26T14:00:05ZPaolo G. Giarrussobase.v: fix typo in comment about MonadSet, and extendThe comment hints at `listset_nodup`, which does _not_ have a MonadSet instance.The comment hints at `listset_nodup`, which does _not_ have a MonadSet instance.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/329Mark set_size and set_fold as TC opaque2021-10-26T12:51:32ZPaolo G. GiarrussoMark set_size and set_fold as TC opaqueUpdated according to suggestions.
-------
Old title/description:
More TC opaqueness (appropriate???)
Take these as questions, and feel free to edit/close/... . Follow up from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/328.Updated according to suggestions.
-------
Old title/description:
More TC opaqueness (appropriate???)
Take these as questions, and feel free to edit/close/... . Follow up from https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/328.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/331Add Arguments bool_decide : simpl never2021-10-25T08:01:18ZMichael SammlerAdd Arguments bool_decide : simpl neverAs discussed on Mattermost, I've encountered a case where simpl on a goal containing bool_decide took 1.5 seconds without making any progress, but was instantaneous after adding `Arguments bool_decide : simpl never.` .As discussed on Mattermost, I've encountered a case where simpl on a goal containing bool_decide took 1.5 seconds without making any progress, but was instantaneous after adding `Arguments bool_decide : simpl never.` .https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/330Normalize focused goal output2021-10-13T17:36:37ZTej Chajedtchajed@gmail.comNormalize focused goal outputMerge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.
std++ does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the ...Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.
std++ does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/328fin_sets: add missing Params instance for `set_map`2021-10-05T18:27:36ZPaolo G. Giarrussofin_sets: add missing Params instance for `set_map`Noticed from VERY slow rewrites.Noticed from VERY slow rewrites.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/325f_equiv optimizations2021-10-02T15:12:18ZRalf Jungjung@mpi-sws.orgf_equiv optimizationsThis makes f_equiv a lot faster.
The first commit is inspired by looking at [this line](https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L105) in Perennial: the ver...This makes f_equiv a lot faster.
The first commit is inspired by looking at [this line](https://github.com/mit-pdos/perennial/blob/3ebb6f05456e2378e687e7eb99c30001930ff396/src/program_logic/crash_weakestpre.v#L105) in Perennial: the very first f_equiv there takes 30s. 20s of that are spent in `simple apply (_ : Proper (R ==> R) f)`, where `f` is `bi_and <some complicated term>` -- basically is tries to treat bi_and as a unary function and takes forever to realize that will not work. There is no TC trace for this, so this must be all unification time. By changing the pattern for this arm from `?R (?f _) _` to `?R (?f _) (?f _)` we avoid entering it unless things match *syntactically*. This seeds up the first f_equiv from 30s to 10s.
The second commit is born from looking at that same line more, and also looking at [the equivalent line in Iris itself](https://gitlab.mpi-sws.org/iris/iris/-/blob/467fa48bc66c2f2459f379a69fd9a41840599e23/iris/program_logic/weakestpre.v#L122): according to the ltac profiler, almost all time is spent in `try simple apply reflexivity` -- again, unification of inequal terms being very slow. So we now do entirely syntactic unification before even trying this. This speeds up the `do 23 (f_contractive || f_equiv)` in Iris from 1.3s to 0.6s, and it speeds up the `do 22 (f_contractive || f_equiv)` in Perennial to 0.75s from originally 42s (22s after the previous commit) -- a whopping 50x overall improvement!
Later commits slightly relax this to fix compatibility, so the fallback cases now do perform unification to match up the functions on the left-hand and right-hand side -- but this barely slows down the benchmarks mentioned above since they do not usually hit those cases. In fact, both in the Iris and Perennial case, 66% of the time is now spent in `f_contractive`.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/326f_equiv: slightly better support for function relations2021-09-27T14:17:27ZRalf Jungjung@mpi-sws.orgf_equiv: slightly better support for function relationsThis makes f_equiv more powerful: with it we can solve goals of the form `f x ≡ g x` where `f, g: X -d> OFE` and `f ≡ g`. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applie...This makes f_equiv more powerful: with it we can solve goals of the form `f x ≡ g x` where `f, g: X -d> OFE` and `f ≡ g`. We still make no attempt at solving goals where the arguments are different. I think in all cases where this applies, it will finish the proof, so I added a `solve`.
I also added the testcases from https://gitlab.mpi-sws.org/iris/stdpp/-/commit/d16ab1aaa77ed3a9b052d12496d92c102288b704.https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/323add size_set_seq2021-09-13T21:16:30ZRalf Jungjung@mpi-sws.orgadd size_set_seqhttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/324add size_difference2021-09-10T15:07:06ZRalf Jungjung@mpi-sws.orgadd size_differencehttps://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/322Revert "Merge branch 'robbert/sprop' into 'master'"2021-09-08T21:26:20ZRalf Jungjung@mpi-sws.orgRevert "Merge branch 'robbert/sprop' into 'master'"This reverts merge request !309. It turned out to be a breaking change due to shadowing imports, and also cause performance regression in at least one case (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/732#note_73457).This reverts merge request !309. It turned out to be a breaking change due to shadowing imports, and also cause performance regression in at least one case (see https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/732#note_73457).