Merge pull request #16 from coq-community/full-dune

Full Dune-based builds

.gitignore

@@ -11,16 +11,17 @@ Makefile.coq
 Makefile.coq.bak
 Makefile.coq.conf
 .coqdeps.d
-coq/KVSAlg1.ml
-coq/KVSAlg1.mli
-coq/KVSAlg2.ml
-coq/KVSAlg2.mli
-coq/KVSAlg3.ml
-coq/KVSAlg3.mli
+ml/KVSAlg1.ml
+ml/KVSAlg1.mli
+ml/KVSAlg2.ml
+ml/KVSAlg2.mli
+ml/KVSAlg3.ml
+ml/KVSAlg3.mli
 benchgen.native
 launchStore1.native
 launchStore2.native
 launchStore3.native
 experiment.native
 _build
 .lia.cache
+.merlin

.travis.yml

@@ -15,6 +15,7 @@ language: shell
       export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
       set -ex  # -e = exit on failure; -x = trace for debug
       opam update -y
+      for DEP in ${LOCAL_DEPS}; do opam pin add ${DEP} . -y -n -k path; done
       opam pin add ${PACKAGE} . -y -n -k path
       opam install ${PACKAGE} -y -j ${NJOBS} --deps-only
       opam config list
@@ -69,6 +70,7 @@ jobs:
   # Test extracted supported versions of Coq via OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:dev
-    - PACKAGE=chapar-kv-stores.dev
+    - PACKAGE=coq-chapar-stores.dev
+    - LOCAL_DEPS=coq-chapar.dev
     - NJOBS=2
     <<: *OPAM

CHANGELOG.md

@@ -5,11 +5,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ## [Unreleased]
 ### Changed
+- OCaml OPAM package definition uses Dune
+- Reorganize extraction to support Dune
+- Coq OPAM package definition uses Dune
 - Declare all scopes and consequently require Coq 8.10 or later
-- Coq OPAM package definition uses dune
 
 ### Added
-- Support for Coq builds with dune
+- Support for OCaml builds with Dune
+- Support for Coq builds with Dune
 
 ## [8.11.0] - 2020-01-31
 ### Fixed

Makefile

@@ -1,6 +1,11 @@
 include Makefile.ml-files
 
-OCAMLBUILD = ocamlbuild -tag safe_string -package batteries -I coq -I ml
+MLFILES = ml/algorithm.ml ml/algorithm1.ml ml/algorithm2.ml ml/algorithm3.ml \
+ ml/common.ml ml/benchgen.ml ml/benchprog.ml ml/commonbench.ml ml/configuration.ml \
+ ml/launchStore1.ml ml/launchStore2.ml ml/launchStore3.ml ml/runtime.ml \
+ ml/experiment.ml ml/readConfig.ml ml/util.ml
+
+OCAMLBUILD = ocamlbuild -tag safe_string -package batteries -I ml
 
 default: coq
 
@@ -18,22 +23,19 @@ $(ALGSML): Makefile.coq
 install: Makefile.coq
 	$(MAKE) -f Makefile.coq install
 
-benchgen.native : ml/*.ml
+benchgen.native : $(MLFILES)
 	$(OCAMLBUILD) benchgen.native
 
-launchStore1.native: $(ALG1) ml/*.ml benchgen.native
-	sed -i "s/failwith \"AXIOM TO BE REALIZED\"/4/g" $(ALG1ML)
+launchStore1.native: $(ALG1) $(MLFILES) benchgen.native
 	$(OCAMLBUILD) launchStore1.native
 
-launchStore2.native: $(ALG2) ml/*.ml benchgen.native
-	sed -i "s/failwith \"AXIOM TO BE REALIZED\"/4/g" $(ALG2ML)
+launchStore2.native: $(ALG2) $(MLFILES) benchgen.native
 	$(OCAMLBUILD) launchStore2.native
 
-launchStore3.native: $(ALG3) ml/*.ml benchgen.native
-	sed -i "s/failwith \"AXIOM TO BE REALIZED\"/4/g" $(ALG3ML)
+launchStore3.native: $(ALG3) $(MLFILES) benchgen.native
 	$(OCAMLBUILD) launchStore3.native
 
-experiment.native: ml/*.ml
+experiment.native: $(MLFILES)
 	$(OCAMLBUILD) experiment.native 
 
 run: launchStore1.native launchStore2.native launchStore2.native benchgen.native

Makefile.coq.local

@@ -1,7 +1,16 @@
 include Makefile.ml-files
 
-$(ALGSML): coq/Algorithms/Extract.v coq/Algorithms/KVSAlg1.vo coq/Algorithms/KVSAlg2.vo coq/Algorithms/KVSAlg3.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) coq/Algorithms/Extract.v
+$(ALG1): ml/ExtractAlgorithm1.v coq/Algorithms/KVSAlg1.vo coq/Algorithms/ExtractAlgorithm.vo
+	cd ml && $(COQC) $(COQDEBUG) $(COQFLAGS) -Q ../coq Chapar ExtractAlgorithm1.v
+
+$(ALG2): ml/ExtractAlgorithm2.v coq/Algorithms/KVSAlg2.vo coq/Algorithms/ExtractAlgorithm.vo
+	cd ml && $(COQC) $(COQDEBUG) $(COQFLAGS) -Q ../coq Chapar ExtractAlgorithm2.v
+
+$(ALG3): ml/ExtractAlgorithm3.v coq/Algorithms/KVSAlg3.vo coq/Algorithms/ExtractAlgorithm.vo
+	cd ml && $(COQC) $(COQDEBUG) $(COQFLAGS) -Q ../coq Chapar ExtractAlgorithm3.v
 
 clean::
-	rm -f $(ALGSML)
+	rm -f $(ALGSML) ml/.ExtractAlgorithm1.aux ml/.ExtractAlgorithm2.aux ml/.ExtractAlgorithm3.aux \
+	 ml/ExtractAlgorithm1.vo ml/ExtractAlgorithm1.vos ml/ExtractAlgorithm1.vok ml/ExtractAlgorithm1.glob \
+	 ml/ExtractAlgorithm2.vo ml/ExtractAlgorithm2.vos ml/ExtractAlgorithm2.vok ml/ExtractAlgorithm2.glob \
+	 ml/ExtractAlgorithm3.vo ml/ExtractAlgorithm3.vos ml/ExtractAlgorithm3.vok ml/ExtractAlgorithm3.glob

Makefile.ml-files

@@ -1,10 +1,10 @@
-ALG1ML = coq/KVSAlg1.ml
-ALG1MLI = coq/KVSAlg1.mli
+ALG1ML = ml/KVSAlg1.ml
+ALG1MLI = ml/KVSAlg1.mli
 ALG1 = $(ALG1ML) $(ALG1MLI)
-ALG2ML = coq/KVSAlg2.ml
-ALG2MLI = coq/KVSAlg2.mli
+ALG2ML = ml/KVSAlg2.ml
+ALG2MLI = ml/KVSAlg2.mli
 ALG2 = $(ALG2ML) $(ALG2MLI)
-ALG3ML = coq/KVSAlg3.ml
-ALG3MLI = coq/KVSAlg3.mli
+ALG3ML = ml/KVSAlg3.ml
+ALG3MLI = ml/KVSAlg3.mli
 ALG3 = $(ALG3ML) $(ALG3MLI)
 ALGSML = $(ALG1) $(ALG2) $(ALG3)

_CoqProject

@@ -1,9 +1,4 @@
--Q coq/Lib Chapar
--Q coq/Framework Chapar
--Q coq/Algorithms Chapar
--Q coq/Examples Chapar
-
--arg -w -arg -extraction-axiom-to-realize
+-Q coq Chapar
 
 coq/Lib/extralib.v
 coq/Lib/Predefs.v
@@ -12,6 +7,6 @@ coq/Framework/ReflectiveAbstractSemantics.v
 coq/Algorithms/KVSAlg1.v
 coq/Algorithms/KVSAlg2.v
 coq/Algorithms/KVSAlg3.v
-coq/Algorithms/Extract.v
+coq/Algorithms/ExtractAlgorithm.v
 coq/Examples/Clients.v
 coq/Examples/ListClient.v

chapar-kv-stores.opam → coq-chapar-stores.opam

@@ -12,12 +12,13 @@ Three key-value stores, verified to be causally consistent in
 the Coq proof assistant and extracted to executable code.
 """
 
-build: [make "-j%{jobs}%" "stores"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "ocaml" {>= "4.05.0"}
-  "coq" {(>= "8.9" & < "8.12~") | (= "dev")}
-  "ocamlbuild" {build}
+  "dune" {>= "2.5"}
+  "coq" {(>= "8.10" & < "8.13~") | (= "dev")}
   "batteries" {>= "2.8.0"}
+  "coq-chapar" {= version}
 ]
 
 authors: [

coq/Algorithms/Extract.v → coq/Algorithms/ExtractAlgorithm.v

@@ -11,10 +11,6 @@ Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
 Require Import ExtrOcamlString.
 
-From Chapar Require Import KVSAlg1.
-From Chapar Require Import KVSAlg2.
-From Chapar Require Import KVSAlg3.
-
 Extract Inlined Constant length => "List.length".
 Extract Inlined Constant negb => "not".
 Extract Inlined Constant app => "List.append".
@@ -25,7 +21,3 @@ Extract Inlined Constant in_dec => "(fun h -> List.mem)".
 Extract Inlined Constant leb => "(<=)".
 Extract Inlined Constant ltb => "(<)".
 Extract Inlined Constant pred => "(fun n -> if n <= 0 then 0 else n - 1)".
-
-Extraction "coq/KVSAlg1.ml" KVSAlg1.KVSAlg1.
-Extraction "coq/KVSAlg2.ml" KVSAlg2.KVSAlg2.
-Extraction "coq/KVSAlg3.ml" KVSAlg3.KVSAlg3.

coq/dune

@@ -1,8 +1,6 @@
 (coq.theory
  (name Chapar)
  (package coq-chapar)
- (synopsis "A framework for verification of causal consistency for distributed key-value stores and their clients in Coq")
- (modules :standard \ Algorithms.Extract)
- (flags -w -extraction-axiom-to-realize))
+ (synopsis "A framework for verification of causal consistency for distributed key-value stores and their clients in Coq"))
 
 (include_subdirs qualified)

ml/ExtractAlgorithm1.v

@@ -0,0 +1,6 @@
+From Chapar Require Import KVSAlg1.
+From Chapar Require Import ExtractAlgorithm.
+
+Extract Constant KVStore.SysPredefs.MaxNId => "4".
+
+Extraction "KVSAlg1.ml" KVSAlg1.KVSAlg1.

ml/ExtractAlgorithm2.v

@@ -0,0 +1,6 @@
+From Chapar Require Import KVSAlg2.
+From Chapar Require Import ExtractAlgorithm.
+
+Extract Constant KVStore.SysPredefs.MaxNId => "4".
+
+Extraction "KVSAlg2.ml" KVSAlg2.KVSAlg2.

ml/ExtractAlgorithm3.v

@@ -0,0 +1,6 @@
+From Chapar Require Import KVSAlg3.
+From Chapar Require Import ExtractAlgorithm.
+
+Extract Constant KVStore.SysPredefs.MaxNId => "4".
+
+Extraction "KVSAlg3.ml" KVSAlg3.KVSAlg3.

ml/dune

@@ -0,0 +1,62 @@
+(executable
+ (name launchStore1)
+ (flags :standard -warn-error -a -w -27-33-39)
+ (public_name chaparStore1)
+ (libraries utils batteries)
+ (modules launchStore1 KVSAlg1 algorithm1)
+ (package coq-chapar-stores))
+
+(executable
+ (name launchStore2)
+ (flags :standard -warn-error -a -w -27-33-39)
+ (public_name chaparStore2)
+ (libraries utils batteries)
+ (modules launchStore2 KVSAlg2 algorithm2)
+ (package coq-chapar-stores))
+
+(executable
+ (name launchStore3)
+ (flags :standard -warn-error -a -w -27-33-39)
+ (public_name chaparStore3)
+ (libraries utils batteries)
+ (modules launchStore3 KVSAlg3 algorithm3)
+ (package coq-chapar-stores))
+
+(executable
+ (name benchgen)
+ (flags :standard -w -35)
+ (public_name chaparBenchgen)
+ (libraries utils)
+ (modules benchgen)
+ (package coq-chapar-stores))
+
+(executable
+ (name experiment)
+ (flags :standard -w -33-35)
+ (libraries utils)
+ (modules experiment))
+
+(coq.extraction
+ (prelude ExtractAlgorithm1)
+ (extracted_modules KVSAlg1)
+ ;(theories Chapar)
+)
+
+(coq.extraction
+ (prelude ExtractAlgorithm2)
+ (extracted_modules KVSAlg2)
+ ;(theories Chapar)
+)
+
+(coq.extraction
+ (prelude ExtractAlgorithm3)
+ (extracted_modules KVSAlg3)
+ ;(theories Chapar)
+)
+
+(library
+ (name utils)
+ (flags :standard -w -27-33-35)
+ (modules util runtime configuration common algorithm readConfig benchprog commonbench)
+ (wrapped false)
+ (libraries unix))

ml/experiment.ml

@@ -1,4 +1,3 @@
-open Pervasives
 (* open Printf *)
 open Configuration
 open ReadConfig