Merge pull request #30 from coq-community/purge-old

Purge old boilerplate

Author: palmskog

CHANGELOG.md

@@ -1,60 +1,16 @@
-include Makefile.ml-files
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
-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
-
-coq: Makefile.coq
-	$(MAKE) -f Makefile.coq all
-
-stores: launchStore1.native launchStore2.native launchStore3.native
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
 	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-$(ALGSML): Makefile.coq
-	$(MAKE) -f Makefile.coq $@
-
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
-
-benchgen.native : $(MLFILES)
-	$(OCAMLBUILD) benchgen.native
+force _CoqProject Makefile: ;
 
-launchStore1.native: $(ALG1) $(MLFILES) benchgen.native
-	$(OCAMLBUILD) launchStore1.native
-
-launchStore2.native: $(ALG2) $(MLFILES) benchgen.native
-	$(OCAMLBUILD) launchStore2.native
-
-launchStore3.native: $(ALG3) $(MLFILES) benchgen.native
-	$(OCAMLBUILD) launchStore3.native
-
-experiment.native: $(MLFILES)
-	$(OCAMLBUILD) experiment.native 
-
-run: launchStore1.native launchStore2.native launchStore2.native benchgen.native
-	./batchrun
-
-run2: launchStore1.native launchStore2.native launchStore2.native benchgen.native
-	./batchrundetach
-
-clean: Makefile.coq
-	$(MAKE) -f Makefile.coq cleanall
-	$(OCAMLBUILD) launchStore1.native -clean
-	$(OCAMLBUILD) launchStore2.native -clean
-	$(OCAMLBUILD) launchStore3.native -clean
-	$(OCAMLBUILD) benchgen.native -clean
-	$(OCAMLBUILD) experiment.native -clean
-	rm -f Makefile.coq Makefile.coq.conf
-	rm -f RemoteAllOutputs.txt
-	rm -f RemoteAllResults.txt
-	rm -f RemoteLauncherOutput.txt
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: default coq run run2 clean install stores $(ALGSML)
-.NOTPARALLEL: $(ALGSML)
+.PHONY: all clean force

Makefile

@@ -1,12 +1,12 @@
--Q coq Chapar
+-Q theories Chapar
 
-coq/Lib/extralib.v
-coq/Lib/Predefs.v
-coq/Framework/KVStore.v
-coq/Framework/ReflectiveAbstractSemantics.v
-coq/Algorithms/KVSAlg1.v
-coq/Algorithms/KVSAlg2.v
-coq/Algorithms/KVSAlg3.v
-coq/Algorithms/ExtractAlgorithm.v
-coq/Examples/Clients.v
-coq/Examples/ListClient.v
+theories/Lib/extralib.v
+theories/Lib/Predefs.v
+theories/Framework/KVStore.v
+theories/Framework/ReflectiveAbstractSemantics.v
+theories/Algorithms/KVSAlg1.v
+theories/Algorithms/KVSAlg2.v
+theories/Algorithms/KVSAlg3.v
+theories/Algorithms/ExtractAlgorithm.v
+theories/Examples/Clients.v
+theories/Examples/ListClient.v

Makefile.coq.local

@@ -59,38 +59,6 @@ tested_coq_nix_versions:
 
 namespace: Chapar
 
-extracted:
-  extracted_fullname: Chapar Key-value Stores
-  extracted_shortname: chapar-kv-stores
-
-  extracted_synopsis: Three executable causally consistent distributed key-value stores
-  extracted_description: |
-    Three key-value stores, verified to be causally consistent in
-    the Coq proof assistant and extracted to executable code.
-
-  extracted_make_target: stores
-
-  extracted_supported_ocaml_versions:
-    text: 4.05.0 or later
-    opam: '{>= "4.05.0"}'
-
-  extracted_tested_coq_opam_versions:
-  - version: dev
-
-  extracted_dependencies:
-  - opam:
-      name: ocamlbuild
-      version: '{build}'
-    nix: ocamlbuild
-    description: >-
-      [OCamlbuild](https://github.com/ocaml/ocamlbuild)
-  - opam:
-      name: batteries
-      version: '{>= "2.8.0"}'
-    nix: batteries
-    description: >-
-      [Batteries Included](https://github.com/ocaml-batteries-team/batteries-included) 2.8.0 or later
-
 keywords:
 - name: causal consistency
 - name: key-value stores
@@ -101,11 +69,15 @@ categories:
 - name: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems
 
 documentation: |
+  ## Chapar Executable Key-value Stores
+
+  Three key-value stores, verified to be causally consistent in the Coq proof assistant and extracted to executable code. See [here](coq-chapar-stores.opam) for the requirements to build the stores.
+  
   ## Documentation
   
   ### Coq Framework
   
-  The Coq definitions and proofs are located in the `coq` directory. The code location of the definitions and lemmas presented in the paper are listed below.
+  The Coq definitions and proofs are located in the `theories` directory. The code location of the definitions and lemmas presented in the paper are listed below.
   
   #### Semantics and the Proof Technique
 
@@ -152,9 +124,9 @@ documentation: |
   
   #### Directory structure
 
-  - root (directory): The execution scripts described in the section Running Experiments below
+  - `scripts` (directory): The execution scripts described in the section Running Experiments below
 
-  - `coq` (directory); the Coq verification framework:
+  - `theories` (directory); the Coq verification framework:
     * `Framework/KVStore.v`: The basic definitions, the semantics and accompanying lemma
     * `Framework/ReflectiveAbstractSemantics.v`: The client verification definitions and lemmas
     * `Algorithms/KVSAlg1.v`: The definition and proof of algorithm 1 in the paper
@@ -165,7 +137,7 @@ documentation: |
     * `Examples/ListClient.v`: Verified client program
     * `Lib` (directory): General purpose Coq libraries
 
-  - `ml` (directory); the OCaml runtime to execute the algorithms:
+  - `src` (directory); the OCaml runtime to execute the algorithms:
     * `algorithm.ml`: Key-value store algorithm shared interface
     * `algorithm1.ml`, `algorithm2.ml`, `algorithm3.ml`: Wrappers for the extracted algorithms
     * `benchgen.ml`: Benchmark generation and storing program