gpfsl issueshttps://gitlab.mpi-sws.org/iris/gpfsl/-/issues2022-08-12T12:11:41Zhttps://gitlab.mpi-sws.org/iris/gpfsl/-/issues/12"Hint Mode" missing2022-08-12T12:11:41ZRalf Jungjung@mpi-sws.org"Hint Mode" missingThe orc11 library declares several typeclasses and none of them has a `Hint Mode`. That's a problem, every class should have a `Hint Mode` as otherwise TC search tends to go into loops.
This is probably the cause of the CI failure in ht...The orc11 library declares several typeclasses and none of them has a `Hint Mode`. That's a problem, every class should have a `Hint Mode` as otherwise TC search tends to go into loops.
This is probably the cause of the CI failure in https://gitlab.mpi-sws.org/iris/lambda-rust/-/pipelines/33601.
Cc @haidang @jjourdanhttps://gitlab.mpi-sws.org/iris/gpfsl/-/issues/6Stale files that are not in _CoqProject2021-04-07T20:43:51ZRobbert KrebbersStale files that are not in _CoqProjectI noted theories/examples/snapshot.v is not in the _CoqProject file. Such files should either be removed or added to the _CoqProject.I noted theories/examples/snapshot.v is not in the _CoqProject file. Such files should either be removed or added to the _CoqProject.https://gitlab.mpi-sws.org/iris/gpfsl/-/issues/3Porting LARA2021-04-07T20:44:38ZHai DangPorting LARAWe need to port LARA from iGPS to GPFSL. The following files are to be ported:
* [x] /logically_atomic.v → /logic/logically_atomic.v
* [x] /invariants.v → /logic/obj_invariants.v
* [x] /examples/snapshot.v → /examples/frac_auth.v and sn...We need to port LARA from iGPS to GPFSL. The following files are to be ported:
* [x] /logically_atomic.v → /logic/logically_atomic.v
* [x] /invariants.v → /logic/obj_invariants.v
* [x] /examples/snapshot.v → /examples/frac_auth.v and snapshot.v
* [x] ~~/examples/hist_protocol.v?~~
* [x] /examples/list_lemmas.v → /base_logic/list_lemmas.v
* [x] /examples/abs_hashtable.v → /examples/abs_hashtable.v
* [ ] /examples/hashtable.v
* [x] /examples/for_loop.v → /logic/for_loop.v
* [x] /examples/repeat.v → /logic/repeat.v
* [x] /examples/kvnode.v → /examples/kvnode.v
* [ ] /examples/kvnode2.v
* [ ] /gps/shared2.v
* [ ] ~~recursive protocol?~~Hai DangHai Danghttps://gitlab.mpi-sws.org/iris/gpfsl/-/issues/2Tactics issues2019-02-11T09:21:05ZHai DangTactics issuesI was trying to use `iInv` to open an Iris invariant around an iProp WP. `iInv` fails, I think, because it cannot solve `atomic`.
Somehow the instance `base_atomic_atomic` was not used. I was able to use it manually though (see https://g...I was trying to use `iInv` to open an Iris invariant around an iProp WP. `iInv` fails, I think, because it cannot solve `atomic`.
Somehow the instance `base_atomic_atomic` was not used. I was able to use it manually though (see https://gitlab.mpi-sws.org/FP/gpfsl/blob/sc_inv/theories/sc_invariants.v).
Another one is that `wp_write` currently doesn't support `l ↦ ?`, which I doubt that it's due to Coq not being able to match against `?`. Should we change the notation then?
@jjourdanhttps://gitlab.mpi-sws.org/iris/gpfsl/-/issues/1Non-equal comparison2018-05-11T16:46:18ZHai DangNon-equal comparison@jjourdan
I look at the sequential LambdaRust and it seems that `lit_neq` is deterministic. `lit_neq` returns `true` if only the two locations are known to be syntactically inequal. So when they are syntactically equal and one of them ...@jjourdan
I look at the sequential LambdaRust and it seems that `lit_neq` is deterministic. `lit_neq` returns `true` if only the two locations are known to be syntactically inequal. So when they are syntactically equal and one of them is unallocated, they are definitely equal?
Is this in between what LLVM does (i.e. with the bitwise rules and aliasing rules from [Ralf's question][1]) and what C allows?
[1]: https://internals.rust-lang.org/t/comparing-dangling-pointers/3019