Skip to content
Snippets Groups Projects

make it compatible with Coq 8.7, and test that

Merged make it compatible with Coq 8.7, and test that
ci/iris-update into master
Merged Ralf Jung requested to merge ci/iris-update into master

Turns out Coq 8.7 is 20% faster. :-) Some of this is lost to parallelism though, it seems.

8.6:

real	11m7.102s
user	25m5.797s
sys	0m17.457s

8.7:

real	9m0.417s
user	19m40.020s
sys	0m16.213s

I reported the fact that I had to change something to make it work again as https://coq.inria.fr/bugs/show_bug.cgi?id=5749.

Edited by Ralf Jung

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
theories/examples/rcu_data.v
222 221 Proof. by rewrite elem_of_of_list elem_of_rcu_info'. Qed.
223 222
224 223 Lemma rcu_dom'_cons H i b :
225 dom (gset _) ((i,b)::H) ≡ {[i]} ∪ dom (gset _) H.
224 dom (gset loc) ((i,b)::H) ≡ {[i]} ∪ dom (gset _) H.
226 225 Proof.
227 226 rewrite /= /RCUHist_dom => x. by rewrite elem_of_of_list fmap_cons.
228 227 Qed.
229 228
230 229 Lemma rcu_dom'_cons_in H i b (In: i ∈ dom (gset _) H):
231 dom (gset _) ((i,b)::H) ≡ dom (gset _) H.
230 dom (gset loc) ((i,b)::H) ≡ dom (gset _) H.
  • Ralf Jung added 2 commits

    added 2 commits

    Compare with previous version

  • Ralf Jung
    Ralf Jung @jung ·
    Author Owner

    I was able to get rid of two of the three erewrites again by using some more annotation (which I think is better here), but for some reason, that would not work in the third place, in fai.v.

  • Ralf Jung added 1 commit

    added 1 commit

    Compare with previous version

  • Ralf Jung added 1 commit

    added 1 commit

    Compare with previous version

  • Ralf Jung
    Ralf Jung @jung ·
    Author Owner

    Nvm, that one also doesn't work on CI for some reason. I stopped caring enough.^^

    So, if CI passes, this is read to be merged as far as I am concerned.

  • Ralf Jung changed the description

    changed the description

  • Ralf Jung added 1 commit

    added 1 commit

    • 015c416f - update for Coq Makefile hooks

    Compare with previous version

  • Robbert Krebbers added 1 commit

    added 1 commit

    • bcfe1b36 - Bump Iris and get rid of some annotations.

    Compare with previous version

  • Ralf Jung mentioned in commit 028d067c

    mentioned in commit 028d067c

  • Ralf Jung merged

    merged

    • Please register or sign in to reply