uwplse · palmskog · Nov 5, 2023 · Nov 5, 2023
diff --git a/.gitignore b/.gitignore
@@ -2,6 +2,7 @@
 *.glob
 *.v.d
 *.buildtime
+_build
 Makefile.coq
 Makefile.coq.bak
 Makefile.coq.conf

diff --git 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
diff --git a/Makefile.ml-files b/Makefile.ml-files
diff --git 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
diff --git a/extraction/vard-log/coq/ExtractVarDRaftLog.v → extraction/vard-log/ExtractVarDRaftLog.v b/extraction/vard-log/coq/ExtractVarDRaftLog.v → 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 → extraction/vard-log/VarDLogArrangement.ml b/extraction/vard-log/ml/VarDLogArrangement.ml → extraction/vard-log/VarDLogArrangement.ml
diff --git a/...ction/vard-log/ml/VarDLogSerialization.ml → extraction/vard-log/VarDLogSerialization.ml b/...ction/vard-log/ml/VarDLogSerialization.ml → 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
@@ -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
diff --git a/extraction/vard-log/ml/vardlog.ml → extraction/vard-log/vardlog.ml b/extraction/vard-log/ml/vardlog.ml → extraction/vard-log/vardlog.ml
diff --git a/extraction/vard/.merlin b/extraction/vard/.merlin
diff --git a/extraction/vard/coq/ExtractVarDRaft.v → extraction/vard/ExtractVarDRaft.v b/extraction/vard/coq/ExtractVarDRaft.v → 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 → extraction/vard/VarDArrangement.ml b/extraction/vard/ml/VarDArrangement.ml → 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 → extraction/vard/VarDSerialization.ml b/extraction/vard/ml/VarDSerialization.ml → 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
@@ -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
diff --git a/extraction/vard/ml/vard.ml → extraction/vard/vard.ml b/extraction/vard/ml/vard.ml → 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
diff --git a/extraction/vard-log/Makefile → script/vard-log/Makefile b/extraction/vard-log/Makefile → script/vard-log/Makefile
diff --git a/extraction/vard-log/bench/bench.py → script/vard-log/bench/bench.py b/extraction/vard-log/bench/bench.py → script/vard-log/bench/bench.py
diff --git a/extraction/vard-log/bench/etcd.py → script/vard-log/bench/etcd.py b/extraction/vard-log/bench/etcd.py → script/vard-log/bench/etcd.py
diff --git a/extraction/vard-log/bench/experiment.py → script/vard-log/bench/experiment.py b/extraction/vard-log/bench/experiment.py → script/vard-log/bench/experiment.py
diff --git a/...on/vard-log/bench/experiments/example.yml → ...pt/vard-log/bench/experiments/example.yml b/...on/vard-log/bench/experiments/example.yml → ...pt/vard-log/bench/experiments/example.yml
diff --git a/...bench/experiments/ssd-etcd-throughput.yml → ...bench/experiments/ssd-etcd-throughput.yml b/...bench/experiments/ssd-etcd-throughput.yml → ...bench/experiments/ssd-etcd-throughput.yml
diff --git a/...bench/experiments/ssd-vard-throughput.yml → ...bench/experiments/ssd-vard-throughput.yml b/...bench/experiments/ssd-vard-throughput.yml → ...bench/experiments/ssd-vard-throughput.yml
diff --git a/...ction/vard-log/bench/experiments/vard.yml → script/vard-log/bench/experiments/vard.yml b/...ction/vard-log/bench/experiments/vard.yml → script/vard-log/bench/experiments/vard.yml
diff --git a/extraction/vard-log/bench/setup.py → script/vard-log/bench/setup.py b/extraction/vard-log/bench/setup.py → script/vard-log/bench/setup.py
diff --git a/extraction/vard-log/bench/vard.py → script/vard-log/bench/vard.py b/extraction/vard-log/bench/vard.py → script/vard-log/bench/vard.py
diff --git a/extraction/vard-log/bench/vard_open_loop.py → script/vard-log/bench/vard_open_loop.py b/extraction/vard-log/bench/vard_open_loop.py → script/vard-log/bench/vard_open_loop.py
diff --git a/extraction/vard-log/bench/vardctl.py → script/vard-log/bench/vardctl.py b/extraction/vard-log/bench/vardctl.py → script/vard-log/bench/vardctl.py
diff --git a/extraction/vard-log/scripts/remove_module.pl → script/vard-log/run/remove_module.pl b/extraction/vard-log/scripts/remove_module.pl → script/vard-log/run/remove_module.pl
diff --git a/extraction/vard-log/scripts/run.sh → script/vard-log/run/run.sh b/extraction/vard-log/scripts/run.sh → script/vard-log/run/run.sh
diff --git a/extraction/vard-log/test/integration.py → script/vard-log/test/integration.py b/extraction/vard-log/test/integration.py → script/vard-log/test/integration.py
diff --git a/extraction/vard/Makefile → script/vard/Makefile b/extraction/vard/Makefile → script/vard/Makefile
diff --git a/extraction/vard/bench/bench.py → script/vard/bench/bench.py b/extraction/vard/bench/bench.py → script/vard/bench/bench.py
diff --git a/extraction/vard/bench/etcd.py → script/vard/bench/etcd.py b/extraction/vard/bench/etcd.py → script/vard/bench/etcd.py
diff --git a/extraction/vard/bench/etcd.txt → script/vard/bench/etcd.txt b/extraction/vard/bench/etcd.txt → script/vard/bench/etcd.txt
diff --git a/extraction/vard/bench/experiment.py → script/vard/bench/experiment.py b/extraction/vard/bench/experiment.py → script/vard/bench/experiment.py
diff --git a/...action/vard/bench/experiments/example.yml → script/vard/bench/experiments/example.yml b/...action/vard/bench/experiments/example.yml → script/vard/bench/experiments/example.yml
diff --git a/...bench/experiments/ssd-etcd-throughput.yml → ...bench/experiments/ssd-etcd-throughput.yml b/...bench/experiments/ssd-etcd-throughput.yml → ...bench/experiments/ssd-etcd-throughput.yml
diff --git a/...bench/experiments/ssd-vard-throughput.yml → ...bench/experiments/ssd-vard-throughput.yml b/...bench/experiments/ssd-vard-throughput.yml → ...bench/experiments/ssd-vard-throughput.yml
diff --git a/extraction/vard/bench/experiments/vard.yml → script/vard/bench/experiments/vard.yml b/extraction/vard/bench/experiments/vard.yml → script/vard/bench/experiments/vard.yml
diff --git a/extraction/vard/bench/setup.py → script/vard/bench/setup.py b/extraction/vard/bench/setup.py → script/vard/bench/setup.py
diff --git a/extraction/vard/bench/vard.py → script/vard/bench/vard.py b/extraction/vard/bench/vard.py → script/vard/bench/vard.py
diff --git a/extraction/vard/bench/vard.txt → script/vard/bench/vard.txt b/extraction/vard/bench/vard.txt → script/vard/bench/vard.txt
diff --git a/extraction/vard/bench/vard_open_loop.py → script/vard/bench/vard_open_loop.py b/extraction/vard/bench/vard_open_loop.py → script/vard/bench/vard_open_loop.py
diff --git a/extraction/vard/bench/vardctl.py → script/vard/bench/vardctl.py b/extraction/vard/bench/vardctl.py → script/vard/bench/vardctl.py
diff --git a/extraction/vard/scripts/bench-etcd.sh → script/vard/run/bench-etcd.sh b/extraction/vard/scripts/bench-etcd.sh → script/vard/run/bench-etcd.sh
diff --git a/extraction/vard/scripts/bench-vard.sh → script/vard/run/bench-vard.sh b/extraction/vard/scripts/bench-vard.sh → script/vard/run/bench-vard.sh
diff --git a/extraction/vard/scripts/clear-etcd.sh → script/vard/run/clear-etcd.sh b/extraction/vard/scripts/clear-etcd.sh → script/vard/run/clear-etcd.sh
diff --git a/extraction/vard/scripts/clear-vard.sh → script/vard/run/clear-vard.sh b/extraction/vard/scripts/clear-vard.sh → script/vard/run/clear-vard.sh
diff --git a/extraction/vard/scripts/run.sh → script/vard/run/run.sh b/extraction/vard/scripts/run.sh → script/vard/run/run.sh
diff --git a/extraction/vard/scripts/start-node.sh → script/vard/run/start-node.sh b/extraction/vard/scripts/start-node.sh → script/vard/run/start-node.sh
diff --git a/extraction/vard/scripts/start-tmux-debug.sh → script/vard/run/start-tmux-debug.sh b/extraction/vard/scripts/start-tmux-debug.sh → script/vard/run/start-tmux-debug.sh
diff --git a/extraction/vard/scripts/start-tmux.sh → script/vard/run/start-tmux.sh b/extraction/vard/scripts/start-tmux.sh → script/vard/run/start-tmux.sh
diff --git a/extraction/vard/test/integration.py → script/vard/test/integration.py b/extraction/vard/test/integration.py → script/vard/test/integration.py
diff --git a/extraction/vard-log/test/OptsTest.ml → tests/vard-log/OptsTest.ml b/extraction/vard-log/test/OptsTest.ml → tests/vard-log/OptsTest.ml