From 08e64224e999968845134857574b0ef5e73a4c32 Mon Sep 17 00:00:00 2001
From: Benjamin Peters <bpeters@mpi-sws.org>
Date: Thu, 19 Oct 2023 12:45:04 +0200
Subject: [PATCH] added makefile

---
 .gitignore     | 20 ++++++++++++++++++
 Makefile       | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++
 semantics.opam | 19 +++++++++++++++++
 3 files changed, 94 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Makefile
 create mode 100644 semantics.opam

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"]