From e17db7704cc9e95d3e6f2dfdcfff60c7795a0539 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 5 Nov 2023 17:49:49 +0100
Subject: [PATCH 1/2] port vard to build with Dune

---
 .gitignore                                    |  1 +
 extraction/vard/{coq => }/ExtractVarDRaft.v   |  2 +-
 extraction/vard/{ml => }/VarDArrangement.ml   |  3 -
 extraction/vard/{ml => }/VarDSerialization.ml |  1 -
 extraction/vard/dune                          | 23 +++++
 extraction/vard/scripts/vard.conf             | 12 ---
 extraction/vard/{ml => }/vard.ml              |  1 -
 script/coqproject.sh                          | 89 -------------------
 {extraction => script}/vard/Makefile          |  0
 {extraction => script}/vard/bench/bench.py    |  0
 {extraction => script}/vard/bench/etcd.py     |  0
 {extraction => script}/vard/bench/etcd.txt    |  0
 .../vard/bench/experiment.py                  |  0
 .../vard/bench/experiments/example.yml        |  0
 .../bench/experiments/ssd-etcd-throughput.yml |  0
 .../bench/experiments/ssd-vard-throughput.yml |  0
 .../vard/bench/experiments/vard.yml           |  0
 {extraction => script}/vard/bench/setup.py    |  0
 {extraction => script}/vard/bench/vard.py     |  0
 {extraction => script}/vard/bench/vard.txt    |  0
 .../vard/bench/vard_open_loop.py              |  0
 {extraction => script}/vard/bench/vardctl.py  |  0
 .../scripts => script/vard/run}/bench-etcd.sh |  0
 .../scripts => script/vard/run}/bench-vard.sh |  0
 .../scripts => script/vard/run}/clear-etcd.sh |  0
 .../scripts => script/vard/run}/clear-vard.sh |  0
 .../vard/scripts => script/vard/run}/run.sh   |  0
 .../scripts => script/vard/run}/start-node.sh |  0
 .../vard/run}/start-tmux-debug.sh             |  0
 .../scripts => script/vard/run}/start-tmux.sh |  0
 .../vard/test/integration.py                  |  0
 .../vard/test => tests/vard}/OptsTest.ml      |  0
 .../vard}/VarDSerializationTest.ml            |  0
 .../vard/test => tests/vard}/VarDTest.ml      |  0
 tests/vard/dune                               |  4 +
 vard.opam                                     |  8 +-
 36 files changed, 32 insertions(+), 112 deletions(-)
 rename extraction/vard/{coq => }/ExtractVarDRaft.v (82%)
 rename extraction/vard/{ml => }/VarDArrangement.ml (99%)
 rename extraction/vard/{ml => }/VarDSerialization.ml (99%)
 create mode 100644 extraction/vard/dune
 delete mode 100644 extraction/vard/scripts/vard.conf
 rename extraction/vard/{ml => }/vard.ml (99%)
 delete mode 100755 script/coqproject.sh
 rename {extraction => script}/vard/Makefile (100%)
 rename {extraction => script}/vard/bench/bench.py (100%)
 rename {extraction => script}/vard/bench/etcd.py (100%)
 rename {extraction => script}/vard/bench/etcd.txt (100%)
 rename {extraction => script}/vard/bench/experiment.py (100%)
 rename {extraction => script}/vard/bench/experiments/example.yml (100%)
 rename {extraction => script}/vard/bench/experiments/ssd-etcd-throughput.yml (100%)
 rename {extraction => script}/vard/bench/experiments/ssd-vard-throughput.yml (100%)
 rename {extraction => script}/vard/bench/experiments/vard.yml (100%)
 rename {extraction => script}/vard/bench/setup.py (100%)
 rename {extraction => script}/vard/bench/vard.py (100%)
 rename {extraction => script}/vard/bench/vard.txt (100%)
 rename {extraction => script}/vard/bench/vard_open_loop.py (100%)
 rename {extraction => script}/vard/bench/vardctl.py (100%)
 rename {extraction/vard/scripts => script/vard/run}/bench-etcd.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/bench-vard.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/clear-etcd.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/clear-vard.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/run.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/start-node.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/start-tmux-debug.sh (100%)
 rename {extraction/vard/scripts => script/vard/run}/start-tmux.sh (100%)
 rename {extraction => script}/vard/test/integration.py (100%)
 rename {extraction/vard/test => tests/vard}/OptsTest.ml (100%)
 rename {extraction/vard/test => tests/vard}/VarDSerializationTest.ml (100%)
 rename {extraction/vard/test => tests/vard}/VarDTest.ml (100%)
 create mode 100644 tests/vard/dune

diff --git a/.gitignore b/.gitignore
index 16e31f04..5d978cd5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,7 @@
 *.glob
 *.v.d
 *.buildtime
+_build
 Makefile.coq
 Makefile.coq.bak
 Makefile.coq.conf
diff --git a/extraction/vard/coq/ExtractVarDRaft.v b/extraction/vard/ExtractVarDRaft.v
similarity index 82%
rename from extraction/vard/coq/ExtractVarDRaft.v
rename to extraction/vard/ExtractVarDRaft.v
index 0eec7b12..185a717c 100644
--- a/extraction/vard/coq/ExtractVarDRaft.v
+++ b/extraction/vard/ExtractVarDRaft.v
@@ -4,5 +4,5 @@ From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString.
 From Verdi Require Import ExtrOcamlBasicExt ExtrOcamlNatIntExt.
 From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt.
 
-Extraction "extraction/vard/ml/VarDRaft.ml" seq vard_raft_base_params
+Extraction "VarDRaft.ml" seq vard_raft_base_params
   vard_raft_multi_params vard_raft_failure_params.
diff --git a/extraction/vard/ml/VarDArrangement.ml b/extraction/vard/VarDArrangement.ml
similarity index 99%
rename from extraction/vard/ml/VarDArrangement.ml
rename to extraction/vard/VarDArrangement.ml
index 4adfd0a2..9f1d2fb6 100644
--- a/extraction/vard/ml/VarDArrangement.ml
+++ b/extraction/vard/VarDArrangement.ml
@@ -1,8 +1,5 @@
-open Str
 open Printf
 open VarDRaft
-open VarD
-open Util
 
 module type IntValue = sig
   val v : int
diff --git a/extraction/vard/ml/VarDSerialization.ml b/extraction/vard/VarDSerialization.ml
similarity index 99%
rename from extraction/vard/ml/VarDSerialization.ml
rename to extraction/vard/VarDSerialization.ml
index 9e1f2e3d..aa96dff9 100644
--- a/extraction/vard/ml/VarDSerialization.ml
+++ b/extraction/vard/VarDSerialization.ml
@@ -1,7 +1,6 @@
 open Str
 open Printf
 open VarDRaft
-open VarD
 open Util
 
 let serializeOutput out =
diff --git a/extraction/vard/dune b/extraction/vard/dune
new file mode 100644
index 00000000..a2c75fd2
--- /dev/null
+++ b/extraction/vard/dune
@@ -0,0 +1,23 @@
+(library
+ (name VarDRaft)
+ (flags :standard -w -27-32-39-67)
+ (modules VarDRaft))
+
+(library
+ (name VarDSerialization)
+ (libraries verdi-runtime VarDRaft)
+ (modules VarDSerialization))
+
+(coq.extraction
+ (prelude ExtractVarDRaft)
+ (extracted_modules VarDRaft)
+ (theories VerdiRaft)
+ (flags :standard -w -extraction-opaque-accessed))
+
+(executable
+ (name vard)
+ (public_name vard) 
+ (libraries verdi-runtime VarDRaft VarDSerialization)
+ (flags :standard -w -27)
+ (modules vard VarDArrangement)
+ (package vard))
diff --git a/extraction/vard/scripts/vard.conf b/extraction/vard/scripts/vard.conf
deleted file mode 100644
index 1b7a2849..00000000
--- a/extraction/vard/scripts/vard.conf
+++ /dev/null
@@ -1,12 +0,0 @@
-# Ubuntu upstart file at /etc/init/vard.conf
-
-pre-start script
-  mkdir -p /var/lib/vard
-  chown ubuntu:ubuntu /var/lib/vard
-  mkdir -p /var/log/vard
-  chown ubuntu:ubuntu /var/log/vard
-end script
-
-script
-  su - ubuntu -c "exec env OCAMLRUNPARAM=b /vard/vard.native -dbpath /var/lib/vard -port 8351 -node 1,$db1:8351 -node 2,$db2:8351 -node 3,$db3:8351 -me $id 2>&1" >> /var/log/vard/vard.log
-end script
diff --git a/extraction/vard/ml/vard.ml b/extraction/vard/vard.ml
similarity index 99%
rename from extraction/vard/ml/vard.ml
rename to extraction/vard/vard.ml
index b1f12e43..bbbc353b 100644
--- a/extraction/vard/ml/vard.ml
+++ b/extraction/vard/vard.ml
@@ -1,6 +1,5 @@
 open List
 open Printf
-open Str
 open Opts
 
 let _ =
diff --git a/script/coqproject.sh b/script/coqproject.sh
deleted file mode 100755
index 0b834bb6..00000000
--- a/script/coqproject.sh
+++ /dev/null
@@ -1,89 +0,0 @@
-#!/usr/bin/env bash
-
-### coqproject.sh
-### Creates a _CoqProject file, including external dependencies.
-
-### See the README.md file for a description.
-
-## Implementation
-
-if [ -z ${DIRS+x} ]; then DIRS=(.); fi
-
-COQPROJECT_TMP=_CoqProject.tmp
-
-rm -f $COQPROJECT_TMP
-touch $COQPROJECT_TMP
-
-function dep_dirs_lines(){
-  dep_dirs_var="$2"_DIRS
-  local -a 'dep_dirs=("${'"$dep_dirs_var"'[@]}")'
-  if [ "x${dep_dirs[0]}" = "x" ]; then dep_dirs=(.); fi
-  for dep_dir in "${dep_dirs[@]}"; do
-      namespace_var=NAMESPACE_"$2"_"$dep_dir"
-      namespace_var=${namespace_var//\//_}
-      namespace_var=${namespace_var//-/_}
-      namespace_var=${namespace_var//./_}
-      namespace=${!namespace_var:=$2}
-      if [ $dep_dir = "." ]; then
-        LINE="-Q $1 $namespace"
-      else
-        LINE="-Q $1/$dep_dir $namespace"
-      fi
-      echo $LINE >> $COQPROJECT_TMP
-  done
-}
-for dep in ${DEPS[@]}; do
-    path_var="$dep"_PATH
-    if [ ! "x${!path_var}" = "x" ]; then
-	path=${!path_var}
-	if [ ! -d "$path" ]; then
-            echo "$dep not found at $path."
-            exit 1
-	fi
-
-	pushd "$path" > /dev/null
-	path=$(pwd)
-	popd > /dev/null
-	echo "$dep found at $path"
-
-	dep_dirs_lines $path $dep
-    fi
-done
-
-COQTOP="coqtop $(cat $COQPROJECT_TMP)"
-function check_canary(){
-    echo "Require Import $@." | $COQTOP 2>&1 | grep -i error 1> /dev/null 2>&1 
-}
-i=0
-len="${#CANARIES[@]}"
-while [ $i -lt $len ]; do
-    if check_canary ${CANARIES[$i]}; then
-        echo "Error: ${CANARIES[$((i + 1))]}"
-        exit 1
-    fi
-    let "i+=2"
-done
-
-for dir in ${DIRS[@]}; do
-    namespace_var=NAMESPACE_"$dir"
-    namespace_var=${namespace_var//\//_}
-    namespace_var=${namespace_var//-/_}
-    namespace_var=${namespace_var//./_}
-    namespace=${!namespace_var:="''"}
-    LINE="-Q $dir $namespace"
-    echo $LINE >> $COQPROJECT_TMP
-done
-
-for dir in ${DIRS[@]}; do
-    echo >> $COQPROJECT_TMP
-    find $dir -iname '*.v' -not -name '*\#*'  >> $COQPROJECT_TMP
-done
-
-for extra in ${EXTRA[@]}; do
-    if ! grep --quiet "^$extra\$" $COQPROJECT_TMP; then
-        echo >> $COQPROJECT_TMP
-        echo $extra >> $COQPROJECT_TMP
-    fi
-done
-
-mv $COQPROJECT_TMP _CoqProject
diff --git a/extraction/vard/Makefile b/script/vard/Makefile
similarity index 100%
rename from extraction/vard/Makefile
rename to script/vard/Makefile
diff --git a/extraction/vard/bench/bench.py b/script/vard/bench/bench.py
similarity index 100%
rename from extraction/vard/bench/bench.py
rename to script/vard/bench/bench.py
diff --git a/extraction/vard/bench/etcd.py b/script/vard/bench/etcd.py
similarity index 100%
rename from extraction/vard/bench/etcd.py
rename to script/vard/bench/etcd.py
diff --git a/extraction/vard/bench/etcd.txt b/script/vard/bench/etcd.txt
similarity index 100%
rename from extraction/vard/bench/etcd.txt
rename to script/vard/bench/etcd.txt
diff --git a/extraction/vard/bench/experiment.py b/script/vard/bench/experiment.py
similarity index 100%
rename from extraction/vard/bench/experiment.py
rename to script/vard/bench/experiment.py
diff --git a/extraction/vard/bench/experiments/example.yml b/script/vard/bench/experiments/example.yml
similarity index 100%
rename from extraction/vard/bench/experiments/example.yml
rename to script/vard/bench/experiments/example.yml
diff --git a/extraction/vard/bench/experiments/ssd-etcd-throughput.yml b/script/vard/bench/experiments/ssd-etcd-throughput.yml
similarity index 100%
rename from extraction/vard/bench/experiments/ssd-etcd-throughput.yml
rename to script/vard/bench/experiments/ssd-etcd-throughput.yml
diff --git a/extraction/vard/bench/experiments/ssd-vard-throughput.yml b/script/vard/bench/experiments/ssd-vard-throughput.yml
similarity index 100%
rename from extraction/vard/bench/experiments/ssd-vard-throughput.yml
rename to script/vard/bench/experiments/ssd-vard-throughput.yml
diff --git a/extraction/vard/bench/experiments/vard.yml b/script/vard/bench/experiments/vard.yml
similarity index 100%
rename from extraction/vard/bench/experiments/vard.yml
rename to script/vard/bench/experiments/vard.yml
diff --git a/extraction/vard/bench/setup.py b/script/vard/bench/setup.py
similarity index 100%
rename from extraction/vard/bench/setup.py
rename to script/vard/bench/setup.py
diff --git a/extraction/vard/bench/vard.py b/script/vard/bench/vard.py
similarity index 100%
rename from extraction/vard/bench/vard.py
rename to script/vard/bench/vard.py
diff --git a/extraction/vard/bench/vard.txt b/script/vard/bench/vard.txt
similarity index 100%
rename from extraction/vard/bench/vard.txt
rename to script/vard/bench/vard.txt
diff --git a/extraction/vard/bench/vard_open_loop.py b/script/vard/bench/vard_open_loop.py
similarity index 100%
rename from extraction/vard/bench/vard_open_loop.py
rename to script/vard/bench/vard_open_loop.py
diff --git a/extraction/vard/bench/vardctl.py b/script/vard/bench/vardctl.py
similarity index 100%
rename from extraction/vard/bench/vardctl.py
rename to script/vard/bench/vardctl.py
diff --git a/extraction/vard/scripts/bench-etcd.sh b/script/vard/run/bench-etcd.sh
similarity index 100%
rename from extraction/vard/scripts/bench-etcd.sh
rename to script/vard/run/bench-etcd.sh
diff --git a/extraction/vard/scripts/bench-vard.sh b/script/vard/run/bench-vard.sh
similarity index 100%
rename from extraction/vard/scripts/bench-vard.sh
rename to script/vard/run/bench-vard.sh
diff --git a/extraction/vard/scripts/clear-etcd.sh b/script/vard/run/clear-etcd.sh
similarity index 100%
rename from extraction/vard/scripts/clear-etcd.sh
rename to script/vard/run/clear-etcd.sh
diff --git a/extraction/vard/scripts/clear-vard.sh b/script/vard/run/clear-vard.sh
similarity index 100%
rename from extraction/vard/scripts/clear-vard.sh
rename to script/vard/run/clear-vard.sh
diff --git a/extraction/vard/scripts/run.sh b/script/vard/run/run.sh
similarity index 100%
rename from extraction/vard/scripts/run.sh
rename to script/vard/run/run.sh
diff --git a/extraction/vard/scripts/start-node.sh b/script/vard/run/start-node.sh
similarity index 100%
rename from extraction/vard/scripts/start-node.sh
rename to script/vard/run/start-node.sh
diff --git a/extraction/vard/scripts/start-tmux-debug.sh b/script/vard/run/start-tmux-debug.sh
similarity index 100%
rename from extraction/vard/scripts/start-tmux-debug.sh
rename to script/vard/run/start-tmux-debug.sh
diff --git a/extraction/vard/scripts/start-tmux.sh b/script/vard/run/start-tmux.sh
similarity index 100%
rename from extraction/vard/scripts/start-tmux.sh
rename to script/vard/run/start-tmux.sh
diff --git a/extraction/vard/test/integration.py b/script/vard/test/integration.py
similarity index 100%
rename from extraction/vard/test/integration.py
rename to script/vard/test/integration.py
diff --git a/extraction/vard/test/OptsTest.ml b/tests/vard/OptsTest.ml
similarity index 100%
rename from extraction/vard/test/OptsTest.ml
rename to tests/vard/OptsTest.ml
diff --git a/extraction/vard/test/VarDSerializationTest.ml b/tests/vard/VarDSerializationTest.ml
similarity index 100%
rename from extraction/vard/test/VarDSerializationTest.ml
rename to tests/vard/VarDSerializationTest.ml
diff --git a/extraction/vard/test/VarDTest.ml b/tests/vard/VarDTest.ml
similarity index 100%
rename from extraction/vard/test/VarDTest.ml
rename to tests/vard/VarDTest.ml
diff --git a/tests/vard/dune b/tests/vard/dune
new file mode 100644
index 00000000..2c88c4fd
--- /dev/null
+++ b/tests/vard/dune
@@ -0,0 +1,4 @@
+(test
+ (name VarDTest)
+ (flags :standard -w -27)
+ (libraries verdi-runtime VarDSerialization VarDRaft ounit2))
diff --git a/vard.opam b/vard.opam
index 2509a156..86df1bde 100644
--- a/vard.opam
+++ b/vard.opam
@@ -8,15 +8,13 @@ bug-reports: "https://github.com/uwplse/verdi-raft/issues"
 license: "BSD-2-Clause"
 synopsis: "Fault-tolerant distributed key-value store using a verified implementation of Raft consensus"
 
-build: [make "-j%{jobs}%" "vard"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "ocaml" {>= "4.05.0"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.14"}
-  "coq-verdi" {= "dev"}
-  "coq-struct-tact" {= "dev"}
-  "coq-cheerios" {= "dev"}
+  "coq-verdi-raft" {= "dev"}
   "verdi-runtime" {= "dev"}
-  "ocamlbuild" {build}
   "ounit" {with-test & >= "2.0.0"}
 ]
 

From 26b63ddad531e86645bce4c3b82dbb0fe05f2055 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 5 Nov 2023 21:12:10 +0100
Subject: [PATCH 2/2] port vard-log to build with Dune

---
 Makefile                                      | 103 ++----------------
 Makefile.coq.local                            |  28 -----
 Makefile.ml-files                             |   5 -
 _CoqProject                                   |   6 -
 extraction/vard-log/.merlin                   |   4 -
 .../vard-log/{coq => }/ExtractVarDRaftLog.v   |   2 +-
 .../vard-log/{ml => }/VarDLogArrangement.ml   |   0
 .../vard-log/{ml => }/VarDLogSerialization.ml |   1 -
 extraction/vard-log/dune                      |  24 ++++
 .../test/VarDSerializedSerializationTest.ml   |  28 -----
 extraction/vard-log/{ml => }/vardlog.ml       |   0
 extraction/vard/.merlin                       |   4 -
 {extraction => script}/vard-log/Makefile      |   0
 .../vard-log/bench/bench.py                   |   0
 {extraction => script}/vard-log/bench/etcd.py |   0
 .../vard-log/bench/experiment.py              |   0
 .../vard-log/bench/experiments/example.yml    |   0
 .../bench/experiments/ssd-etcd-throughput.yml |   0
 .../bench/experiments/ssd-vard-throughput.yml |   0
 .../vard-log/bench/experiments/vard.yml       |   0
 .../vard-log/bench/setup.py                   |   0
 {extraction => script}/vard-log/bench/vard.py |   0
 .../vard-log/bench/vard_open_loop.py          |   0
 .../vard-log/bench/vardctl.py                 |   0
 .../vard-log/run}/remove_module.pl            |   0
 .../scripts => script/vard-log/run}/run.sh    |   0
 .../vard-log/test/integration.py              |   0
 .../test => tests/vard-log}/OptsTest.ml       |   0
 tests/vard-log/VarDLogSerializationTest.ml    |  28 +++++
 .../vard-log/VarDLogTest.ml                   |   4 +-
 tests/vard-log/dune                           |   4 +
 vard-log.opam                                 |  10 +-
 32 files changed, 73 insertions(+), 178 deletions(-)
 delete mode 100644 Makefile.coq.local
 delete mode 100644 Makefile.ml-files
 delete mode 100644 extraction/vard-log/.merlin
 rename extraction/vard-log/{coq => }/ExtractVarDRaftLog.v (87%)
 rename extraction/vard-log/{ml => }/VarDLogArrangement.ml (100%)
 rename extraction/vard-log/{ml => }/VarDLogSerialization.ml (99%)
 create mode 100644 extraction/vard-log/dune
 delete mode 100644 extraction/vard-log/test/VarDSerializedSerializationTest.ml
 rename extraction/vard-log/{ml => }/vardlog.ml (100%)
 delete mode 100644 extraction/vard/.merlin
 rename {extraction => script}/vard-log/Makefile (100%)
 rename {extraction => script}/vard-log/bench/bench.py (100%)
 rename {extraction => script}/vard-log/bench/etcd.py (100%)
 rename {extraction => script}/vard-log/bench/experiment.py (100%)
 rename {extraction => script}/vard-log/bench/experiments/example.yml (100%)
 rename {extraction => script}/vard-log/bench/experiments/ssd-etcd-throughput.yml (100%)
 rename {extraction => script}/vard-log/bench/experiments/ssd-vard-throughput.yml (100%)
 rename {extraction => script}/vard-log/bench/experiments/vard.yml (100%)
 rename {extraction => script}/vard-log/bench/setup.py (100%)
 rename {extraction => script}/vard-log/bench/vard.py (100%)
 rename {extraction => script}/vard-log/bench/vard_open_loop.py (100%)
 rename {extraction => script}/vard-log/bench/vardctl.py (100%)
 rename {extraction/vard-log/scripts => script/vard-log/run}/remove_module.pl (100%)
 rename {extraction/vard-log/scripts => script/vard-log/run}/run.sh (100%)
 rename {extraction => script}/vard-log/test/integration.py (100%)
 rename {extraction/vard-log/test => tests/vard-log}/OptsTest.ml (100%)
 create mode 100644 tests/vard-log/VarDLogSerializationTest.ml
 rename extraction/vard-log/test/VarDSerializedTest.ml => tests/vard-log/VarDLogTest.ml (56%)
 create mode 100644 tests/vard-log/dune

diff --git a/Makefile b/Makefile
index ddf58619..ad909e53 100644
--- a/Makefile
+++ b/Makefile
@@ -1,99 +1,16 @@
-PYTHON=python2.7
-
-include Makefile.ml-files
-
-default: Makefile.coq
-	$(MAKE) -f Makefile.coq
-
-quick: Makefile.coq
-	$(MAKE) -f Makefile.coq quick
-
-vos: Makefile.coq
-	$(MAKE) -f Makefile.coq vos
-
-checkproofs: quick
-	$(MAKE) -f Makefile.coq checkproofs
-
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
-
-proofalytics:
-	$(MAKE) -C proofalytics clean
-	$(MAKE) -C proofalytics
-	$(MAKE) -C proofalytics publish
-
-STDBUF=$(shell [ -x "$$(which gstdbuf)" ] && echo "gstdbuf" || echo "stdbuf")
-BUILDTIMER=$(PWD)/proofalytics/build-timer.sh $(STDBUF) -i0 -o0
-
-proofalytics-aux: Makefile.coq
-	$(MAKE) -f Makefile.coq TIMECMD="$(BUILDTIMER)"
-
-Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
-
-theories/Raft/RaftState.v: theories/Raft/RaftState.v.rec
-	$(PYTHON) script/extract_record_notation.py theories/Raft/RaftState.v.rec raft_data > theories/Raft/RaftState.v
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
 clean: Makefile.coq
-	$(MAKE) -f Makefile.coq cleanall
-	rm -f Makefile.coq Makefile.coq.conf
-	find . -name '*.buildtime' -delete
-	$(MAKE) -C proofalytics clean
-	$(MAKE) -C extraction/vard clean
-	$(MAKE) -C extraction/vard-serialized clean
-	$(MAKE) -C extraction/vard-log clean
-	$(MAKE) -C extraction/vard-serialized-log clean
-	$(MAKE) -C extraction/vard-debug clean
-
-assumptions: Makefile.coq
-	$(MAKE) -f Makefile.coq script/assumptions.vo
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
-$(VARDML) $(VARDSERML) $(VARDLOGML) $(VARDSERLOGML) $(VARDDEBUGML): Makefile.coq
-	$(MAKE) -f Makefile.coq $@
-
-vard:
-	+$(MAKE) -C extraction/vard
-
-vard-test:
-	+$(MAKE) -C extraction/vard test
-
-vard-serialized:
-	+$(MAKE) -C extraction/vard-serialized
-
-vard-serialized-test:
-	+$(MAKE) -C extraction/vard-serialized test
-
-vard-log:
-	+$(MAKE) -C extraction/vard-log
-
-vard-log-test:
-	+$(MAKE) -C extraction/vard-log test
-
-vard-serialized-log:
-	+$(MAKE) -C extraction/vard-serialized-log
-
-vard-serialized-log-test:
-	+$(MAKE) -C extraction/vard-serialized-log test
-
-vard-debug:
-	+$(MAKE) -C extraction/vard-debug
-
-vard-debug-test:
-	+$(MAKE) -C extraction/vard-debug test
-
-lint:
-	@echo "Possible use of hypothesis names:"
-	find . -name '*.v' -exec grep -Hn 'H[0-9][0-9]*' {} \;
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-distclean: clean
-	rm -f _CoqProject
+force _CoqProject Makefile: ;
 
-.PHONY: default quick install clean lint proofalytics distclean checkproofs assumptions vos
-.PHONY: vard vard-test vard-serialized vard-serialized-test vard-log vard-log-test vard-serialized-log vard-serialized-log-test vard-debug vard-debug-test
-.PHONY: $(VARDML) $(VARDSERML) $(VARDLOGML) $(VARDSERLOGML) $(VARDDEBUGML)
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.NOTPARALLEL: $(VARDML)
-.NOTPARALLEL: $(VARDSERML)
-.NOTPARALLEL: $(VARDLOGML)
-.NOTPARALLEL: $(VARDSERLOGML)
-.NOTPARALLEL: $(VARDDEBUGML)
+.PHONY: all clean force
diff --git a/Makefile.coq.local b/Makefile.coq.local
deleted file mode 100644
index 58fd4fd6..00000000
--- a/Makefile.coq.local
+++ /dev/null
@@ -1,28 +0,0 @@
-include Makefile.ml-files
-
-script/assumptions.vo script/assumptions.glob script/assumptions.v.d: script/assumptions.v theories/RaftProofs/EndToEndLinearizability.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) script/assumptions.v
-
-$(VARDML): extraction/vard/coq/ExtractVarDRaft.v theories/Systems/VarDRaft.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard/coq/ExtractVarDRaft.v
-
-$(VARDSERML): extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v theories/Systems/VarDRaftSerialized.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v
-
-$(VARDLOGML): extraction/vard-log/coq/ExtractVarDRaftLog.v theories/Systems/VarDRaftLog.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-log/coq/ExtractVarDRaftLog.v
-
-$(VARDSERLOGML): extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v theories/Systems/VarDRaftSerializedLog.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v
-
-$(VARDDEBUGML): extraction/vard-debug/coq/ExtractVarDRaftDebug.v theories/Systems/VarDRaft.vo
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-debug/coq/ExtractVarDRaftDebug.v
-
-clean::
-	rm -f script/assumptions.vo script/assumptions.glob script/assumptions.v.d \
-	  script/.assumptions.vo.aux script/.assumptions.aux \
-	  $(VARDML) \
-	  $(VARDSERML) \
-	  $(VARDLOGML) \
-	  $(VARDSERLOGML) \
-	  $(VARDDEBUGML)
diff --git a/Makefile.ml-files b/Makefile.ml-files
deleted file mode 100644
index d256c127..00000000
--- a/Makefile.ml-files
+++ /dev/null
@@ -1,5 +0,0 @@
-VARDML = extraction/vard/ml/VarDRaft.ml extraction/vard/ml/VarDRaft.mli
-VARDSERML = extraction/vard-serialized/ml/VarDRaftSerialized.ml extraction/vard-serialized/ml/VarDRaftSerialized.mli
-VARDLOGML = extraction/vard-log/ml/VarDRaftLog.ml extraction/vard-log/ml/VarDRaftLog.mli
-VARDSERLOGML = extraction/vard-serialized-log/ml/VarDRaftSerializedLog.ml extraction/vard-serialized-log/ml/VarDRaftSerializedLog.mli
-VARDDEBUGML = extraction/vard-debug/ml/VarDRaftDebug.ml extraction/vard-debug/ml/VarDRaftDebug.mli
diff --git a/_CoqProject b/_CoqProject
index d975c0dc..9d809a2d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -210,9 +210,3 @@ theories/Systems/VarDRaftSerialized.v
 theories/Systems/VarDRaftSerializers.v
 theories/Systems/VarDRaftLog.v
 theories/Systems/VarDRaft.v
-
-extraction/vard/coq/ExtractVarDRaft.v
-extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v
-extraction/vard-log/coq/ExtractVarDRaftLog.v
-extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v
-extraction/vard-debug/coq/ExtractVarDRaftDebug.v
diff --git a/extraction/vard-log/.merlin b/extraction/vard-log/.merlin
deleted file mode 100644
index 1ca7a4ba..00000000
--- a/extraction/vard-log/.merlin
+++ /dev/null
@@ -1,4 +0,0 @@
-S ml
-S test
-B _build/**
-PKG verdi-runtime cheerios-runtime
diff --git a/extraction/vard-log/coq/ExtractVarDRaftLog.v b/extraction/vard-log/ExtractVarDRaftLog.v
similarity index 87%
rename from extraction/vard-log/coq/ExtractVarDRaftLog.v
rename to extraction/vard-log/ExtractVarDRaftLog.v
index 605bbc0e..2a2e4bf2 100644
--- a/extraction/vard-log/coq/ExtractVarDRaftLog.v
+++ b/extraction/vard-log/ExtractVarDRaftLog.v
@@ -7,5 +7,5 @@ From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt ExtrOcamlD
 From Cheerios Require Import ExtrOcamlCheeriosBasic ExtrOcamlCheeriosNatInt.
 From Cheerios Require Import ExtrOcamlCheeriosString ExtrOcamlCheeriosFinInt.
 
-Extraction "extraction/vard-log/ml/VarDRaftLog.ml" seq transformed_base_params
+Extraction "VarDRaftLog.ml" seq transformed_base_params
   transformed_multi_params transformed_failure_params.
diff --git a/extraction/vard-log/ml/VarDLogArrangement.ml b/extraction/vard-log/VarDLogArrangement.ml
similarity index 100%
rename from extraction/vard-log/ml/VarDLogArrangement.ml
rename to extraction/vard-log/VarDLogArrangement.ml
diff --git a/extraction/vard-log/ml/VarDLogSerialization.ml b/extraction/vard-log/VarDLogSerialization.ml
similarity index 99%
rename from extraction/vard-log/ml/VarDLogSerialization.ml
rename to extraction/vard-log/VarDLogSerialization.ml
index a5e0236b..88dc0d15 100644
--- a/extraction/vard-log/ml/VarDLogSerialization.ml
+++ b/extraction/vard-log/VarDLogSerialization.ml
@@ -1,7 +1,6 @@
 open Str
 open Printf
 open VarDRaftLog
-open VarD
 open Util
 
 let outputToString out =
diff --git a/extraction/vard-log/dune b/extraction/vard-log/dune
new file mode 100644
index 00000000..fbf95579
--- /dev/null
+++ b/extraction/vard-log/dune
@@ -0,0 +1,24 @@
+(library
+ (name VarDRaftLog)
+ (flags :standard -w -27-32-39-67)
+ (libraries verdi-runtime cheerios-runtime)
+ (modules VarDRaftLog))
+
+(library
+ (name VarDLogSerialization)
+ (libraries verdi-runtime VarDRaftLog)
+ (modules VarDLogSerialization))
+
+(coq.extraction
+ (prelude ExtractVarDRaftLog)
+ (extracted_modules VarDRaftLog)
+ (theories VerdiRaft)
+ (flags :standard -w -extraction-opaque-accessed))
+
+(executable
+ (name vardlog)
+ (public_name vardlog)
+ (libraries verdi-runtime VarDRaftLog VarDLogSerialization)
+ (flags :standard -w -27)
+ (modules vardlog VarDLogArrangement)
+ (package vard-log))
diff --git a/extraction/vard-log/test/VarDSerializedSerializationTest.ml b/extraction/vard-log/test/VarDSerializedSerializationTest.ml
deleted file mode 100644
index 7c870606..00000000
--- a/extraction/vard-log/test/VarDSerializedSerializationTest.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-open OUnit2
-open ListLabels
-open Util
-
-let tear_down () text_ctxt = ()
-
-let test_serialize_output_not_leader text_ctxt =
-  assert_equal (2, Bytes.of_string "NotLeader 15")
-    (VarDSerializedSerialization.serializeOutput (VarDRaftSerialized.NotLeader (2, 15)))
-
-let test_serialize_output_client_response test_ctxt =
-  let o = VarDRaftSerialized.Response (char_list_of_string "awesome", None, None) in
-  assert_equal (3, Bytes.of_string "Response 34 awesome - -")
-    (VarDSerializedSerialization.serializeOutput (VarDRaftSerialized.ClientResponse (3, 34, (Obj.magic o))))
-  
-let test_list =
-  [
-    "serialize NotLeader", test_serialize_output_not_leader;
-    "serialize ClientResponse", test_serialize_output_client_response
-  ]
-
-let tests =
-  "VarDSerializedSerialization" >:::
-    (map test_list ~f:(fun (name, test_fn) ->
-      name >:: (fun test_ctxt ->
-	bracket ignore tear_down test_ctxt;
-	test_fn test_ctxt)
-     ))
diff --git a/extraction/vard-log/ml/vardlog.ml b/extraction/vard-log/vardlog.ml
similarity index 100%
rename from extraction/vard-log/ml/vardlog.ml
rename to extraction/vard-log/vardlog.ml
diff --git a/extraction/vard/.merlin b/extraction/vard/.merlin
deleted file mode 100644
index c650f32a..00000000
--- a/extraction/vard/.merlin
+++ /dev/null
@@ -1,4 +0,0 @@
-S ml
-S test
-B _build/**
-PKG verdi-runtime
diff --git a/extraction/vard-log/Makefile b/script/vard-log/Makefile
similarity index 100%
rename from extraction/vard-log/Makefile
rename to script/vard-log/Makefile
diff --git a/extraction/vard-log/bench/bench.py b/script/vard-log/bench/bench.py
similarity index 100%
rename from extraction/vard-log/bench/bench.py
rename to script/vard-log/bench/bench.py
diff --git a/extraction/vard-log/bench/etcd.py b/script/vard-log/bench/etcd.py
similarity index 100%
rename from extraction/vard-log/bench/etcd.py
rename to script/vard-log/bench/etcd.py
diff --git a/extraction/vard-log/bench/experiment.py b/script/vard-log/bench/experiment.py
similarity index 100%
rename from extraction/vard-log/bench/experiment.py
rename to script/vard-log/bench/experiment.py
diff --git a/extraction/vard-log/bench/experiments/example.yml b/script/vard-log/bench/experiments/example.yml
similarity index 100%
rename from extraction/vard-log/bench/experiments/example.yml
rename to script/vard-log/bench/experiments/example.yml
diff --git a/extraction/vard-log/bench/experiments/ssd-etcd-throughput.yml b/script/vard-log/bench/experiments/ssd-etcd-throughput.yml
similarity index 100%
rename from extraction/vard-log/bench/experiments/ssd-etcd-throughput.yml
rename to script/vard-log/bench/experiments/ssd-etcd-throughput.yml
diff --git a/extraction/vard-log/bench/experiments/ssd-vard-throughput.yml b/script/vard-log/bench/experiments/ssd-vard-throughput.yml
similarity index 100%
rename from extraction/vard-log/bench/experiments/ssd-vard-throughput.yml
rename to script/vard-log/bench/experiments/ssd-vard-throughput.yml
diff --git a/extraction/vard-log/bench/experiments/vard.yml b/script/vard-log/bench/experiments/vard.yml
similarity index 100%
rename from extraction/vard-log/bench/experiments/vard.yml
rename to script/vard-log/bench/experiments/vard.yml
diff --git a/extraction/vard-log/bench/setup.py b/script/vard-log/bench/setup.py
similarity index 100%
rename from extraction/vard-log/bench/setup.py
rename to script/vard-log/bench/setup.py
diff --git a/extraction/vard-log/bench/vard.py b/script/vard-log/bench/vard.py
similarity index 100%
rename from extraction/vard-log/bench/vard.py
rename to script/vard-log/bench/vard.py
diff --git a/extraction/vard-log/bench/vard_open_loop.py b/script/vard-log/bench/vard_open_loop.py
similarity index 100%
rename from extraction/vard-log/bench/vard_open_loop.py
rename to script/vard-log/bench/vard_open_loop.py
diff --git a/extraction/vard-log/bench/vardctl.py b/script/vard-log/bench/vardctl.py
similarity index 100%
rename from extraction/vard-log/bench/vardctl.py
rename to script/vard-log/bench/vardctl.py
diff --git a/extraction/vard-log/scripts/remove_module.pl b/script/vard-log/run/remove_module.pl
similarity index 100%
rename from extraction/vard-log/scripts/remove_module.pl
rename to script/vard-log/run/remove_module.pl
diff --git a/extraction/vard-log/scripts/run.sh b/script/vard-log/run/run.sh
similarity index 100%
rename from extraction/vard-log/scripts/run.sh
rename to script/vard-log/run/run.sh
diff --git a/extraction/vard-log/test/integration.py b/script/vard-log/test/integration.py
similarity index 100%
rename from extraction/vard-log/test/integration.py
rename to script/vard-log/test/integration.py
diff --git a/extraction/vard-log/test/OptsTest.ml b/tests/vard-log/OptsTest.ml
similarity index 100%
rename from extraction/vard-log/test/OptsTest.ml
rename to tests/vard-log/OptsTest.ml
diff --git a/tests/vard-log/VarDLogSerializationTest.ml b/tests/vard-log/VarDLogSerializationTest.ml
new file mode 100644
index 00000000..1b06b466
--- /dev/null
+++ b/tests/vard-log/VarDLogSerializationTest.ml
@@ -0,0 +1,28 @@
+open OUnit2
+open ListLabels
+open Util
+
+let tear_down () text_ctxt = ()
+
+let test_serialize_output_not_leader text_ctxt =
+  assert_equal ("0aac4d743ccc4473a2e04f4072734722", Bytes.of_string "NotLeader 15")
+    (VarDLogSerialization.serializeOutput (VarDRaftLog.NotLeader (Obj.magic (char_list_of_string "0aac4d743ccc4473a2e04f4072734722"), 15)))
+
+let test_serialize_output_client_response test_ctxt =
+  let o = VarDRaftLog.Response (char_list_of_string "awesome", None, None) in
+  assert_equal ("0f5f33f091094d5db68a72e9f4cf9b14", Bytes.of_string "Response 34 awesome - -")
+    (VarDLogSerialization.serializeOutput (VarDRaftLog.ClientResponse (Obj.magic (char_list_of_string "0f5f33f091094d5db68a72e9f4cf9b14"), 34, (Obj.magic o))))
+
+let test_list =
+  [
+    "serialize NotLeader", test_serialize_output_not_leader;
+    "serialize ClientResponse", test_serialize_output_client_response
+  ]
+
+let tests =
+  "VarDLogSerialization" >:::
+    (map test_list ~f:(fun (name, test_fn) ->
+      name >:: (fun test_ctxt ->
+	bracket ignore tear_down test_ctxt;
+	test_fn test_ctxt)
+     ))
diff --git a/extraction/vard-log/test/VarDSerializedTest.ml b/tests/vard-log/VarDLogTest.ml
similarity index 56%
rename from extraction/vard-log/test/VarDSerializedTest.ml
rename to tests/vard-log/VarDLogTest.ml
index be675f8e..907494c4 100644
--- a/extraction/vard-log/test/VarDSerializedTest.ml
+++ b/tests/vard-log/VarDLogTest.ml
@@ -3,8 +3,8 @@ open OUnit2
 let () =
   run_test_tt_main 
     ~exit
-    ("VarD" >:::
+    ("VarDLog" >:::
 	[
           OptsTest.tests;
-          VarDSerializedSerializationTest.tests
+          VarDLogSerializationTest.tests
 	])
diff --git a/tests/vard-log/dune b/tests/vard-log/dune
new file mode 100644
index 00000000..cfdd8640
--- /dev/null
+++ b/tests/vard-log/dune
@@ -0,0 +1,4 @@
+(test
+ (name VarDLogTest)
+ (flags :standard -w -27)
+ (libraries verdi-runtime VarDLogSerialization VarDRaftLog ounit2))
diff --git a/vard-log.opam b/vard-log.opam
index 348b788e..dc841f71 100644
--- a/vard-log.opam
+++ b/vard-log.opam
@@ -8,17 +8,15 @@ bug-reports: "https://github.com/uwplse/verdi-raft/issues"
 license: "BSD-2-Clause"
 synopsis: "Fault-tolerant distributed key-value store using a verified implementation of Raft consensus"
 
-build: [make "-j%{jobs}%" "vard-log"]
+build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "ocaml" {>= "4.05.0"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.14"}
-  "coq-verdi" {= "dev"}
-  "coq-struct-tact" {= "dev"}
-  "coq-cheerios" {= "dev"}
+  "coq-verdi-raft" {= "dev"}
   "verdi-runtime" {= "dev"}
-  "ocamlbuild" {build}
-  "ounit" {with-test & >= "2.0.0"}
   "cheerios-runtime" {= "dev"}
+  "ounit" {with-test & >= "2.0.0"}
 ]
 
 authors: [