Dockerfile and ci

.travis.yml

+os: linux
+dist: bionic
+language: shell
+
+notifications:
+  email:
+    - gregersen@cs.au.dk
+
+branches:
+  only:
+    - master
+    - /^ci\//
+    # for version tags of the form v0.1 or v0.1.1
+    - /^v\d+\.\d+(\.\d+)?$/
+
+services:
+  - docker
+
+env:
+  jobs:
+  - COQ_IMAGE="coqorg/coq:8.12"
+
+script:
+- echo -e "${ANSI_YELLOW}Building Aneris...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
+- docker build --build-arg=coq_image="${COQ_IMAGE}" --pull -t aneris .
+- echo -en 'travis_fold:end:script\\r'

Dockerfile

+ARG coq_image="coqorg/coq:dev"
+FROM ${coq_image}
+
+LABEL maintainer="gregersen@cs.au.dk"
+
+RUN eval $(opam env --switch=${COMPILER_EDGE} --set-switch) \
+    opam repository add --all-switches --set-default iris-dev https://gitlab.mpi-sws.org/iris/opam.git \
+    && opam update -y -u \
+    && opam config list && opam repo list && opam list \
+    && opam clean -a -c -s --logs
+
+COPY --chown=coq:coq . /coq
+WORKDIR /coq
+ENV OPAMYES true
+
+RUN git submodule update --recursive \
+    && make build-dep
+RUN make clean \
+    && make -j ${NJOBS}

Makefile

@@ -14,10 +14,10 @@ Makefile.coq: _CoqProject
 	+make -f Makefile.coq $@
 
 # Install build-dependencies
-build-dep/opam: opam Makefile
+build-dep/opam: aneris.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
+	@sed <aneris.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
@@ -38,6 +38,6 @@ build-dep: build-dep/opam phony
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
 _CoqProject: ;
-opam: ;
+aneris.opam: ;
 
 .PHONY: all clean phony

aneris.opam

 opam-version: "2.0"
+name: "coq-aneris"
 synopsis: "Coq development of the Aneris program logic"
 maintainer: "Simon Gregersen <gregersen@cs.au.dk>"
 authors: "The Aneris Team"
@@ -9,7 +10,7 @@ bug-reports: "https://github.com/logsem/aneris/issues"
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (= "8.12.0") | (= "dev") }
+  "coq" { (>= "8.11.0" & < "8.12~") | (= "dev") }
   "coq-iris" { (= "dev.2020-09-03.2.26739725") | (= "dev") }
   "coq-stdpp" { (= "dev.2020-09-02.0.897b954e") | (= "dev") }
   "coq-iris-string-ident" { (= "dev")  }