lambda-rust issueshttps://gitlab.mpi-sws.org/iris/lambda-rust/-/issues2021-11-15T22:59:10Zhttps://gitlab.mpi-sws.org/iris/lambda-rust/-/issues/7Improving coding style2021-11-15T22:59:10ZRalf Jungjung@mpi-sws.orgImproving 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
- [x] import "options" file everywhere that sets `Default Goal Selector`
- [x] En...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
- [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/lambda-rust/-/issues/2Port late master additions to weak_mem2018-09-01T13:48:26ZRalf Jungjung@mpi-sws.orgPort late master additions to weak_memSince the paper has been published, I made a few small additions to master as questions came up in discussions or as the standard library changed:
* [x] https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/505d86a5fbb85abd4e5fada1853136a...Since the paper has been published, I made a few small additions to master as questions came up in discussions or as the standard library changed:
* [x] https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/505d86a5fbb85abd4e5fada1853136ac690a60bf: `&mut T <-> &mut Cell<T>`
* [x] https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/ff244cf1b7deabfd9bc1e4eae0bc48db6aedbe77: `Box<T> <-> Box<Cell<T>>`
* [x] https://gitlab.mpi-sws.org/FP/LambdaRust-coq/commit/7da18513b7d41b50cc58cd08136115d59d42828e: `impl<T> Send for JoinHandle<T>`
* [x] e6a4bef: Faking a `&&mut`.
@haidang @jjourdan which of these still need porting to `weak_mem`?https://gitlab.mpi-sws.org/iris/lambda-rust/-/issues/1Fix allocation to make sure it uses a fresh block2018-07-27T10:59:34ZRalf Jungjung@mpi-sws.orgFix allocation to make sure it uses a fresh blockCurrently, we just check if the new locations are free. We should fix this discrepancy with the on-paper presentation.
Cc @jjourdanCurrently, we just check if the new locations are free. We should fix this discrepancy with the on-paper presentation.
Cc @jjourdan