Skip to content
Snippets Groups Projects
Ralf Jung's avatar
closed merge request !59 "Add Chase-Lev deque" at Iris / examples
Ralf Jung's avatar
commented on merge request !59 "Add Chase-Lev deque" at Iris / examples

This issue has remain unresolved for a while now, so I'll close this MR. Thanks for your contribution! However, I'm afraid we don't have the capaci...

Ralf Jung's avatar
commented on merge request !49 "Added petersons algorithm as an example of sequential consistency" at Iris / examples

@jihgfee do you still plan to get back to this? There are some review comments above.

Ralf Jung's avatar
commented on merge request !69 "two more styles of lock spec" at Iris / examples

Thanks! I left some comments, they apply to both files....

Ralf Jung's avatar
commented on merge request !69 "two more styles of lock spec" at Iris / examples

Please don't keep commented-out code around.

Ralf Jung's avatar
commented on merge request !69 "two more styles of lock spec" at Iris / examples

Please add some more comments explaining what is happening here... I think the point of this is just to implement the interface? It's confusing tha...

Ralf Jung's avatar
commented on merge request !69 "two more styles of lock spec" at Iris / examples

This should be called _fractional

Ralf Jung's avatar
pushed to branch master at Iris / examples
Robbert Krebbers's avatar
accepted merge request !70 "Add annotations to avoid evars" at Iris / examples
Robbert Krebbers's avatar
pushed to branch master at Iris / examples
Robbert Krebbers's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples

Gitlab can squash on merge.

Quentin VERMANDE's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples

Should I also squash?

Quentin VERMANDE's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples

It does solve the slow dones (this is actually most of the time saved).

Robbert Krebbers's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples

Yes, sealing bin_log_related seems like the way to go....

Robbert Krebbers's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples

These big lines with multiple chained tactics in first are quite hard to maintain. If you could change as above, that would be great.

Robbert Krebbers's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples
    iApply (interp_expr_bind' [FstCtx] [FstCtx])....
Quentin VERMANDE's avatar
commented on merge request !70 "Add annotations to avoid evars" at Iris / examples

Digging a little bit on the constants involved, I guess you wanted me to seal envs_entails, but it is already (partially) sealed. I ended up sealing ...

Ralf Jung's avatar
pushed to branch master at Iris / examples
Robbert Krebbers's avatar
pushed to branch master at Iris / examples
  • 593cca1f · Bump Iris (Transfinite algebra).
Ralf Jung's avatar
pushed to branch master at Iris / examples