Fix the examples / solution files for latest Iris.

We fix the tutorial so that it works with the development version of Iris.

Before merging, there is a small issue that should be looked into (see the FIXMEs): a previously working instance of wp_apply has been replaced (there are several occurrences of that) by a wp_bind (_ ||| _)%E followed by an iApply. Is that an Iris bug?

Fixes #2 (closed)

mentioned in issue #2 (closed)

changed the description

I will take care of adding the usual pinning infrastructure before we merge this PR.

Seems to me we should just state wp_par with value lambdas then?

Isn't that par_spec?

No, that doesn't have the thunking.

I'm not sure what's the use of that. It will look pretty ugly since we do not have a notation for ||| with value lambdas (and I'm not at all convinced we would want such a notation).

For all practical matters, wouldn't it be better to just use par_spec?

It would be nice if we could avoid having to do wp_lam. We didn't write a thunk, after all.

There is a thunk implicitly, so I don't mind if the user has to be aware of that.

Anyway, what are the alternatives:

• Have a lemma for par (LamV <> e) (LamV <> e).
• Make a notation for par (LamV <> e) (LamV <> e) and state the lemma in terms of that notation.

None of these appear appealing to me.

Have a lemma for par (LamV <> e) (LamV <> e).

That's what I am proposing. I think we can write (λ _, e)%V for (LamV <> e).

Not a huge fan of that.

By the way, there is a worse problem when defining things like while loops. There you would hope to have the usual spec:

WP if e1 then (e2; while e1 do e2) else #() {{ Φ }} -∗
WP while e1 do e2 {{ Φ }}}

But this only works in case while is a version with lambda-values for the thunks. If you would write it analogous to the way you propose for par, you end up with:

WP if e1 then (e2; while (λ <>, e1)%V (λ <>, e2)%V) else #() {{ Φ }} -∗
WP while (λ <>, e1)%V (λ <>, e2)%V {{ Φ }}}

Which is rather ugly. If you write the lemma without thunking, you end up with:

WP if v1 #() then (v2 #(); while v1 v2) else #() {{ Φ }} -∗
WP while v1 v2 {{ Φ }}}

Which is not great either...

Not a huge fan of that.

I don't understand why. I also don't understand why you bring up while.

par (λ _, e1)%V (λ _, e2)%V is the shape that the expressions will always have in the moment the user can apply wp_par. So it makes perfect sense to state the lemma that way. Is the lack of notation your only concern?

I don't understand why.

Because the spec using value lambdas does not use the notation.

I also don't understand why you bring up while.

Because there we have exactly the same issues:

• while takes thunks as arguments, like par.
• the notation for while will be stated using thunks, like par.
• these thunks have to be turned into value lambdas.
• stating the spec using value lambdas is ugly, which is the same problem we are having here for par.

Because the spec using value lambdas does not use the notation.

I agree the spec is less readable than it should, but I think that's worth the trade-off for producing more readable goals after being applied. This is weighing displaying the proof state right after iApply wp_par in any user of this spec against readability of the spec.

Actually it's not even a trade-off, because if you don't like wp_par you can use par_spec in your proofs. But I don't understand why you want to force everyone else to have an uglier proof state.

Just to get things clear: By saying that I'm not a huge fan of wp_par the way you would like to state it, I'm not necessarily suggesting to remove it, I'm mostly wondering if we can do better and pointing out where similar issues appear (c.f. the while example) so that we can come up with a uniform solution.

Also, it would be good if we have some way of making clear to users when to use which specs. For a novice user it's not really clear when to use neither wp_par nor par_spec. (And not just notice users, which is witnessed by the fact this issue exists in the first place).

I'm mostly wondering if we can do better and pointing out where similar issues appear (c.f. the while example) so that we can come up with a uniform solution.

Ah I see. Makes sense.

I don't think I can come up with anything better than redundant notation, though.

I made a proposal at https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/210, to at least move us a bit into the right direction (and to unblock this MR).

mentioned in merge request iris!210 (merged)

added 2 commits

• 9d4bb10d - 1 commit from branch master
• c7d3c88b - Merged from master.

Compare with previous version

added 9 commits

• c7d3c88b...43cf91c4 - 7 commits from branch master
• 5efd4e91 - Merged from master.
• 9a31dcc8 - Merge branch 'master' into latest_iris

Compare with previous version

I think we are ready for merging, up to version information, but I don't really know what version number to point to. What I known is that everything works fine with dev.2019-01-22.0.b85a3cfc. What should I do @jung?

@lepigre then please point it to that specific version in the opam file. It's as good as any...

These fixed references do not make much sense any more, but I can edit the README after we merge this.

OK, I guess we should recommend obtaining the dependencies with opam now. You seem to know more about that than I do, so I'll let you edit the README.

added 1 commit

• 7e44373e - Compatible [iris-coq] version in the [opam] file.

Compare with previous version

mentioned in commit 53a92a4e

merged

Thanks!

Oh, seems I missed this change. I reverted it. The goal is to keep the Makefile exactly the same across all our projects. That makes it much easier to make sure all projects got the latest version -- even if it means that some projects carry directives they do not need.

The reason why I removed it is that it makes make clean fail on this project. Neither theories nor tests exist in this repository, so find just fails.

Oh, good point. Seems like I will have to make our generic Makefile even more generic...

Why not just use find . ...?

I have local opam switches in these directories, and find would go and delete files in them.

mentioned in merge request !3 (merged)