Package JSCert for opam. Update flocq to 2.5.2. Fixes Travis CI builds.

Fixes: resource-reasoning/jscert_dev#41

.travis.yml

@@ -4,34 +4,30 @@ env:
   global:
     - OPAMYES=true
   matrix:
-    - PPA=ocaml41 OPAMROOT=~/.opam41
-    - PPA=ocaml42 OPAMROOT=~/.opam42
-    - PPA=ocaml42 OPAMROOT=~/.opam42 MAKETARGET=all
-    - PPA=ocaml42 OPAMROOT=~/.opam42 MAKETARGET=proof
+    - MAKETARGET=all
+    - MAKETARGET=proof
 
 # Caching is only enabled for private builds
 cache:
-  apt: true
   directories:
-    - ~/.opam41
-    - ~/.opam42
+    - ~/.opam
 
 before_install:
-  # Use an ubuntu ppa coq build to speed things up
-  - sudo add-apt-repository -y ppa:grand-edgemaster/coq-$PPA
-  - sudo add-apt-repository -y ppa:avsm/$PPA+opam12
+  - sudo add-apt-repository -y ppa:avsm/ocaml42+opam12
   - sudo apt-get update
-  - make init
+  - sudo apt-get install -y ocaml-compiler-libs ocaml-interp ocaml-base-nox ocaml-base ocaml ocaml-nox ocaml-native-compilers camlp4 camlp4-extra opam
 
 install:
-  - sudo apt-get install -y coq ocaml-compiler-libs ocaml-interp ocaml-base-nox ocaml-base ocaml ocaml-nox ocaml-native-compilers camlp4 camlp4-extra opam
   - opam init -a
-  - opam update -u
+  - opam repo add coq-released https://coq.inria.fr/opam/released || true
   - eval `opam config env`
-  - make install_optional_depend
+  - opam update
+  - sed -ie "/coq-jscert/d" ~/.opam/`opam switch show`/reinstall || true
+  - opam upgrade
+  - make init
 
+# Always keep coq-jscert installed so correct versions of dependencies are installed
+# on upgrade step above, even if this duplicates compilations.
 script:
-  - make $MAKETARGET
-
-notifications:
-  webhooks:  https://www-rw.doc.ic.ac.uk/ci/irc-webhook/travis-ci
+  - opam reinstall -yv coq-jscert
+  - travis_wait 30 make $MAKETARGET

Makefile

@@ -13,8 +13,6 @@
 
 COQBIN=
 TLC=lib/tlc/src
-FLOCQ=lib/flocq
-FLOCQ_INC=-R $(FLOCQ)/src Flocq
 
 # Define FAST to be non empty for compiling Coq proofs faster
 FAST=
@@ -26,10 +24,6 @@ LAMBDAS5=~/Documents/data/LambdaS5/tests/s5
 SPIDERMONKEY=~/Mozilla/Central/Central/js/src/build_release/js
 NODEJS=/usr/bin/nodejs
 
-# Alternative definition for FLOCQ_INC:
-# FLOCQ_FOLDERS=$(addprefix $(FLOCQ)/src/,Core Calc Appli Prop)
-# FLOCQ_INC=$(addprefix -I ,$(FLOCQ_FOLDERS))
-
 # Edit settings.sh to modify the default paths mentioned above
 -include settings.sh
 
@@ -39,13 +33,10 @@ NODEJS=/usr/bin/nodejs
 TLC_SRC=$(wildcard $(TLC)/*.v)
 TLC_VO=$(TLC_SRC:.v=.vo)
 
-FLOCQ_SRC=$(wildcard $(FLOCQ)/src/*/*.v)
-FLOCQ_VO=$(FLOCQ_SRC:.v=.vo)
-
 
 #######################################################
 
-COQINCLUDES=-I coq -I $(TLC) $(FLOCQ_INC)
+COQINCLUDES=-I coq -I $(TLC)
 COQC=$(COQBIN)coqc
 COQDEP=$(COQBIN)coqdep
 COQFLAGS=-dont-load-proofs
@@ -115,7 +106,7 @@ report:
 tags: $(JS_SRC)
 	./gentags.sh
 
-.PHONY: all default debug report init tlc flocq lib \
+.PHONY: all default debug report init tlc lib \
         local nofast
 
 #######################################################
@@ -135,19 +126,14 @@ install_optional_depend: install_depend
 init:
 	tools/git-hooks/install.sh .
 	git submodule update --init
-	opam pin -y add JS_Parser "https://github.com/resource-reasoning/JS_Parser.git#v0.1.0"
-	opam install JS_Parser
-	mkdir -p lib/flocq
-	tar -xzf lib/flocq-2.1.0.tar.gz -C lib/flocq --strip-components 1
-# alternative: pull git from svn
-#	git clone https://gforge.inria.fr/git/flocq/flocq.git flocq
+	opam pin -yn add JS_Parser "https://github.com/resource-reasoning/JS_Parser.git#v0.1.0"
+	opam pin -yn add coq-jscert .
+	opam install -yv --deps-only coq-jscert
 
-lib: tlc flocq
+lib: tlc
 
 tlc: $(TLC_VO)
 
-flocq: $(FLOCQ_VO)
-
 #######################################################
 # Coq Compilation Implicit Rules
 %.v.d: %.v
@@ -304,16 +290,16 @@ clean: clean_interp
 	-rm -f coq/*.{vo,glob,d}
 
 clean_all: clean
+	-rm -rf lib/flocq
 	find . -iname "*.vo" -exec rm {} \;
 	find . -iname "*.glob" -exec rm {} \;
 	find . -iname "*.d" -exec rm {} \;
 
 
 #######################################################
-# LOCAL: copy all flocq and tlc .vo files to the head folder
+# LOCAL: copy all tlc .vo files to the head folder
 
 local:
-	@$(foreach file, $(FLOCQ_VO), cp $(file) $(notdir $(file));)
 	@$(foreach file, $(TLC_VO), cp $(file) $(notdir $(file));)
 
 #######################################################
@@ -323,5 +309,4 @@ local:
 ifeq ($(filter init clean% install%,$(MAKECMDGOALS)),)
 -include $(JS_SRC:.v=.v.d)
 -include $(TLC_SRC:.v=.v.d)
--include $(FLOCQ_SRC:.v=.v.d)
 endif

coq-jscert.install

@@ -0,0 +1,3 @@
+bin: [
+  "interp/run_js.native" { "run_js" }
+]

opam

@@ -0,0 +1,33 @@
+opam-version: "1.2"
+name: "coq-jscert"
+version: "~unknown"
+maintainer: "Thomas Wood <thomas.wood09@imperial.ac.uk>"
+authors: [
+  "Martin Bodin <martin.bodin@inria.fr>"
+  "Arthur Charguéraud <arthur@chargueraud.org>"
+  "Daniele Filaretti"
+  "Sergio Maffeis <maffeis@doc.ic.ac.uk>"
+  "Petar Maksimovic <p.maksimovic@imperial.ac.uk>"
+  "Daiva Naudziuniene <d.naudziuniene11@imperial.ac.uk>"
+  "Alan Schmitt <alan.schmitt@inria.fr>"
+  "Gareth Smith"
+  "Thomas Wood <thomas.wood09@imperial.ac.uk>"
+]
+
+homepage: "http://www.jscert.org/"
+bug-reports: "https://github.com/jscert/jscert/issues"
+license: "BSD"
+dev-repo: "https://github.com/jscert/jscert.git"
+build: [
+  [make]
+]
+available: [ ocaml-version >= "4.02" & ocaml-version < "4.04~" ]
+depends: [
+  "ocamlfind" {build}
+  "coq" { >= "8.4" & < "8.5~" }
+  (* "coq-tlc" *)
+  "coq-flocq" { >= "2.1" & < "2.6~" }
+  "lwt"
+  "bisect"
+  "JS_Parser"
+]