Skip to content

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 wp_par.

  • In ex_01_swap.v, some uses of wp_lam have to be replaced with wp_let.
  • .coqdeps.d should be under gitignore
  • The use of wp_apply (wp_par ...) in ex_04_parallel_add.v doesn't work - I couldn't fix it myself, the code looks to me like it should work as written.