Merge branch 'ci/ralf/ci' into 'master'

install CI and update build system

See merge request !1

.gitignore

@@ -13,3 +13,5 @@
 *.bak
 .coq-native/
 Makefile.coq
+Makefile.coq.conf
+build-dep/

.gitlab-ci.yml

+image: ralfjung/opam-ci:latest
+
+stages:
+  - build
+
+variables:
+  CPU_CORES: "10"
+  GIT_SUBMODULE_STRATEGY: "recursive"
+
+.template: &template
+  stage: build
+  tags:
+  - fp
+  script:
+  - ci/buildjob
+  cache:
+    key: "$CI_JOB_NAME"
+    paths:
+    - opamroot/
+  only:
+  - master
+  - /^ci/
+  except:
+  - triggers
+  - schedules
+
+## Build jobs
+
+build-coq.8.7.2:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.7.2   coq-mathcomp-ssreflect version 1.6.4"
+
+build-coq.8.6.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.4"

.gitmodules

+[submodule "ci"]
+	path = ci
+	url = https://gitlab.mpi-sws.org/FP/iris-ci.git

Makefile

-#####
-## This has been adapted from the Makefile of iris-coq
-
 # 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
+	find theories \( -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
 
+# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
+# filename, so we do some file gymnastics.
 Makefile.coq: _CoqProject Makefile awk.Makefile
-	coq_makefile -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
+
+# Install build-dependencies
+build-dep/opam: opam Makefile
+	# Creating the 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.
+	@# Upgrading is needed in case the pin already exists, but the builddep package changed.
+	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
+	  echo "# Pinning build-dep package." && \
+	  opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	  echo "# Updating build-dep package." && \
+	  opam upgrade "$$BUILD_DEP_PACKAGE"
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
 _CoqProject: ;
 awk.Makefile: ;
+opam: ;
 
-# Phony targets (i.e. targets that should be run no matter the timestamps of the involved files)
+# Phony wildcard targets
 phony: ;
-.PHONY: all clean phony
+.PHONY: phony

README.md

@@ -2,8 +2,8 @@
 
 This version is known to compile with:
 
- - Coq 8.6.1
- - Ssreflect 1.6
+ - Coq 8.6.1 / 8.7.2
+ - Ssreflect 1.6.4
  - Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
  - std++ version [32570aa6e0d04633047d9fddb3cf8da1748d9695](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/32570aa6e0d04633047d9fddb3cf8da1748d9695)
  - Iris version [7e33a806f2cd8da0409f1e5a13126317afd23e3d](https://gitlab.mpi-sws.org/FP/iris-coq/tree/7e33a806f2cd8da0409f1e5a13126317afd23e3d)

awk.Makefile

+# awk program that patches the Makefile generated by Coq.
+
+# Detect the name this project will be installed under.
+/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
+# Wow, POSIX awk is really broken.  I mean, isn't it supposed to be a text processing language?
+# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
+# we can just split the string at '/' here.
+	split($0, PIECES, /\//);
+	PROJECT=PIECES[2];
+}
+
+# Patch the uninstall target to work properly, and to also uninstall stale files.
+# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
+# This (and the section above) can be removed once we no longer support Coq 8.6.
+/^uninstall: / {
+	print "uninstall:";
+	print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
+	getline;
+	next
+}
+
+# This forwards all unchanged lines
+1

ci @ e5889b23

+Subproject commit e5889b234143d4f3c2b6d4a90e46b39802c00388

opam

+opam-version: "1.2"
+name: "coq-iris-logrel"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "Dan Frumin, Robbert Krebbers"
+homepage: "http://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/dfrumin/logrel-conc/issues"
+dev-repo: "https://gitlab.mpi-sws.org/dfrumin/logrel-conc.git"
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_logrel"]
+depends: [
+  "coq-iris" { (= "dev.2018-04-09.0") | (= "dev") }
+  "coq-autosubst" { = "dev.coq86" }
+]