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

Purge old boilerplate
coq-community · Oct 1, 2023 · 95e4b27 · 95e4b27
2 parents 52504cc + 047438f
commit 95e4b27
Show file tree

Hide file tree

Showing 53 changed files with 53 additions and 145 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -5,6 +5,21 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ## [Unreleased]
 
+## [8.16.0] - 2023-10-01
+
+### Changed
+- Adjust build for Coq 8.18 and beyond
+- Use Dune wrapping for OCaml modules
+- Remove boilerplate for OCamlbuild
+- Move bash scripts to scripts directory
+- Use standard theories/src directory names
+
+### Fixed
+- Stores build with Dune 3.6 or later
+- Nix CI configuration
+- List lemma deprecations in 8.18
+
+## [8.15.0] - 2023-02-05
 ### Changed
 - Removed unecessary imports
 - Adjust build for Coq 8.16 and beyond
@@ -71,7 +86,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Modernize build scripts to use `coq_makefile` features
 - Reorganize code into subdirectories
 
-[Unreleased]: https://github.com/coq-community/chapar/compare/v8.13.0...master
+[Unreleased]: https://github.com/coq-community/chapar/compare/v8.16.0...master
+[8.16.0]: https://github.com/coq-community/chapar/releases/tag/v8.16.0
+[8.15.0]: https://github.com/coq-community/chapar/releases/tag/v8.15.0
+[8.14.0]: https://github.com/coq-community/chapar/releases/tag/v8.14.0
 [8.13.0]: https://github.com/coq-community/chapar/releases/tag/v8.13.0
 [8.12.0]: https://github.com/coq-community/chapar/releases/tag/v8.12.0
 [8.11.0]: https://github.com/coq-community/chapar/releases/tag/v8.11.0

diff --git a/Makefile b/Makefile
@@ -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
diff --git a/Makefile.coq.local b/Makefile.coq.local
diff --git a/Makefile.ml-files b/Makefile.ml-files
diff --git a/README.md b/README.md
@@ -69,28 +69,16 @@ make   # or make -j <number-of-cores-on-your-machine>
 make install
 ```
 
-## Chapar Key-value Stores
 
-Three key-value stores, verified to be causally consistent in
-the Coq proof assistant and extracted to executable code.
+## Chapar Executable Key-value Stores
 
-
-- Compatible OCaml versions: 4.05.0 or later
-- Additional dependencies:
-  - [OCamlbuild](https://github.com/ocaml/ocamlbuild) 
-  - [Batteries Included](https://github.com/ocaml-batteries-team/batteries-included) 2.8.0 or later 
-
-### Building
-To extract the code and compile manually, use the following command:
-```
-make 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
 
@@ -137,9 +125,9 @@ The Coq definitions and proofs are located in the `coq` directory. The code loca
 
 #### 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
@@ -150,7 +138,7 @@ The Coq definitions and proofs are located in the `coq` directory. The code loca
   * `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

diff --git a/_CoqProject b/_CoqProject
@@ -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
diff --git a/meta.yml b/meta.yml
@@ -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

diff --git a/Settings.txt → scripts/Settings.txt b/Settings.txt → scripts/Settings.txt
diff --git a/Settings1.txt → scripts/Settings1.txt b/Settings1.txt → scripts/Settings1.txt
diff --git a/Settings2.txt → scripts/Settings2.txt b/Settings2.txt → scripts/Settings2.txt
diff --git a/batchrun → scripts/batchrun b/batchrun → scripts/batchrun
diff --git a/batchrundetach → scripts/batchrundetach b/batchrundetach → scripts/batchrundetach
diff --git a/clearnodes → scripts/clearnodes b/clearnodes → scripts/clearnodes
diff --git a/common → scripts/common b/common → scripts/common
diff --git a/fetchresults → scripts/fetchresults b/fetchresults → scripts/fetchresults
diff --git a/printlauncherout → scripts/printlauncherout b/printlauncherout → scripts/printlauncherout
diff --git a/printnodesout → scripts/printnodesout b/printnodesout → scripts/printnodesout
diff --git a/run → scripts/run b/run → scripts/run
diff --git a/ml/bench/benchgen.ml → src/bench/benchgen.ml b/ml/bench/benchgen.ml → src/bench/benchgen.ml
diff --git a/ml/bench/dune → src/bench/dune b/ml/bench/dune → src/bench/dune
diff --git a/ml/bench/experiment.ml → src/bench/experiment.ml b/ml/bench/experiment.ml → src/bench/experiment.ml
diff --git a/ml/store1/ExtractAlgorithm1.v → src/store1/ExtractAlgorithm1.v b/ml/store1/ExtractAlgorithm1.v → src/store1/ExtractAlgorithm1.v
diff --git a/ml/store1/algorithm1.ml → src/store1/algorithm1.ml b/ml/store1/algorithm1.ml → src/store1/algorithm1.ml
diff --git a/ml/store1/dune → src/store1/dune b/ml/store1/dune → src/store1/dune
diff --git a/ml/store1/launchStore1.ml → src/store1/launchStore1.ml b/ml/store1/launchStore1.ml → src/store1/launchStore1.ml
diff --git a/ml/store2/ExtractAlgorithm2.v → src/store2/ExtractAlgorithm2.v b/ml/store2/ExtractAlgorithm2.v → src/store2/ExtractAlgorithm2.v
diff --git a/ml/store2/algorithm2.ml → src/store2/algorithm2.ml b/ml/store2/algorithm2.ml → src/store2/algorithm2.ml
diff --git a/ml/store2/dune → src/store2/dune b/ml/store2/dune → src/store2/dune
diff --git a/ml/store2/launchStore2.ml → src/store2/launchStore2.ml b/ml/store2/launchStore2.ml → src/store2/launchStore2.ml
diff --git a/ml/store3/ExtractAlgorithm3.v → src/store3/ExtractAlgorithm3.v b/ml/store3/ExtractAlgorithm3.v → src/store3/ExtractAlgorithm3.v
diff --git a/ml/store3/algorithm3.ml → src/store3/algorithm3.ml b/ml/store3/algorithm3.ml → src/store3/algorithm3.ml
diff --git a/ml/store3/dune → src/store3/dune b/ml/store3/dune → src/store3/dune
diff --git a/ml/store3/launchStore3.ml → src/store3/launchStore3.ml b/ml/store3/launchStore3.ml → src/store3/launchStore3.ml
diff --git a/ml/utils/algorithm.ml → src/utils/algorithm.ml b/ml/utils/algorithm.ml → src/utils/algorithm.ml
diff --git a/ml/utils/benchprog.ml → src/utils/benchprog.ml b/ml/utils/benchprog.ml → src/utils/benchprog.ml
diff --git a/ml/utils/common.ml → src/utils/common.ml b/ml/utils/common.ml → src/utils/common.ml
diff --git a/ml/utils/commonbench.ml → src/utils/commonbench.ml b/ml/utils/commonbench.ml → src/utils/commonbench.ml
diff --git a/ml/utils/configuration.ml → src/utils/configuration.ml b/ml/utils/configuration.ml → src/utils/configuration.ml
diff --git a/ml/utils/dune → src/utils/dune b/ml/utils/dune → src/utils/dune
diff --git a/ml/utils/readConfig.ml → src/utils/readConfig.ml b/ml/utils/readConfig.ml → src/utils/readConfig.ml
diff --git a/ml/utils/runtime.ml → src/utils/runtime.ml b/ml/utils/runtime.ml → src/utils/runtime.ml
diff --git a/ml/utils/util.ml → src/utils/util.ml b/ml/utils/util.ml → src/utils/util.ml
diff --git a/coq/Algorithms/ExtractAlgorithm.v → theories/Algorithms/ExtractAlgorithm.v b/coq/Algorithms/ExtractAlgorithm.v → theories/Algorithms/ExtractAlgorithm.v
diff --git a/coq/Algorithms/KVSAlg1.v → theories/Algorithms/KVSAlg1.v b/coq/Algorithms/KVSAlg1.v → theories/Algorithms/KVSAlg1.v
diff --git a/coq/Algorithms/KVSAlg2.v → theories/Algorithms/KVSAlg2.v b/coq/Algorithms/KVSAlg2.v → theories/Algorithms/KVSAlg2.v
diff --git a/coq/Algorithms/KVSAlg3.v → theories/Algorithms/KVSAlg3.v b/coq/Algorithms/KVSAlg3.v → theories/Algorithms/KVSAlg3.v
diff --git a/coq/Examples/Clients.v → theories/Examples/Clients.v b/coq/Examples/Clients.v → theories/Examples/Clients.v
diff --git a/coq/Examples/ListClient.v → theories/Examples/ListClient.v b/coq/Examples/ListClient.v → theories/Examples/ListClient.v
diff --git a/coq/Framework/KVStore.v → theories/Framework/KVStore.v b/coq/Framework/KVStore.v → theories/Framework/KVStore.v
diff --git a/coq/Framework/ReflectiveAbstractSemantics.v → ...s/Framework/ReflectiveAbstractSemantics.v b/coq/Framework/ReflectiveAbstractSemantics.v → ...s/Framework/ReflectiveAbstractSemantics.v
diff --git a/coq/Lib/Predefs.v → theories/Lib/Predefs.v b/coq/Lib/Predefs.v → theories/Lib/Predefs.v
diff --git a/coq/Lib/extralib.v → theories/Lib/extralib.v b/coq/Lib/extralib.v → theories/Lib/extralib.v
diff --git a/coq/dune → theories/dune b/coq/dune → theories/dune