Merge pull request #143 from uwplse/theories-dir

reorganize files under standard theories directory
uwplse · Oct 21, 2023 · 44aacdc · 44aacdc
2 parents bfb44e8 + 19cad66
commit 44aacdc
Show file tree

Hide file tree

Showing 46 changed files with 60 additions and 190 deletions.
diff --git a/Makefile b/Makefile
@@ -1,24 +1,16 @@
-default: Makefile.coq
-	$(MAKE) -f Makefile.coq
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
-quick: Makefile.coq
-	$(MAKE) -f Makefile.coq quick
-
-install: Makefile.coq
-	$(MAKE) -f Makefile.coq install
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
-
-clean: Makefile.coq
-	$(MAKE) -f Makefile.coq cleanall
-	rm -f Makefile.coq Makefile.coq.conf
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-lint:
-	@echo "Possible use of hypothesis names:"
-	find . -name '*.v' -exec grep -Hn 'H[0-9][0-9]*' {} \;
+force _CoqProject Makefile: ;
 
-distclean: clean
-	rm -f _CoqProject
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
 
-.PHONY: default quick clean lint distclean install
+.PHONY: all clean force
diff --git a/_CoqProject b/_CoqProject
@@ -1,48 +1,45 @@
--Q core Verdi
--Q lib Verdi
--Q systems Verdi
--Q extraction Verdi
+-Q theories Verdi
 
-core/NameOverlay.v
-core/DynamicNetLemmas.v
-core/Net.v
-core/HandlerMonad.v
-core/Verdi.v
-core/StateMachineHandlerMonad.v
-core/InverseTraceRelations.v
-core/SingleSimulations.v
-core/PartialMapSimulations.v
-core/TotalMapExecutionSimulations.v
-core/VerdiHints.v
-core/DupDropReordering.v
-core/PartialMapExecutionSimulations.v
-core/GhostSimulations.v
-core/StatePacketPacketDecomposition.v
-core/TraceRelations.v
-core/LabeledNet.v
-core/TotalMapSimulations.v
-core/PartialExtendedMapSimulations.v
+theories/Core/NameOverlay.v
+theories/Core/DynamicNetLemmas.v
+theories/Core/Net.v
+theories/Core/HandlerMonad.v
+theories/Core/Verdi.v
+theories/Core/StateMachineHandlerMonad.v
+theories/Core/InverseTraceRelations.v
+theories/Core/SingleSimulations.v
+theories/Core/PartialMapSimulations.v
+theories/Core/TotalMapExecutionSimulations.v
+theories/Core/VerdiHints.v
+theories/Core/DupDropReordering.v
+theories/Core/PartialMapExecutionSimulations.v
+theories/Core/GhostSimulations.v
+theories/Core/StatePacketPacketDecomposition.v
+theories/Core/TraceRelations.v
+theories/Core/LabeledNet.v
+theories/Core/TotalMapSimulations.v
+theories/Core/PartialExtendedMapSimulations.v
 
-lib/Ssrexport.v
-lib/FMapVeryWeak.v
+theories/Lib/Ssrexport.v
+theories/Lib/FMapVeryWeak.v
 
-systems/Counter.v
-systems/SerializedMsgParams.v
-systems/PrimaryBackup.v
-systems/SerializedMsgParamsCorrect.v
-systems/LockServSeqNum.v
-systems/VarDPrimaryBackup.v
-systems/VarD.v
-systems/SeqNum.v
-systems/LiveLockServ.v
-systems/SeqNumCorrect.v
-systems/LockServ.v
-systems/Log.v
-systems/LogCorrect.v
+theories/Systems/Counter.v
+theories/Systems/SerializedMsgParams.v
+theories/Systems/PrimaryBackup.v
+theories/Systems/SerializedMsgParamsCorrect.v
+theories/Systems/LockServSeqNum.v
+theories/Systems/VarDPrimaryBackup.v
+theories/Systems/VarD.v
+theories/Systems/SeqNum.v
+theories/Systems/LiveLockServ.v
+theories/Systems/SeqNumCorrect.v
+theories/Systems/LockServ.v
+theories/Systems/Log.v
+theories/Systems/LogCorrect.v
 
-extraction/ExtrOcamlFinInt.v
-extraction/ExtrOcamlNatIntExt.v
-extraction/ExtrOcamlDiskOp.v
-extraction/ExtrOcamlBasicExt.v
-extraction/ExtrOcamlBool.v
-extraction/ExtrOcamlList.v
+theories/Extraction/ExtrOcamlFinInt.v
+theories/Extraction/ExtrOcamlNatIntExt.v
+theories/Extraction/ExtrOcamlDiskOp.v
+theories/Extraction/ExtrOcamlBasicExt.v
+theories/Extraction/ExtrOcamlBool.v
+theories/Extraction/ExtrOcamlList.v
diff --git a/dune-project b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 3.5)
+(using coq 0.6)
+(name verdi)
diff --git a/script/checkpaths.sh b/script/checkpaths.sh
diff --git a/script/coqproject.sh b/script/coqproject.sh
diff --git a/core/DupDropReordering.v → theories/Core/DupDropReordering.v b/core/DupDropReordering.v → theories/Core/DupDropReordering.v
diff --git a/core/DynamicNetLemmas.v → theories/Core/DynamicNetLemmas.v b/core/DynamicNetLemmas.v → theories/Core/DynamicNetLemmas.v
diff --git a/core/GhostSimulations.v → theories/Core/GhostSimulations.v b/core/GhostSimulations.v → theories/Core/GhostSimulations.v
diff --git a/core/HandlerMonad.v → theories/Core/HandlerMonad.v b/core/HandlerMonad.v → theories/Core/HandlerMonad.v
diff --git a/core/InverseTraceRelations.v → theories/Core/InverseTraceRelations.v b/core/InverseTraceRelations.v → theories/Core/InverseTraceRelations.v
diff --git a/core/LabeledNet.v → theories/Core/LabeledNet.v b/core/LabeledNet.v → theories/Core/LabeledNet.v
diff --git a/core/NameOverlay.v → theories/Core/NameOverlay.v b/core/NameOverlay.v → theories/Core/NameOverlay.v
diff --git a/core/Net.v → theories/Core/Net.v b/core/Net.v → theories/Core/Net.v
diff --git a/core/PartialExtendedMapSimulations.v → ...ries/Core/PartialExtendedMapSimulations.v b/core/PartialExtendedMapSimulations.v → ...ries/Core/PartialExtendedMapSimulations.v
diff --git a/core/PartialMapExecutionSimulations.v → ...ies/Core/PartialMapExecutionSimulations.v b/core/PartialMapExecutionSimulations.v → ...ies/Core/PartialMapExecutionSimulations.v
diff --git a/core/PartialMapSimulations.v → theories/Core/PartialMapSimulations.v b/core/PartialMapSimulations.v → theories/Core/PartialMapSimulations.v
diff --git a/core/SingleSimulations.v → theories/Core/SingleSimulations.v b/core/SingleSimulations.v → theories/Core/SingleSimulations.v
diff --git a/core/StateMachineHandlerMonad.v → theories/Core/StateMachineHandlerMonad.v b/core/StateMachineHandlerMonad.v → theories/Core/StateMachineHandlerMonad.v
diff --git a/core/StatePacketPacketDecomposition.v → ...ies/Core/StatePacketPacketDecomposition.v b/core/StatePacketPacketDecomposition.v → ...ies/Core/StatePacketPacketDecomposition.v
diff --git a/core/TotalMapExecutionSimulations.v → theories/Core/TotalMapExecutionSimulations.v b/core/TotalMapExecutionSimulations.v → theories/Core/TotalMapExecutionSimulations.v
diff --git a/core/TotalMapSimulations.v → theories/Core/TotalMapSimulations.v b/core/TotalMapSimulations.v → theories/Core/TotalMapSimulations.v
diff --git a/core/TraceRelations.v → theories/Core/TraceRelations.v b/core/TraceRelations.v → theories/Core/TraceRelations.v
diff --git a/core/Verdi.v → theories/Core/Verdi.v b/core/Verdi.v → theories/Core/Verdi.v
diff --git a/core/VerdiHints.v → theories/Core/VerdiHints.v b/core/VerdiHints.v → theories/Core/VerdiHints.v
diff --git a/extraction/ExtrOcamlBasicExt.v → theories/Extraction/ExtrOcamlBasicExt.v b/extraction/ExtrOcamlBasicExt.v → theories/Extraction/ExtrOcamlBasicExt.v
diff --git a/extraction/ExtrOcamlBool.v → theories/Extraction/ExtrOcamlBool.v b/extraction/ExtrOcamlBool.v → theories/Extraction/ExtrOcamlBool.v
diff --git a/extraction/ExtrOcamlDiskOp.v → theories/Extraction/ExtrOcamlDiskOp.v b/extraction/ExtrOcamlDiskOp.v → theories/Extraction/ExtrOcamlDiskOp.v
diff --git a/extraction/ExtrOcamlFinInt.v → theories/Extraction/ExtrOcamlFinInt.v b/extraction/ExtrOcamlFinInt.v → theories/Extraction/ExtrOcamlFinInt.v
diff --git a/extraction/ExtrOcamlList.v → theories/Extraction/ExtrOcamlList.v b/extraction/ExtrOcamlList.v → theories/Extraction/ExtrOcamlList.v
diff --git a/extraction/ExtrOcamlNatIntExt.v → theories/Extraction/ExtrOcamlNatIntExt.v b/extraction/ExtrOcamlNatIntExt.v → theories/Extraction/ExtrOcamlNatIntExt.v
diff --git a/lib/FMapVeryWeak.v → theories/Lib/FMapVeryWeak.v b/lib/FMapVeryWeak.v → theories/Lib/FMapVeryWeak.v
diff --git a/lib/Ssrexport.v → theories/Lib/Ssrexport.v b/lib/Ssrexport.v → theories/Lib/Ssrexport.v
diff --git a/systems/Counter.v → theories/Systems/Counter.v b/systems/Counter.v → theories/Systems/Counter.v
diff --git a/systems/LiveLockServ.v → theories/Systems/LiveLockServ.v b/systems/LiveLockServ.v → theories/Systems/LiveLockServ.v
diff --git a/systems/LockServ.v → theories/Systems/LockServ.v b/systems/LockServ.v → theories/Systems/LockServ.v
diff --git a/systems/LockServSeqNum.v → theories/Systems/LockServSeqNum.v b/systems/LockServSeqNum.v → theories/Systems/LockServSeqNum.v
diff --git a/systems/Log.v → theories/Systems/Log.v b/systems/Log.v → theories/Systems/Log.v
diff --git a/systems/LogCorrect.v → theories/Systems/LogCorrect.v b/systems/LogCorrect.v → theories/Systems/LogCorrect.v
diff --git a/systems/PrimaryBackup.v → theories/Systems/PrimaryBackup.v b/systems/PrimaryBackup.v → theories/Systems/PrimaryBackup.v
diff --git a/systems/SeqNum.v → theories/Systems/SeqNum.v b/systems/SeqNum.v → theories/Systems/SeqNum.v
diff --git a/systems/SeqNumCorrect.v → theories/Systems/SeqNumCorrect.v b/systems/SeqNumCorrect.v → theories/Systems/SeqNumCorrect.v
diff --git a/systems/SerializedMsgParams.v → theories/Systems/SerializedMsgParams.v b/systems/SerializedMsgParams.v → theories/Systems/SerializedMsgParams.v
diff --git a/systems/SerializedMsgParamsCorrect.v → ...ries/Systems/SerializedMsgParamsCorrect.v b/systems/SerializedMsgParamsCorrect.v → ...ries/Systems/SerializedMsgParamsCorrect.v
diff --git a/systems/VarD.v → theories/Systems/VarD.v b/systems/VarD.v → theories/Systems/VarD.v
diff --git a/systems/VarDPrimaryBackup.v → theories/Systems/VarDPrimaryBackup.v b/systems/VarDPrimaryBackup.v → theories/Systems/VarDPrimaryBackup.v
diff --git a/theories/dune b/theories/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name Verdi)
+ (package coq-verdi)
+ (synopsis "Framework for verification of implementations of distributed systems in Coq"))
+
+(include_subdirs qualified)