Merge pull request #101 from uwplse/theories-dune

reorganize files under standard theories directory

Makefile

@@ -31,8 +31,8 @@ proofalytics-aux: Makefile.coq
 Makefile.coq: _CoqProject
 	coq_makefile -f _CoqProject -o Makefile.coq
 
-raft/RaftState.v: raft/RaftState.v.rec
-	$(PYTHON) script/extract_record_notation.py raft/RaftState.v.rec raft_data > raft/RaftState.v
+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
 
 clean: Makefile.coq
 	$(MAKE) -f Makefile.coq cleanall

Makefile.coq.local

@@ -1,21 +1,21 @@
 include Makefile.ml-files
 
-script/assumptions.vo script/assumptions.glob script/assumptions.v.d: script/assumptions.v raft-proofs/EndToEndLinearizability.vo
+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 systems/VarDRaft.vo
+$(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 systems/VarDRaftSerialized.vo
+$(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 systems/VarDRaftLog.vo
+$(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 systems/VarDRaftSerializedLog.vo
+$(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 systems/VarDRaft.vo
+$(VARDDEBUGML): extraction/vard-debug/coq/ExtractVarDRaftDebug.v theories/Systems/VarDRaft.vo
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) extraction/vard-debug/coq/ExtractVarDRaftDebug.v
 
 clean::

README.md

@@ -75,9 +75,9 @@ compiled without checking any proofs.
 
 ## Files
 
-The `raft` and `raft-proofs` subdirectories contain the implementation and
-verification of Raft. For each proof interface file in `raft`, there is a 
-corresponding proof file in `raft-proofs`. The files in the `raft` 
+The `Raft` and `RaftProofs` subdirectories of `theories` contain the implementation
+and verification of Raft. For each proof interface file in `Raft`, there is a
+corresponding proof file in `RaftProofs`. The files in the `Raft`
 subdirectory include:
 
 - `Raft.v`: an implementation of Raft in Verdi
@@ -87,16 +87,16 @@ subdirectory include:
 - `CommonTheorems.v`: several useful theorems about functions used by
   the Raft implementation
 - `OneLeaderPerTermInterface`: a statement of Raft's *election
-  safety* property. See also the corresponding proof file in `raft-proofs`.
+  safety* property. See also the corresponding proof file in `RaftProofs`.
     - `CandidatesVoteForSelvesInterface.v`, `VotesCorrectInterface.v`, and
       `CroniesCorrectInterface.v`: statements of properties used by the proof
       `OneLeaderPerTermProof.v`
 - `LogMatchingInterface.v`: a statement of Raft's *log matching*
-    property. See also `LogMatchingProof.v` in `raft-proofs`
+    property. See also `LogMatchingProof.v` in `RaftProofs`
     - `LeaderSublogInterface.v`, `SortedInterface.v`, and `UniqueIndicesInterface.v`: statements
       of properties used by `LogMatchingProof.v`
 
-The file `EndToEndLinearizability.v` in `raft-proofs` uses the proofs of
+The file `EndToEndLinearizability.v` in `RaftProofs` uses the proofs of
 all proof interfaces to show Raft's *linearizability* property.
 
 ## The `vard` Key-Value Store