From a228537813acc5e6f43a77e1f4ce1fc04c6bd4bf Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 1 Oct 2023 11:27:53 +0200 Subject: [PATCH 1/2] purge OCamlbuild boilerplate, use simple Makefile, move bash scripts to scripts directory, update changelog --- CHANGELOG.md | 19 +++++- Makefile | 62 +++----------------- Makefile.coq.local | 16 ----- Makefile.ml-files | 10 ---- README.md | 16 +---- meta.yml | 36 ++---------- Settings.txt => scripts/Settings.txt | 0 Settings1.txt => scripts/Settings1.txt | 0 Settings2.txt => scripts/Settings2.txt | 0 batchrun => scripts/batchrun | 0 batchrundetach => scripts/batchrundetach | 0 clearnodes => scripts/clearnodes | 0 common => scripts/common | 0 fetchresults => scripts/fetchresults | 0 printlauncherout => scripts/printlauncherout | 0 printnodesout => scripts/printnodesout | 0 run => scripts/run | 0 17 files changed, 33 insertions(+), 126 deletions(-) delete mode 100644 Makefile.coq.local delete mode 100644 Makefile.ml-files rename Settings.txt => scripts/Settings.txt (100%) rename Settings1.txt => scripts/Settings1.txt (100%) rename Settings2.txt => scripts/Settings2.txt (100%) rename batchrun => scripts/batchrun (100%) rename batchrundetach => scripts/batchrundetach (100%) rename clearnodes => scripts/clearnodes (100%) rename common => scripts/common (100%) rename fetchresults => scripts/fetchresults (100%) rename printlauncherout => scripts/printlauncherout (100%) rename printnodesout => scripts/printnodesout (100%) rename run => scripts/run (100%) diff --git a/CHANGELOG.md b/CHANGELOG.md index d52ac55..20e0f9c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,20 @@ 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 + +### 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 +85,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 index ea39691..ad909e5 100644 --- 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 deleted file mode 100644 index 3bf458e..0000000 --- a/Makefile.coq.local +++ /dev/null @@ -1,16 +0,0 @@ -include Makefile.ml-files - -$(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) 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 diff --git a/Makefile.ml-files b/Makefile.ml-files deleted file mode 100644 index 0e11c0a..0000000 --- a/Makefile.ml-files +++ /dev/null @@ -1,10 +0,0 @@ -ALG1ML = ml/KVSAlg1.ml -ALG1MLI = ml/KVSAlg1.mli -ALG1 = $(ALG1ML) $(ALG1MLI) -ALG2ML = ml/KVSAlg2.ml -ALG2MLI = ml/KVSAlg2.mli -ALG2 = $(ALG2ML) $(ALG2MLI) -ALG3ML = ml/KVSAlg3.ml -ALG3MLI = ml/KVSAlg3.mli -ALG3 = $(ALG3ML) $(ALG3MLI) -ALGSML = $(ALG1) $(ALG2) $(ALG3) diff --git a/README.md b/README.md index 1bdeb8d..6cd496b 100644 --- a/README.md +++ b/README.md @@ -69,22 +69,10 @@ make # or make -j 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 diff --git a/meta.yml b/meta.yml index d253922..1ad6119 100644 --- 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,6 +69,10 @@ 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 diff --git a/Settings.txt b/scripts/Settings.txt similarity index 100% rename from Settings.txt rename to scripts/Settings.txt diff --git a/Settings1.txt b/scripts/Settings1.txt similarity index 100% rename from Settings1.txt rename to scripts/Settings1.txt diff --git a/Settings2.txt b/scripts/Settings2.txt similarity index 100% rename from Settings2.txt rename to scripts/Settings2.txt diff --git a/batchrun b/scripts/batchrun similarity index 100% rename from batchrun rename to scripts/batchrun diff --git a/batchrundetach b/scripts/batchrundetach similarity index 100% rename from batchrundetach rename to scripts/batchrundetach diff --git a/clearnodes b/scripts/clearnodes similarity index 100% rename from clearnodes rename to scripts/clearnodes diff --git a/common b/scripts/common similarity index 100% rename from common rename to scripts/common diff --git a/fetchresults b/scripts/fetchresults similarity index 100% rename from fetchresults rename to scripts/fetchresults diff --git a/printlauncherout b/scripts/printlauncherout similarity index 100% rename from printlauncherout rename to scripts/printlauncherout diff --git a/printnodesout b/scripts/printnodesout similarity index 100% rename from printnodesout rename to scripts/printnodesout diff --git a/run b/scripts/run similarity index 100% rename from run rename to scripts/run From 047438fc09672b7703143ba77fa68b1010688cd0 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 1 Oct 2023 11:32:07 +0200 Subject: [PATCH 2/2] use more standard theories/src directory names --- CHANGELOG.md | 1 + README.md | 8 +++---- _CoqProject | 22 +++++++++---------- meta.yml | 8 +++---- {ml => src}/bench/benchgen.ml | 0 {ml => src}/bench/dune | 0 {ml => src}/bench/experiment.ml | 0 {ml => src}/store1/ExtractAlgorithm1.v | 0 {ml => src}/store1/algorithm1.ml | 0 {ml => src}/store1/dune | 0 {ml => src}/store1/launchStore1.ml | 0 {ml => src}/store2/ExtractAlgorithm2.v | 0 {ml => src}/store2/algorithm2.ml | 0 {ml => src}/store2/dune | 0 {ml => src}/store2/launchStore2.ml | 0 {ml => src}/store3/ExtractAlgorithm3.v | 0 {ml => src}/store3/algorithm3.ml | 0 {ml => src}/store3/dune | 0 {ml => src}/store3/launchStore3.ml | 0 {ml => src}/utils/algorithm.ml | 0 {ml => src}/utils/benchprog.ml | 0 {ml => src}/utils/common.ml | 0 {ml => src}/utils/commonbench.ml | 0 {ml => src}/utils/configuration.ml | 0 {ml => src}/utils/dune | 0 {ml => src}/utils/readConfig.ml | 0 {ml => src}/utils/runtime.ml | 0 {ml => src}/utils/util.ml | 0 .../Algorithms/ExtractAlgorithm.v | 0 {coq => theories}/Algorithms/KVSAlg1.v | 0 {coq => theories}/Algorithms/KVSAlg2.v | 0 {coq => theories}/Algorithms/KVSAlg3.v | 0 {coq => theories}/Examples/Clients.v | 0 {coq => theories}/Examples/ListClient.v | 0 {coq => theories}/Framework/KVStore.v | 0 .../Framework/ReflectiveAbstractSemantics.v | 0 {coq => theories}/Lib/Predefs.v | 0 {coq => theories}/Lib/extralib.v | 0 {coq => theories}/dune | 0 39 files changed, 20 insertions(+), 19 deletions(-) rename {ml => src}/bench/benchgen.ml (100%) rename {ml => src}/bench/dune (100%) rename {ml => src}/bench/experiment.ml (100%) rename {ml => src}/store1/ExtractAlgorithm1.v (100%) rename {ml => src}/store1/algorithm1.ml (100%) rename {ml => src}/store1/dune (100%) rename {ml => src}/store1/launchStore1.ml (100%) rename {ml => src}/store2/ExtractAlgorithm2.v (100%) rename {ml => src}/store2/algorithm2.ml (100%) rename {ml => src}/store2/dune (100%) rename {ml => src}/store2/launchStore2.ml (100%) rename {ml => src}/store3/ExtractAlgorithm3.v (100%) rename {ml => src}/store3/algorithm3.ml (100%) rename {ml => src}/store3/dune (100%) rename {ml => src}/store3/launchStore3.ml (100%) rename {ml => src}/utils/algorithm.ml (100%) rename {ml => src}/utils/benchprog.ml (100%) rename {ml => src}/utils/common.ml (100%) rename {ml => src}/utils/commonbench.ml (100%) rename {ml => src}/utils/configuration.ml (100%) rename {ml => src}/utils/dune (100%) rename {ml => src}/utils/readConfig.ml (100%) rename {ml => src}/utils/runtime.ml (100%) rename {ml => src}/utils/util.ml (100%) rename {coq => theories}/Algorithms/ExtractAlgorithm.v (100%) rename {coq => theories}/Algorithms/KVSAlg1.v (100%) rename {coq => theories}/Algorithms/KVSAlg2.v (100%) rename {coq => theories}/Algorithms/KVSAlg3.v (100%) rename {coq => theories}/Examples/Clients.v (100%) rename {coq => theories}/Examples/ListClient.v (100%) rename {coq => theories}/Framework/KVStore.v (100%) rename {coq => theories}/Framework/ReflectiveAbstractSemantics.v (100%) rename {coq => theories}/Lib/Predefs.v (100%) rename {coq => theories}/Lib/extralib.v (100%) rename {coq => theories}/dune (100%) diff --git a/CHANGELOG.md b/CHANGELOG.md index 20e0f9c..9d4672e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - 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 diff --git a/README.md b/README.md index 6cd496b..9023cf4 100644 --- a/README.md +++ b/README.md @@ -78,7 +78,7 @@ Three key-value stores, verified to be causally consistent in the Coq proof assi ### 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 @@ -125,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 @@ -138,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 index b469be8..6fcc4a6 100644 --- 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 index 1ad6119..9704ac7 100644 --- a/meta.yml +++ b/meta.yml @@ -77,7 +77,7 @@ 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 @@ -124,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 @@ -137,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/ml/bench/benchgen.ml b/src/bench/benchgen.ml similarity index 100% rename from ml/bench/benchgen.ml rename to src/bench/benchgen.ml diff --git a/ml/bench/dune b/src/bench/dune similarity index 100% rename from ml/bench/dune rename to src/bench/dune diff --git a/ml/bench/experiment.ml b/src/bench/experiment.ml similarity index 100% rename from ml/bench/experiment.ml rename to src/bench/experiment.ml diff --git a/ml/store1/ExtractAlgorithm1.v b/src/store1/ExtractAlgorithm1.v similarity index 100% rename from ml/store1/ExtractAlgorithm1.v rename to src/store1/ExtractAlgorithm1.v diff --git a/ml/store1/algorithm1.ml b/src/store1/algorithm1.ml similarity index 100% rename from ml/store1/algorithm1.ml rename to src/store1/algorithm1.ml diff --git a/ml/store1/dune b/src/store1/dune similarity index 100% rename from ml/store1/dune rename to src/store1/dune diff --git a/ml/store1/launchStore1.ml b/src/store1/launchStore1.ml similarity index 100% rename from ml/store1/launchStore1.ml rename to src/store1/launchStore1.ml diff --git a/ml/store2/ExtractAlgorithm2.v b/src/store2/ExtractAlgorithm2.v similarity index 100% rename from ml/store2/ExtractAlgorithm2.v rename to src/store2/ExtractAlgorithm2.v diff --git a/ml/store2/algorithm2.ml b/src/store2/algorithm2.ml similarity index 100% rename from ml/store2/algorithm2.ml rename to src/store2/algorithm2.ml diff --git a/ml/store2/dune b/src/store2/dune similarity index 100% rename from ml/store2/dune rename to src/store2/dune diff --git a/ml/store2/launchStore2.ml b/src/store2/launchStore2.ml similarity index 100% rename from ml/store2/launchStore2.ml rename to src/store2/launchStore2.ml diff --git a/ml/store3/ExtractAlgorithm3.v b/src/store3/ExtractAlgorithm3.v similarity index 100% rename from ml/store3/ExtractAlgorithm3.v rename to src/store3/ExtractAlgorithm3.v diff --git a/ml/store3/algorithm3.ml b/src/store3/algorithm3.ml similarity index 100% rename from ml/store3/algorithm3.ml rename to src/store3/algorithm3.ml diff --git a/ml/store3/dune b/src/store3/dune similarity index 100% rename from ml/store3/dune rename to src/store3/dune diff --git a/ml/store3/launchStore3.ml b/src/store3/launchStore3.ml similarity index 100% rename from ml/store3/launchStore3.ml rename to src/store3/launchStore3.ml diff --git a/ml/utils/algorithm.ml b/src/utils/algorithm.ml similarity index 100% rename from ml/utils/algorithm.ml rename to src/utils/algorithm.ml diff --git a/ml/utils/benchprog.ml b/src/utils/benchprog.ml similarity index 100% rename from ml/utils/benchprog.ml rename to src/utils/benchprog.ml diff --git a/ml/utils/common.ml b/src/utils/common.ml similarity index 100% rename from ml/utils/common.ml rename to src/utils/common.ml diff --git a/ml/utils/commonbench.ml b/src/utils/commonbench.ml similarity index 100% rename from ml/utils/commonbench.ml rename to src/utils/commonbench.ml diff --git a/ml/utils/configuration.ml b/src/utils/configuration.ml similarity index 100% rename from ml/utils/configuration.ml rename to src/utils/configuration.ml diff --git a/ml/utils/dune b/src/utils/dune similarity index 100% rename from ml/utils/dune rename to src/utils/dune diff --git a/ml/utils/readConfig.ml b/src/utils/readConfig.ml similarity index 100% rename from ml/utils/readConfig.ml rename to src/utils/readConfig.ml diff --git a/ml/utils/runtime.ml b/src/utils/runtime.ml similarity index 100% rename from ml/utils/runtime.ml rename to src/utils/runtime.ml diff --git a/ml/utils/util.ml b/src/utils/util.ml similarity index 100% rename from ml/utils/util.ml rename to src/utils/util.ml diff --git a/coq/Algorithms/ExtractAlgorithm.v b/theories/Algorithms/ExtractAlgorithm.v similarity index 100% rename from coq/Algorithms/ExtractAlgorithm.v rename to theories/Algorithms/ExtractAlgorithm.v diff --git a/coq/Algorithms/KVSAlg1.v b/theories/Algorithms/KVSAlg1.v similarity index 100% rename from coq/Algorithms/KVSAlg1.v rename to theories/Algorithms/KVSAlg1.v diff --git a/coq/Algorithms/KVSAlg2.v b/theories/Algorithms/KVSAlg2.v similarity index 100% rename from coq/Algorithms/KVSAlg2.v rename to theories/Algorithms/KVSAlg2.v diff --git a/coq/Algorithms/KVSAlg3.v b/theories/Algorithms/KVSAlg3.v similarity index 100% rename from coq/Algorithms/KVSAlg3.v rename to theories/Algorithms/KVSAlg3.v diff --git a/coq/Examples/Clients.v b/theories/Examples/Clients.v similarity index 100% rename from coq/Examples/Clients.v rename to theories/Examples/Clients.v diff --git a/coq/Examples/ListClient.v b/theories/Examples/ListClient.v similarity index 100% rename from coq/Examples/ListClient.v rename to theories/Examples/ListClient.v diff --git a/coq/Framework/KVStore.v b/theories/Framework/KVStore.v similarity index 100% rename from coq/Framework/KVStore.v rename to theories/Framework/KVStore.v diff --git a/coq/Framework/ReflectiveAbstractSemantics.v b/theories/Framework/ReflectiveAbstractSemantics.v similarity index 100% rename from coq/Framework/ReflectiveAbstractSemantics.v rename to theories/Framework/ReflectiveAbstractSemantics.v diff --git a/coq/Lib/Predefs.v b/theories/Lib/Predefs.v similarity index 100% rename from coq/Lib/Predefs.v rename to theories/Lib/Predefs.v diff --git a/coq/Lib/extralib.v b/theories/Lib/extralib.v similarity index 100% rename from coq/Lib/extralib.v rename to theories/Lib/extralib.v diff --git a/coq/dune b/theories/dune similarity index 100% rename from coq/dune rename to theories/dune