Example code in exercises does not work with latest version of Iris
Some of the provided code doesn't work in the exercises. I'm using the latest version of Iris (FP/iris-coq@fb211a177abf). There were some easy fixes but I got stuck on using
ex_01_swap.v, some uses of
wp_lamhave to be replaced with
.coqdeps.dshould be under gitignore
- The use of
wp_apply (wp_par ...)in
ex_04_parallel_add.vdoesn't work - I couldn't fix it myself, the code looks to me like it should work as written.