chore: Add build dependencies

Makefile

@@ -17,13 +17,39 @@ clean: Makefile.coq
 	+@$(MAKE) -f Makefile.coq clean
 	@# Make sure not to enter the `_opam` folder.
 	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache
+	rm -f Makefile.coq .lia.cache builddep/*
 .PHONY: clean
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
 	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
+# Install build-dependencies
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install 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 "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) -y $(BUILDDEPFILES)
+.PHONY: builddep
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
 # Some files that do *not* need to be forwarded to Makefile.coq.
 # ("::" lets Makefile.local overwrite this.)
 Makefile Makefile.local _CoqProject $(OPAMFILES):: ;

README.md

 ## Installation
 
+You first need to make sure [`opam` is installed on your system](https://opam.ocaml.org/doc/Install.html).
+After that you can install the dependencies as follows:
 ```
-opam switch create bachelor-thesis ocaml-base-compiler.4.14.0
+opam switch create iris-barriers ocaml-base-compiler.4.14.0
 eval $(opam env)
-opam switch link bachelor-thesis .
+opam switch link iris-barriers .
 opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-opam install coq-iris coq-iris-heap-lang
-```
\ No newline at end of file
+make builddep
+```
+To build the project files, run `make -jN` with `N` the number of used CPU cores.
\ No newline at end of file

barriers.opam

+opam-version: "2.0"
+name: "coq-iris-barriers"
+license: "BSD-3-Clause"
+maintainer: "Simcha van Collem"
+authors: "Robbert Krebbers, Simcha van Collem"
+synopsis: "Bachelor thesis of Simcha van Collem, verifying different barriers in Iris"
+homepage: "https://gitlab.science.ru.nl/svcollem/bachelor-thesis/"
+bug-reports: "https://gitlab.science.ru.nl/svcollem/bachelor-thesis/issues"
+version: "dev"
+
+depends: [
+  "coq" { (>= "8.15" & < "8.16~") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-10-31.0.1e9db5bd") | (= "dev") }
+]
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]