update opam and Travis for 8.10

.travis.yml

@@ -13,7 +13,7 @@ opam: &OPAM
       set -ex  # -e = exit on failure; -x = trace for debug
       opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
       opam update -y
-      opam pin add ${CONTRIB_NAME} . -y --no-action
+      opam pin add ${CONTRIB_NAME} . -y -n -k path
       opam install ${CONTRIB_NAME} -y -j ${NJOBS} --deps-only
       opam config list
       opam repo list
@@ -40,6 +40,11 @@ matrix:
     - CONTRIB_NAME=coq-cheerios
     - NJOBS=2
     <<: *OPAM
+  - env:
+    - COQ_IMAGE=coqorg/coq:8.10
+    - CONTRIB_NAME=coq-cheerios
+    - NJOBS=2
+    <<: *OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
     - CONTRIB_NAME=coq-cheerios

Makefile

@@ -1,13 +1,6 @@
-# sets COQVERSION
-include Makefile.detect-coq-version
-
 # sets MLTREE, etc.
 include Makefile.ml-files
 
-ifeq (,$(filter $(COQVERSION),8.6 8.7 8.8 8.9 8.10 dev))
-$(error "Cheerios is only compatible with Coq version 8.6.1 or later")
-endif
-
 COQPROJECT_EXISTS := $(wildcard _CoqProject)
 
 ifeq "$(COQPROJECT_EXISTS)" ""

README.md

@@ -27,7 +27,7 @@ Runtime:
 Building
 --------
 
-The easiest way to install Cheerios is via [OPAM](http://opam.ocaml.org/doc/Install.html):
+The easiest way to build and install Cheerios is via [OPAM](http://opam.ocaml.org/doc/Install.html):
 ```
 opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 opam install coq-cheerios

cheerios-runtime.opam

@@ -7,17 +7,21 @@ dev-repo: "git+https://github.com/uwplse/cheerios.git"
 bug-reports: "https://github.com/uwplse/cheerios/issues"
 license: "BSD-2-Clause"
 synopsis: "Cheerios serialization framework runtime library"
+description: """
+OCaml support library for the Coq library Cheerios,
+enabling running extracted verified serialization code.
+"""
 
-build: [ make "-j%{jobs}%" "-C" "runtime" ]
+build: [make "-j%{jobs}%" "-C" "runtime"]
 depends: [
   "ocaml" {>= "4.02.3"}
   "ocamlbuild" {build}
 ]
 
 authors: [
-  "Keith Simmons"
-  "Doug Woos"
-  "James R. Wilcox"
   "Justin Adsuara"
   "Karl Palmskog"
+  "Keith Simmons"
+  "James R. Wilcox"
+  "Doug Woos"
 ]

coq-cheerios.opam

@@ -6,21 +6,21 @@ homepage: "https://github.com/uwplse/cheerios"
 dev-repo: "git+https://github.com/uwplse/cheerios.git"
 bug-reports: "https://github.com/uwplse/cheerios/issues"
 license: "BSD-2-Clause"
-synopsis: "Coq library for serialization"
+synopsis: "Coq library for verified serialization"
 description: """
-Cheerios is a formally verified serialization library for Coq,
-which defines a typeclass for serializable types and defines instances
-for many built-in types.
+A formally verified serialization library for Coq
+which defines a typeclass for serializable types and instances
+for many standard library types.
 """
 
 build: [
-  [ "./configure" ]
-  [ make "-j%{jobs}%" ]
+  ["./configure"]
+  [make "-j%{jobs}%"]
 ]
-install: [ make "install" ]
+install: [make "install"]
 depends: [
   "ocaml"
-  "coq" {(>= "8.6.1" & < "8.10~") | (= "dev")}
+  "coq" {(>= "8.6.1" & < "8.11~") | (= "dev")}
   "coq-struct-tact" {= "dev"}
 ]
 
@@ -30,9 +30,9 @@ tags: [
   "logpath:Cheerios"
 ]
 authors: [
-  "Keith Simmons"
-  "Doug Woos"
-  "James R. Wilcox"
   "Justin Adsuara"
   "Karl Palmskog"
+  "Keith Simmons"
+  "James R. Wilcox"
+  "Doug Woos"
 ]