Merge branch 'master' into latest_iris

.gitignore

@@ -27,3 +27,7 @@ _*_.tex
 *.v.d
 *.vio
 Makefile.coq*
+*.crashcoqide
+.coqdeps.d
+build-dep
+_opam

.gitlab-ci.yml

+image: ralfjung/opam-ci:opam2
+
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+
+.template: &template
+  stage: build
+  tags:
+  - fp
+  script:
+  - git clone https://gitlab.mpi-sws.org/iris/ci.git ci -b opam2
+  - ci/buildjob
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - opamroot/
+  only:
+  - master
+  - /^ci/
+  except:
+  - triggers
+  - schedules
+
+## Build jobs
+
+build-coq.8.8.2:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.8.2   coq-mathcomp-ssreflect version 1.7.0"
+
+build-coq.8.7.2:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.7.2   coq-mathcomp-ssreflect version 1.7.0"
+
+build-coq.8.6.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.7.0"

Makefile

+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	+@make -f Makefile.coq $@
+
+all: Makefile.coq
+	+@make -f Makefile.coq all
+.PHONY: all
+
+clean: Makefile.coq
+	+@make -f Makefile.coq clean
+	rm -f Makefile.coq
+.PHONY: clean
+
+# Create Coq Makefile.
+Makefile.coq: _CoqProject Makefile
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+
+# Install build-dependencies
+build-dep/opam: opam Makefile
+	@echo "# Creating build-dep package."
+	@mkdir -p build-dep
+	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
+	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
+
+build-dep: build-dep/opam phony
+	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
+	@# that are incompatible with our build requirements.
+	@# To achieve this, we create a fake opam package that has our build-dependencies as
+	@# dependencies, but does not actually install anything itself.
+	@echo "# Pinning build-dep package." && \
+	  if opam --version | grep "^1\." -q; then \
+	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
+	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
+	  else \
+	    opam install $(OPAMFLAGS) build-dep/; \
+	  fi
+
+# Some files that do *not* need to be forwarded to Makefile.coq
+Makefile: ;
+_CoqProject: ;
+opam: ;
+
+# Phony wildcard targets
+phony: ;
+.PHONY: phony

README.md

@@ -9,8 +9,8 @@ This tutorial comes in two versions:
 
 For the tutorial material you need to have the following dependencies installed:
 
-- Coq 8.6.1 / 8.7.0 / 8.7.1
-- Ssreflect 1.6.4
+- Coq 8.6.1 / 8.7.2 / 8.8.2
+- Ssreflect 1.7.0
 - Coq-std++ 1.1
 - Iris (latest version)
 
@@ -34,10 +34,10 @@ Then you can do `opam install coq-iris`.
 If you are unable to use opam, you can also build Iris from source. For this,
 run `make; make install` for all of:
 
-* ssreflect: <https://github.com/math-comp/math-comp/archive/mathcomp-1.6.4.tar.gz>
+* ssreflect: <https://github.com/math-comp/math-comp/archive/mathcomp-1.7.0.tar.gz>
   (`cd mathcomp/ssreflect` to only compile and install what is needed)
-* std++: <https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/repository/coq-stdpp-1.1.0/archive.tar.gz>
-* Iris: <https://gitlab.mpi-sws.org/FP/iris-coq/-/archive/master/iris-coq-master.tar.gz>
+* std++: <https://gitlab.mpi-sws.org/iris/stdpp/repository/coq-stdpp-1.1.0/archive.tar.gz>
+* Iris: <https://gitlab.mpi-sws.org/FP/iris-coq/repository/iris-3.1.0/archive.tar.gz>
 
 ## Compiling the exercises
 

_CoqProject

+-Q exercises exercises
+-Q solutions solutions
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+exercises/ex_01_swap.v
+exercises/ex_02_sumlist.v
+exercises/ex_03_spinlock.v
+exercises/ex_04_parallel_add.v
+exercises/ex_05_parallel_add_mul.v
+solutions/ex_01_swap.v
+solutions/ex_02_sumlist.v
+solutions/ex_03_spinlock.v
+solutions/ex_04_parallel_add.v
+solutions/ex_05_parallel_add_mul.v

exercises/Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
-all: Makefile.coq
-	+@make -f Makefile.coq all
-.PHONY: all
-
-clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find ./ \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
-	rm -f Makefile.coq
-.PHONY: clean
-
-Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject -o Makefile.coq
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-
-# Phony wildcard targets
-phony: ;
-.PHONY: phony

exercises/_CoqProject

--Q . tutorial
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-ex_01_swap.v
-ex_02_sumlist.v
-ex_03_spinlock.v
-ex_04_parallel_add.v
-ex_05_parallel_add_mul.v

exercises/ex_04_parallel_add.v

@@ -6,7 +6,7 @@ threads increase a reference that's initially zero by two, the result is four.
 From iris.algebra Require Import auth frac_auth.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import lib.par proofmode notation.
-From tutorial Require Import ex_03_spinlock.
+From exercises Require Import ex_03_spinlock.
 
 (** The program as a heap-lang expression. We use the heap-lang [par] module for
 parallel composition. *)

exercises/ex_05_parallel_add_mul.v

@@ -11,7 +11,7 @@ Contrary to the earlier exercises, this exercise is nearly entirely open.
 From iris.algebra Require Import auth frac_auth.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import proofmode notation lib.par.
-From tutorial Require Import ex_03_spinlock.
+From exercises Require Import ex_03_spinlock.
 
 Definition parallel_add_mul : expr :=
   let: "r" := ref #0 in

opam

+opam-version: "1.2"
+name: "coq-iris-tutorial-popl18"
+maintainer: "The Iris Organization"
+authors: "The Iris Organization"
+homepage: "https://gitlab.mpi-sws.org/iris/tutorial-popl18"
+bug-reports: "https://gitlab.mpi-sws.org/iris/tutorial-popl18/issues"
+dev-repo: "https://gitlab.mpi-sws.org/iris/tutorial-popl18.git"
+build: [make "-j%{jobs}%"]
+install: [] # This repo does not install
+remove: []
+depends: [
+  "coq-iris" { (= "3.1.0") }
+]

solutions/Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
-all: Makefile.coq
-	+@make -f Makefile.coq all
-.PHONY: all
-
-clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find ./ \( -name "*.v.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
-	rm -f Makefile.coq
-.PHONY: clean
-
-Makefile.coq: _CoqProject Makefile
-	coq_makefile -f _CoqProject -o Makefile.coq
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-
-# Phony wildcard targets
-phony: ;
-.PHONY: phony

solutions/_CoqProject

--Q . tutorial
--arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-ex_01_swap.v
-ex_02_sumlist.v
-ex_03_spinlock.v
-ex_04_parallel_add.v
-ex_05_parallel_add_mul.v

solutions/ex_04_parallel_add.v

@@ -6,7 +6,7 @@ threads increase a reference that's initially zero by two, the result is four.
 From iris.algebra Require Import auth frac_auth.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import lib.par proofmode notation.
-From tutorial Require Import ex_03_spinlock.
+From solutions Require Import ex_03_spinlock.
 
 (** The program as a heap-lang expression. We use the heap-lang [par] module for
 parallel composition. *)

solutions/ex_05_parallel_add_mul.v

@@ -11,7 +11,7 @@ Contrary to the earlier exercises, this exercise is nearly entirely open.
 From iris.algebra Require Import auth frac_auth.
 From iris.base_logic.lib Require Import invariants.
 From iris.heap_lang Require Import proofmode notation lib.par.
-From tutorial Require Import ex_03_spinlock.
+From solutions Require Import ex_03_spinlock.
 
 Definition parallel_add_mul : expr :=
   let: "r" := ref #0 in