update build system; support Coq 8.7

.gitlab-ci.yml

@@ -13,7 +13,7 @@ variables:
   # build
   - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
   - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
-  - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \(user: [0-9]" | tee build-time.txt'
+  - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
   - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
   cache:
     key: "coq.$COQ_VERSION-ssr.$SSR_VERSION"
@@ -23,12 +23,18 @@ variables:
   - master
   - /^ci/
 
-iratomic-coq8.6.1:
+build-coq8.7:
+  <<: *template
+  variables:
+    COQ_VERSION: "8.7.dev"
+    SSR_VERSION: "dev"
+
+build-coq8.6.1:
   <<: *template
   variables:
     COQ_VERSION: "8.6.1"
     SSR_VERSION: "1.6.1"
-    VALIDATE: 1
+    VALIDATE: "1"
   artifacts:
     paths:
     - build-time.txt

awk.Makefile

@@ -19,17 +19,16 @@
 	next
 }
 
-# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring
+# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring
 # that the .vio files are up-to-date, and (b) only schedule vio2vo for those
 # files where the .vo is *older* than the .vio.
 /^vio2vo:/ {
-	print "vio2vo:";
+	print "quick2vo:";
 	print "\t@make -j $(J) quick"
-	print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\"
+	print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\"
 	print "\t echo \"VIO2VO: $$VIOFILES\"; \\"
-	print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
-	getline;
-	next
+	print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
+	print ".PHONY: quick2vo"
 }
 
 # This forwards all unchanged lines

opam

@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_atomic" ]
 depends: [
-  "coq-iris" { (= "dev.2017-09-21.3") | (= "dev") }
+  "coq-iris" { (= "dev.2017-09-27.1") | (= "dev") }
 ]

theories/peritem.v

@@ -47,7 +47,7 @@ Section proofs.
   Lemma new_bag_spec:
     {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
   Proof.
-    iIntros (Φ) "HΦ". iApply wp_fupd.
+    iIntros (Φ) "_ HΦ". iApply wp_fupd.
     wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
     wp_alloc s as "Hs".
     iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".