diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..5c27129
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,20 @@
+*.vo
+*.vos
+*.vok
+*.vio
+*.glob
+*.cache
+*.aux
+\#*\#
+.\#*
+*~
+*.bak
+Makefile.coq
+Makefile.coq.conf
+.Makefile.coq.d
+.coq-native/
+builddep
+_opam
+tags
+_build
+public
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..7ebc68f
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,55 @@
+# Default target
+all: Makefile.coq
+	+@$(MAKE) -f Makefile.coq all
+.PHONY: all
+
+# Permit local customization
+-include Makefile.local
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
+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 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):: ;
diff --git a/semantics.opam b/semantics.opam
new file mode 100644
index 0000000..b97fb93
--- /dev/null
+++ b/semantics.opam
@@ -0,0 +1,19 @@
+opam-version: "2.0"
+name: "coq-semantics-course"
+license: "BSD-3-Clause"
+maintainer: "Simon Spies, Lennard Gäher"
+authors: "Derek Dreyer, Simon Spies, Lennard Gäher"
+synopsis: "Best course this side of the milky way"
+homepage: "https://plv.mpi-sws.org/semantics-course/"
+bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
+version: "dev"
+
+depends: [
+  "coq" { (>= "8.18" & < "8.19~") | (= "dev") }
+  "coq-iris-heap-lang" { (= "4.1.0") | (= "dev") }
+  "coq-equations" { (= "1.3+8.18") }
+  "coq-autosubst" { (= "1.8") | (= "dev")  }
+]
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]