Merge pull request #4 from DistributedComponents/coq-8.7-opam

ilyasergey · web-flow · commit fe01c09dcacf · 2017-11-28T19:48:31.000Z
update OPAM-related definitions, makefile and Travis tasks for Coq 8.7
diff --git a/.travis-ci.sh b/.travis-ci.sh
@@ -4,8 +4,11 @@ opam init --yes --no-setup
 eval $(opam config env)
 
 opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
+opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 
-opam pin add coq $COQ_VERSION --yes --verbose
+opam pin add coq $COQ_VERSION --kind=version --yes --verbose
+opam pin add coq-mathcomp-ssreflect $SSREFLECT_VERSION --kind=version --yes --verbose
 
 opam pin add Heaps --yes --verbose
 opam pin add Core --yes --verbose
diff --git a/.travis.yml b/.travis.yml
@@ -9,8 +9,7 @@ addons:
       - aspcud
 env:
   matrix:
-    - COQ_VERSION=8.6.1
-    - COQ_VERSION=8.6
+    - COQ_VERSION=8.7.0 SSREFLECT_VERSION=1.6.4
 script: bash -ex .travis-ci.sh
 sudo: false
 notifications:
diff --git a/Core/Make b/Core/Make
@@ -1,21 +1,22 @@
-State.v
-Freshness.v
-Protocols.v
-EqTypeX.v
-DepMaps.v
-StatePredicates.v
-NewStatePredicates.v
-Worlds.v
-NetworkSem.v
-Rely.v
-Actions.v
-Injection.v
-InductiveInv.v
-Process.v
-Always.v
-HoareTriples.v
-InferenceRules.v
-While.v 
-DiSeLExtraction.v
+-Q . DiSeL.Core
+-arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
 
--R . DiSeL.Core
+./State.v
+./Freshness.v
+./Protocols.v
+./EqTypeX.v
+./DepMaps.v
+./StatePredicates.v
+./NewStatePredicates.v
+./Worlds.v
+./NetworkSem.v
+./Rely.v
+./Actions.v
+./Injection.v
+./InductiveInv.v
+./Process.v
+./Always.v
+./HoareTriples.v
+./InferenceRules.v
+./While.v 
+./DiSeLExtraction.v
diff --git a/Core/Makefile b/Core/Makefile
@@ -11,9 +11,9 @@ install: Makefile.coq
 clean:
 	if [ -f Makefile.coq ]; then \
 	  $(MAKE) -f Makefile.coq clean; fi
-	rm -f Makefile.coq
+	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: Make
-	coq_makefile -arg -w -arg -notation-overridden -f Make -o Makefile.coq
+	coq_makefile -f Make -o Makefile.coq
 
 .PHONY: default clean install
diff --git a/Core/opam b/Core/opam
@@ -1,20 +1,20 @@
 opam-version: "1.2"
-name: "coq-disel-core"
+name: "disel-core"
 version: "dev"
 maintainer: "palmskog@gmail.com"
 
 homepage: "https://github.com/DistributedComponents/disel"
 dev-repo: "https://github.com/DistributedComponents/disel.git"
 bug-reports: "https://github.com/DistributedComponents/disel/issues"
-license: "Proprietary"
+license: "BSD2"
 
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/DiSeL/Core'" ]
 depends: [
-  "coq" { ((>= "8.6" & < "8.7~") | (= "dev")) }
-  "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) }
-  "coq-disel-heaps" {= "dev"}
+  "coq" { ((>= "8.7" & < "8.8~") | (= "dev")) }
+  "coq-mathcomp-ssreflect" { ((>= "1.6.2" & < "1.7~") | (= "dev")) }
+  "disel-heaps" {= "dev"}
 ]
 
 tags: [
diff --git a/Examples/Make b/Examples/Make
@@ -1,4 +1,7 @@
-SeqLib.v
+-Q . DiSeL.Examples
+-arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
+
+./SeqLib.v
 Greeter/Greeter.v
 Querying/QueryProtocol.v
 Querying/QueryHooked.v
@@ -18,5 +21,3 @@ TwoPhaseCommit/TwoPhaseInductiveProof.v
 Querying/QueryPlusTPC.v
 LockResource/LockProtocol.v
 LockResource/ResourceProtocol.v
-
--R . DiSeL.Examples
diff --git a/Examples/Makefile b/Examples/Makefile
@@ -11,9 +11,9 @@ install: Makefile.coq
 clean:
 	if [ -f Makefile.coq ]; then \
 	  $(MAKE) -f Makefile.coq clean; fi
-	rm -f Makefile.coq
+	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: Make
-	coq_makefile -arg -w -arg -notation-overridden -f Make -o Makefile.coq
+	coq_makefile -f Make -o Makefile.coq
 
 .PHONY: default clean install
diff --git a/Heaps/Make b/Heaps/Make
@@ -1,14 +1,15 @@
-coding.v
-domain.v
-finmap.v
-heap.v
-idynamic.v
-ordtype.v
-pcm.v
-pperm.v
-pred.v
-prelude.v
-spcm.v
-unionmap.v
+-Q . DiSeL.Heaps
+-arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
 
--R . DiSeL.Heaps
+./coding.v
+./domain.v
+./finmap.v
+./heap.v
+./idynamic.v
+./ordtype.v
+./pcm.v
+./pperm.v
+./pred.v
+./prelude.v
+./spcm.v
+./unionmap.v
diff --git a/Heaps/Makefile b/Heaps/Makefile
@@ -11,9 +11,9 @@ install: Makefile.coq
 clean:
 	if [ -f Makefile.coq ]; then \
 	  $(MAKE) -f Makefile.coq clean; fi
-	rm -f Makefile.coq
+	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: Make
-	coq_makefile -arg -w -arg -notation-overridden -f Make -o Makefile.coq
+	coq_makefile -f Make -o Makefile.coq
 
 .PHONY: default clean install
diff --git a/Heaps/opam b/Heaps/opam
@@ -1,19 +1,19 @@
 opam-version: "1.2"
-name: "coq-disel-heaps"
+name: "disel-heaps"
 version: "dev"
 maintainer: "palmskog@gmail.com"
 
 homepage: "https://github.com/DistributedComponents/disel"
 dev-repo: "https://github.com/DistributedComponents/disel.git"
 bug-reports: "https://github.com/DistributedComponents/disel/issues"
-license: "Proprietary"
+license: "BSD2"
 
 build: [ make "-j" "%{jobs}%" ]
 install: [ make "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/DiSeL'" ]
 depends: [
-  "coq" { ((>= "8.6" & < "8.7~") | (= "dev")) }
-  "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev")) }
+  "coq" { ((>= "8.7" & < "8.8~") | (= "dev")) }
+  "coq-mathcomp-ssreflect" { ((>= "1.6.2" & < "1.7~") | (= "dev")) }
 ]
 
 tags: [
diff --git a/Makefile b/Makefile
@@ -11,10 +11,10 @@ install: Makefile.coq
 clean:
 	if [ -f Makefile.coq ]; then \
 	  $(MAKE) -f Makefile.coq clean; fi
-	rm -f Makefile.coq
+	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
-	coq_makefile -arg -w -arg -notation-overridden -f _CoqProject -o Makefile.coq
+	coq_makefile -f _CoqProject -o Makefile.coq
 
 TPCMain.d.byte: default
 	ocamlbuild -libs unix -I extraction/TPC -I shims shims/TPCMain.d.byte
diff --git a/_CoqProject b/_CoqProject
@@ -1,7 +1,6 @@
 -Q . DiSeL
 -arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
 
--R . DiSeL
 Heaps/coding.v
 Heaps/domain.v
 Heaps/finmap.v
