update opam package definitions and README.md for 8.12 and MC 1.11

Author: palmskog

.travis.yml

@@ -44,6 +44,11 @@ matrix:
     - PACKAGE=coq-disel
     - NJOBS=2
     <<: *OPAM
+  - env:
+    - COQ_IMAGE=coqorg/coq:8.12
+    - PACKAGE=coq-disel
+    - NJOBS=2
+    <<: *OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
     - PACKAGE=coq-disel

README.md

@@ -1,4 +1,4 @@
-# Disel - Distributed Separation Logic
+# Disel: Distributed Separation Logic
 
 Implementation and case studies of Disel, a separation-style logic for
 compositional verification of distributed systems.
@@ -11,8 +11,8 @@ by Ilya Sergey, James R. Wilcox, and Zachary Tatlock, in the POPL 2018 proceedin
 ### Requirements
 
 * [Coq 8.7 or later](https://coq.inria.fr)
-* [Mathematical Components 1.6.2 or later](http://math-comp.github.io/math-comp/) (`ssreflect` suffices)
-* [FCSL PCM library 1.0.0 or later](https://github.com/imdea-software/fcsl-pcm)
+* [Mathematical Components 1.9.0 or later](http://math-comp.github.io/math-comp/) (`ssreflect` suffices)
+* [FCSL PCM library 1.1.0 or later](https://github.com/imdea-software/fcsl-pcm)
 * [OCaml 4.05.0 or later](https://ocaml.org) (to compile and run the extracted applications)
 
 ### Building Manually

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.12~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.13~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.9.0" & < "1.12~") | (= "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.12~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.13~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.9.0" & < "1.12~") | (= "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.12~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.13~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.9.0" & < "1.12~") | (= "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.12~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.6.2" & < "1.11~") | (= "dev")}
+  "coq" {(>= "8.7" & < "8.13~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "1.9.0" & < "1.12~") | (= "dev")}
   "coq-fcsl-pcm"
 ]