Local OPAM packages for Travis (#4)

.travis-ci.sh

@@ -7,12 +7,15 @@ opam repo add coq-released https://coq.inria.fr/opam/released
 opam repo add distributedcomponents-dev http://opam-dev.distributedcomponents.net
 
 opam pin add coq $COQ_VERSION --yes --verbose
-opam pin add coq-mathcomp-ssreflect $SSREFLECT_VERSION --yes --verbose
-
-opam install verdi StructTact verdi-runtime ocamlbuild --yes --verbose
 
 case $MODE in
+  lockserv)
+    opam pin add lockserv . --yes --verbose
+    ;;
+  lockserv-seqnum)
+    opam pin add lockserv-seqnum . --yes --verbose
+    ;;
   *)
-    ./build.sh
+    opam pin add verdi-lockserv . --yes --verbose
     ;;
 esac

.travis.yml

@@ -9,8 +9,10 @@ addons:
       - aspcud
 env:
   matrix:
-    - MODE=build COQ_VERSION=8.6 SSREFLECT_VERSION=1.6.1
-    - MODE=build COQ_VERSION=8.5.3 SSREFLECT_VERSION=1.6
+    - MODE=build COQ_VERSION=8.5.3
+    - MODE=build COQ_VERSION=8.6
+    - MODE=lockserv COQ_VERSION=8.6 OPAMBUILDTEST=1
+    - MODE=lockserv-seqnum COQ_VERSION=8.6
 script: bash -ex .travis-ci.sh
 sudo: false
 notifications:

Makefile

@@ -18,7 +18,6 @@ endif
 
 default: Makefile.coq
 	$(MAKE) -f Makefile.coq
-	+$(MAKE) -C extraction/lockserv
 
 LOCKSERV_MLFILES = extraction/lockserv/ocaml/LockServ.ml extraction/lockserv/ocaml/LockServ.mli
 LOCKSERV_SEQNUM_MLFILES = extraction/lockserv-seqnum/ocaml/LockServSeqNum.ml extraction/lockserv-seqnum/ocaml/LockServSeqNum.mli
@@ -40,6 +39,9 @@ $(LOCKSERV_MLFILES) $(LOCKSERV_SEQNUM_MLFILES): Makefile.coq
 lockserv:
 	+$(MAKE) -C extraction/lockserv
 
+lockserv-test:
+	+$(MAKE) -C extraction/lockserv test
+
 lockserv-seqnum:
 	+$(MAKE) -C extraction/lockserv-seqnum
 
@@ -57,4 +59,4 @@ lint:
 distclean: clean
 	rm -f _CoqProject
 
-.PHONY: default clean lint $(LOCKSERV_MLFILES) $(LOCKSERV_SEQNUM_MLFILES) lockserv lockserv-seqnum
+.PHONY: default clean lint $(LOCKSERV_MLFILES) $(LOCKSERV_SEQNUM_MLFILES) lockserv lockserv-test lockserv-seqnum

README.md

@@ -44,7 +44,9 @@ Then, run `./configure` in the root directory.  This will check for the appropri
 
 By default, the script assumes that `Verdi` and `StructTact` are installed in Coq's `user-contrib` directory, but this can be overridden by setting the `Verdi_PATH` and `StructTact_PATH` environment variables.
 
-Finally, run `make` in the root directory. This will compile the lock server definitions, check the proofs of mutual exclusion, and finally build an OCaml program from the extracted code called `LockServMain` in the `extraction/lockserv` directory.
+Finally, run `make` in the root directory. This will compile the lock server definitions, check the proofs of mutual exclusion, and extract OCaml event handler code.
+
+To build an OCaml program from the extracted code called `LockServMain.native` in the `extraction/lockserv` directory, run `make lockserv` in the root directory.
 
 Running LockServ on a Cluster
 -----------------------------

lockserv-seqnum.install

@@ -0,0 +1 @@
+bin: ["extraction/lockserv-seqnum/_build/ocaml/LockServSeqNumMain.native" {"lockserv-seqnum"}]

lockserv-seqnum.opam

@@ -0,0 +1,32 @@
+opam-version: "1.2"
+version: "dev"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/DistributedComponents/verdi-lockserv"
+dev-repo: "https://github.com/DistributedComponents/verdi-lockserv.git"
+bug-reports: "https://github.com/DistributedComponents/verdi-lockserv/issues"
+license: "BSD"
+
+build: [
+  [ "./configure" ]
+  [ make "-j%{jobs}%" "lockserv-seqnum" ]
+]
+available: [ ocaml-version >= "4.02.3" ]
+depends: [
+  "coq" {((>= "8.5" & < "8.6~") | (>= "8.6" & < "8.7~"))}
+  "verdi" {= "dev"}
+  "StructTact" {= "dev"}
+  "verdi-runtime" {= "dev"}
+  "ocamlfind" {build}
+  "ocamlbuild" {build}
+]
+
+authors: [
+  "James Wilcox <>"
+  "Doug Woos <>"
+  "Pavel Panchekha <>"
+  "Zachary Tatlock <>"
+  "Steve Anton <>"
+  "Karl Palmskog <>"
+  "Ryan Doenges <>"
+]

lockserv.install

@@ -0,0 +1 @@
+bin: ["extraction/lockserv/_build/ocaml/LockServMain.native" {"lockserv"}]

lockserv.opam

@@ -0,0 +1,34 @@
+opam-version: "1.2"
+version: "dev"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/DistributedComponents/verdi-lockserv"
+dev-repo: "https://github.com/DistributedComponents/verdi-lockserv.git"
+bug-reports: "https://github.com/DistributedComponents/verdi-lockserv/issues"
+license: "BSD"
+
+build: [
+  [ "./configure" ]
+  [ make "-j%{jobs}%" "lockserv" ]
+]
+build-test: [make "lockserv-test"]
+available: [ ocaml-version >= "4.02.3" ]
+depends: [
+  "coq" {((>= "8.5" & < "8.6~") | (>= "8.6" & < "8.7~"))}
+  "verdi" {= "dev"}
+  "StructTact" {= "dev"}
+  "verdi-runtime" {= "dev"}
+  "ocamlfind" {build}
+  "ocamlbuild" {build}
+  "ounit" {test & >= "2.0.0"}
+]
+
+authors: [
+  "James Wilcox <>"
+  "Doug Woos <>"
+  "Pavel Panchekha <>"
+  "Zachary Tatlock <>"
+  "Steve Anton <>"
+  "Karl Palmskog <>"
+  "Ryan Doenges <>"
+]

verdi-lockserv.opam

@@ -0,0 +1,28 @@
+opam-version: "1.2"
+version: "dev"
+maintainer: "palmskog@gmail.com"
+
+homepage: "https://github.com/DistributedComponents/verdi-lockserv"
+dev-repo: "https://github.com/DistributedComponents/verdi-lockserv.git"
+bug-reports: "https://github.com/DistributedComponents/verdi-lockserv/issues"
+license: "BSD"
+
+build: [
+  [ "./configure" ]
+  [ make "-j%{jobs}%" ]
+]
+depends: [
+  "coq" {((>= "8.5" & < "8.6~") | (>= "8.6" & < "8.7~"))}
+  "verdi" {= "dev"}
+  "StructTact" {= "dev"}
+]
+
+authors: [
+  "James Wilcox <>"
+  "Doug Woos <>"
+  "Pavel Panchekha <>"
+  "Zachary Tatlock <>"
+  "Steve Anton <>"
+  "Karl Palmskog <>"
+  "Ryan Doenges <>"
+]