adjust opam and Travis for Coq 8.11

Author: palmskog

.gitignore

@@ -25,6 +25,9 @@ Thumbs.db
 *.thr_debug_o
 *.o
 *.vo
+*.vio
+*.vos
+*.vok
 *.a
 *.o.cmd
 *.depend*
@@ -84,4 +87,5 @@ _build
 *.d.byte
 *.native
 Makefile.coq.conf
+.Makefile.coq.d
 .coqdeps.d

.travis.yml

@@ -5,27 +5,27 @@ opam: &OPAM
   install: |
     # Prepare the COQ container
     docker pull ${COQ_IMAGE}
-    docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${CONTRIB_NAME} -w /home/coq/${CONTRIB_NAME} ${COQ_IMAGE}
+    docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/${PACKAGE} -w /home/coq/${PACKAGE} ${COQ_IMAGE}
     docker exec COQ /bin/bash --login -c "
       # This bash script is double-quoted to interpolate Travis CI env vars:
       echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex  # -e = exit on failure; -x = trace for debug
       opam update -y
-      opam pin add ${CONTRIB_NAME} . -y -n -k path
-      opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only
+      opam pin add ${PACKAGE} . -y -n -k path
+      opam install ${PACKAGE} -y -j ${NJOBS} --deps-only
       opam config list
       opam repo list
       opam list
       "
   script:
-  - echo -e "${ANSI_YELLOW}Building ${CONTRIB_NAME}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
+  - echo -e "${ANSI_YELLOW}Building ${PACKAGE}...${ANSI_RESET}" && echo -en 'travis_fold:start:script\\r'
   - |
     docker exec COQ /bin/bash --login -c "
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex
-      sudo chown -R coq:coq /home/coq/${CONTRIB_NAME}
-      opam install ${CONTRIB_NAME} -v -y -j ${NJOBS}
+      sudo chown -R coq:coq /home/coq/${PACKAGE}
+      opam install ${PACKAGE} -v -y -j ${NJOBS}
       "
   - docker stop COQ  # optional
   - echo -en 'travis_fold:end:script\\r'
@@ -35,17 +35,17 @@ matrix:
 
   # Test supported versions of Coq via OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:8.9
-    - CONTRIB_NAME=coq-disel
+    - COQ_IMAGE=coqorg/coq:8.10
+    - PACKAGE=coq-disel
     - NJOBS=2
     <<: *OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:8.10
-    - CONTRIB_NAME=coq-disel
+    - COQ_IMAGE=coqorg/coq:8.11
+    - PACKAGE=coq-disel
     - NJOBS=2
     <<: *OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
-    - CONTRIB_NAME=coq-disel
+    - PACKAGE=coq-disel
     - NJOBS=2
     <<: *OPAM

coq-disel-calculator.opam

@@ -10,8 +10,8 @@ synopsis: "Calculator implemented in Disel, a separation-style logic for composi
 build: [make "-j%{jobs}%" "calculator"]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.10~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
   "coq-fcsl-pcm"
   "ocamlbuild" {build}
 ]

coq-disel-examples.opam

@@ -11,8 +11,8 @@ build: [make "-j%{jobs}%" "-C" "Examples"]
 install: [make "-C" "Examples" "install"]
 depends: [
   "ocaml"
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.10~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
   "coq-fcsl-pcm"
   "coq-disel" {= version}
 ]

coq-disel-tpc.opam

@@ -10,8 +10,8 @@ synopsis: "Two-phase commit implemented in Disel, a separation-style logic for c
 build: [make "-j%{jobs}%" "tpc"]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.10~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
   "coq-fcsl-pcm"
   "ocamlbuild" {build}
 ]

coq-disel.opam

@@ -20,8 +20,8 @@ build: [make "-j%{jobs}%" "-C" "Core"]
 install: [make "-C" "Core" "install"]
 depends: [
   "ocaml"
-  "coq" {(>= "8.7" & < "8.11~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.10~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.12~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
   "coq-fcsl-pcm"
 ]