examples issueshttps://gitlab.mpi-sws.org/iris/examples/-/issues2023-08-09T12:47:19Zhttps://gitlab.mpi-sws.org/iris/examples/-/issues/20SPAM2023-08-09T12:47:19ZCarina Schmittcschmitt@mpi-klsb.mpg.deSPAMSPAM issue plese ignoteSPAM issue plese ignotehttps://gitlab.mpi-sws.org/iris/examples/-/issues/18Bump Iris version to get more recent stdpp version (blocking coq/coq#16920)2023-04-14T08:38:20ZOlivier LaurentBump Iris version to get more recent stdpp version (blocking coq/coq#16920)Coq-ci is using `coq-iris-heap-lang` version `dev.2023-03-10.0.45e5a052` through `coq-iris-examples.opam`.
What would be a good choice of new version to take benefits from changes in std++ which look to be integrated in iris in commit 80...Coq-ci is using `coq-iris-heap-lang` version `dev.2023-03-10.0.45e5a052` through `coq-iris-examples.opam`.
What would be a good choice of new version to take benefits from changes in std++ which look to be integrated in iris in commit 80e0a15f?
This is blocking PR coq/coq#16920.
@prouxhttps://gitlab.mpi-sws.org/iris/examples/-/issues/13Improve coding style2021-07-23T16:30:01ZRalf Jungjung@mpi-sws.orgImprove coding styleIt would be a good idea to also enforce (via CI) the coding style improvements we have in Iris, here in the examples project:
- [x] no auto-generated names -- mostly done, some files missing:
- [x] `logrel/stlc/fundamental.v`
- [x] `...It would be a good idea to also enforce (via CI) the coding style improvements we have in Iris, here in the examples project:
- [x] no auto-generated names -- mostly done, some files missing:
- [x] `logrel/stlc/fundamental.v`
- [x] `logrel/F_mu_ref_conc/unary/logrel.v`
- [x] `logrel/F_mu_ref_conc/binary/logrel.v`
- [x] import "options" file everywhere that sets `Default Goal Selector`
- [x] Enforce `Local`/`Global` via our `coq-lint.sh`
Then we also should enable CI for MRs the same way we do for Iris.https://gitlab.mpi-sws.org/iris/examples/-/issues/9Logical relation with fundamental theorem and logical compatibility lemmas2020-10-01T12:21:49ZRalf Jungjung@mpi-sws.orgLogical relation with fundamental theorem and logical compatibility lemmasFor example, the lemmas in https://gitlab.mpi-sws.org/iris/examples/blob/master/theories/logrel/F_mu_ref/fundamental_binary.v use meta-level implication. These should all be strengthened magic wands.
On the other hand, the logical relat...For example, the lemmas in https://gitlab.mpi-sws.org/iris/examples/blob/master/theories/logrel/F_mu_ref/fundamental_binary.v use meta-level implication. These should all be strengthened magic wands.
On the other hand, the logical relation on `logrel_heaplang` does not have a syntactic type system, and hence no fundamental lemma proven in Coq.
Cc @robbertkrebbers @dfruminhttps://gitlab.mpi-sws.org/iris/examples/-/issues/12Fix build with Coq 8.122020-08-07T08:45:08ZRalf Jungjung@mpi-sws.orgFix build with Coq 8.12Building this repository with the Coq 8.12 beta is currently broken:
```
File "./theories/barrier/proof.v", line 120, characters 4-58:
Error: No matching clauses for match.
```
Somehow, `set_solver` fails to solve a goal that it was able...Building this repository with the Coq 8.12 beta is currently broken:
```
File "./theories/barrier/proof.v", line 120, characters 4-58:
Error: No matching clauses for match.
```
Somehow, `set_solver` fails to solve a goal that it was able to handle fine before. @robbertkrebbers could you look into this?https://gitlab.mpi-sws.org/iris/examples/-/issues/6Add Derek's keynote example2020-06-12T10:53:23ZRalf Jungjung@mpi-sws.orgAdd Derek's keynote exampleAs in, merge https://gitlab.mpi-sws.org/swasey/derek-popl18-talk/As in, merge https://gitlab.mpi-sws.org/swasey/derek-popl18-talk/David SwaseyDavid Swaseyhttps://gitlab.mpi-sws.org/iris/examples/-/issues/8Fix concurrent stacks for more realistic CAS2019-03-06T12:42:02ZRalf Jungjung@mpi-sws.orgFix concurrent stacks for more realistic CAShttps://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/165 made CAS more realistic, which broke the concurrent stacks in the [ci/gen_proofmode](https://gitlab.mpi-sws.org/FP/iris-examples/tree/ci/gen_proofmode) branch. All four of them co...https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/165 made CAS more realistic, which broke the concurrent stacks in the [ci/gen_proofmode](https://gitlab.mpi-sws.org/FP/iris-examples/tree/ci/gen_proofmode) branch. All four of them contain a CAS comparing arbitrary values, which I do not think is possible in a lock-free way.
I asked Danny to have a look at this; I don't think he has an account here.https://gitlab.mpi-sws.org/iris/examples/-/issues/10LICENSE is missing2018-12-10T17:02:41ZRobbert KrebbersLICENSE is missingThere is no LICENCE in this development. I propose using BSD3 like Iris, but I'm open to alternatives.There is no LICENCE in this development. I propose using BSD3 like Iris, but I'm open to alternatives.https://gitlab.mpi-sws.org/iris/examples/-/issues/7Fix hocap for more realistic CAS2018-07-04T13:56:24ZRalf Jungjung@mpi-sws.orgFix hocap for more realistic CAShttps://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/165 made CAS more realistic, which broke HoCAP in the [ci/gen_proofmode](https://gitlab.mpi-sws.org/FP/iris-examples/tree/ci/gen_proofmode) branch. `hocap/fg_bag.v` contains a CAS com...https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/165 made CAS more realistic, which broke HoCAP in the [ci/gen_proofmode](https://gitlab.mpi-sws.org/FP/iris-examples/tree/ci/gen_proofmode) branch. `hocap/fg_bag.v` contains a CAS comparing arbitrary values, which I do not think is possible in a lock-free way.
@dfrumin could you have a look at this?Dan FruminDan Fruminhttps://gitlab.mpi-sws.org/iris/examples/-/issues/4Dedicated make targets2018-02-16T09:47:02ZRalf Jungjung@mpi-sws.orgDedicated make targets@amintimany reports that some of his projects that we are considering to add take pretty long to compile. We should provide `make` targets that only compile one particular project, to make it easier for people to look at a particular ca...@amintimany reports that some of his projects that we are considering to add take pretty long to compile. We should provide `make` targets that only compile one particular project, to make it easier for people to look at a particular case study they are interested in.
I can experiment with that, once we have something in the repo.Ralf Jungjung@mpi-sws.orgRalf Jungjung@mpi-sws.orghttps://gitlab.mpi-sws.org/iris/examples/-/issues/5Add stack with helping2018-01-12T15:36:09ZRobbert KrebbersAdd stack with helpinghttp://iris-project.org/artifacts/2017-case-study-concurrent-stacks-with-helping.tar.gzhttp://iris-project.org/artifacts/2017-case-study-concurrent-stacks-with-helping.tar.gzAleš Bizjakales@alesb.comAleš Bizjakales@alesb.comhttps://gitlab.mpi-sws.org/iris/examples/-/issues/3Add spanning tree proof2017-12-15T09:16:52ZRalf Jungjung@mpi-sws.orgAdd spanning tree proofI heard that @amintimany has a port of FCSL's spanning tree algorithm to Iris. That would be a good candidate to be added here, wouldn't it? @amintimany, which version of Iris is it working with?I heard that @amintimany has a port of FCSL's spanning tree algorithm to Iris. That would be a good candidate to be added here, wouldn't it? @amintimany, which version of Iris is it working with?Amin TimanyAmin Timanyhttps://gitlab.mpi-sws.org/iris/examples/-/issues/2Add IPM logical relation2017-12-15T09:13:18ZRalf Jungjung@mpi-sws.orgAdd IPM logical relationIt would be great to have the IPM logical relation in iris-examples. AFAIK, @amintimany has this on his TODO-list.It would be great to have the IPM logical relation in iris-examples. AFAIK, @amintimany has this on his TODO-list.Amin TimanyAmin Timanyhttps://gitlab.mpi-sws.org/iris/examples/-/issues/1Does not compile with latest Iris2017-10-28T13:20:11ZRalf Jungjung@mpi-sws.orgDoes not compile with latest IrisMostly due to the big rename MRMostly due to the big rename MRRobbert KrebbersRobbert Krebbers