From 19cad6602bf59d3df551cc010b3b1048b5fbd9b2 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 21 Oct 2023 17:42:16 +0200 Subject: [PATCH] reorganize files under standard theories directory, use standard Makefile and Dune builds --- Makefile | 28 +++--- _CoqProject | 85 +++++++++--------- dune-project | 3 + script/checkpaths.sh | 39 -------- script/coqproject.sh | 89 ------------------- {core => theories/Core}/DupDropReordering.v | 0 {core => theories/Core}/DynamicNetLemmas.v | 0 {core => theories/Core}/GhostSimulations.v | 0 {core => theories/Core}/HandlerMonad.v | 0 .../Core}/InverseTraceRelations.v | 0 {core => theories/Core}/LabeledNet.v | 0 {core => theories/Core}/NameOverlay.v | 0 {core => theories/Core}/Net.v | 0 .../Core}/PartialExtendedMapSimulations.v | 0 .../Core}/PartialMapExecutionSimulations.v | 0 .../Core}/PartialMapSimulations.v | 0 {core => theories/Core}/SingleSimulations.v | 0 .../Core}/StateMachineHandlerMonad.v | 0 .../Core}/StatePacketPacketDecomposition.v | 0 .../Core}/TotalMapExecutionSimulations.v | 0 {core => theories/Core}/TotalMapSimulations.v | 0 {core => theories/Core}/TraceRelations.v | 0 {core => theories/Core}/Verdi.v | 0 {core => theories/Core}/VerdiHints.v | 0 .../Extraction}/ExtrOcamlBasicExt.v | 0 .../Extraction}/ExtrOcamlBool.v | 0 .../Extraction}/ExtrOcamlDiskOp.v | 0 .../Extraction}/ExtrOcamlFinInt.v | 0 .../Extraction}/ExtrOcamlList.v | 0 .../Extraction}/ExtrOcamlNatIntExt.v | 0 {lib => theories/Lib}/FMapVeryWeak.v | 0 {lib => theories/Lib}/Ssrexport.v | 0 {systems => theories/Systems}/Counter.v | 0 {systems => theories/Systems}/LiveLockServ.v | 0 {systems => theories/Systems}/LockServ.v | 0 .../Systems}/LockServSeqNum.v | 0 {systems => theories/Systems}/Log.v | 0 {systems => theories/Systems}/LogCorrect.v | 0 {systems => theories/Systems}/PrimaryBackup.v | 0 {systems => theories/Systems}/SeqNum.v | 0 {systems => theories/Systems}/SeqNumCorrect.v | 0 .../Systems}/SerializedMsgParams.v | 0 .../Systems}/SerializedMsgParamsCorrect.v | 0 {systems => theories/Systems}/VarD.v | 0 .../Systems}/VarDPrimaryBackup.v | 0 theories/dune | 6 ++ 46 files changed, 60 insertions(+), 190 deletions(-) create mode 100644 dune-project delete mode 100755 script/checkpaths.sh delete mode 100755 script/coqproject.sh rename {core => theories/Core}/DupDropReordering.v (100%) rename {core => theories/Core}/DynamicNetLemmas.v (100%) rename {core => theories/Core}/GhostSimulations.v (100%) rename {core => theories/Core}/HandlerMonad.v (100%) rename {core => theories/Core}/InverseTraceRelations.v (100%) rename {core => theories/Core}/LabeledNet.v (100%) rename {core => theories/Core}/NameOverlay.v (100%) rename {core => theories/Core}/Net.v (100%) rename {core => theories/Core}/PartialExtendedMapSimulations.v (100%) rename {core => theories/Core}/PartialMapExecutionSimulations.v (100%) rename {core => theories/Core}/PartialMapSimulations.v (100%) rename {core => theories/Core}/SingleSimulations.v (100%) rename {core => theories/Core}/StateMachineHandlerMonad.v (100%) rename {core => theories/Core}/StatePacketPacketDecomposition.v (100%) rename {core => theories/Core}/TotalMapExecutionSimulations.v (100%) rename {core => theories/Core}/TotalMapSimulations.v (100%) rename {core => theories/Core}/TraceRelations.v (100%) rename {core => theories/Core}/Verdi.v (100%) rename {core => theories/Core}/VerdiHints.v (100%) rename {extraction => theories/Extraction}/ExtrOcamlBasicExt.v (100%) rename {extraction => theories/Extraction}/ExtrOcamlBool.v (100%) rename {extraction => theories/Extraction}/ExtrOcamlDiskOp.v (100%) rename {extraction => theories/Extraction}/ExtrOcamlFinInt.v (100%) rename {extraction => theories/Extraction}/ExtrOcamlList.v (100%) rename {extraction => theories/Extraction}/ExtrOcamlNatIntExt.v (100%) rename {lib => theories/Lib}/FMapVeryWeak.v (100%) rename {lib => theories/Lib}/Ssrexport.v (100%) rename {systems => theories/Systems}/Counter.v (100%) rename {systems => theories/Systems}/LiveLockServ.v (100%) rename {systems => theories/Systems}/LockServ.v (100%) rename {systems => theories/Systems}/LockServSeqNum.v (100%) rename {systems => theories/Systems}/Log.v (100%) rename {systems => theories/Systems}/LogCorrect.v (100%) rename {systems => theories/Systems}/PrimaryBackup.v (100%) rename {systems => theories/Systems}/SeqNum.v (100%) rename {systems => theories/Systems}/SeqNumCorrect.v (100%) rename {systems => theories/Systems}/SerializedMsgParams.v (100%) rename {systems => theories/Systems}/SerializedMsgParamsCorrect.v (100%) rename {systems => theories/Systems}/VarD.v (100%) rename {systems => theories/Systems}/VarDPrimaryBackup.v (100%) create mode 100644 theories/dune diff --git a/Makefile b/Makefile index 77cf63c2..ad909e53 100644 --- 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 index 5bb4eec4..91d40f5d 100644 --- 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 new file mode 100644 index 00000000..1182f1f2 --- /dev/null +++ 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 deleted file mode 100755 index b6e5e2f1..00000000 --- a/script/checkpaths.sh +++ /dev/null @@ -1,39 +0,0 @@ -#!/usr/bin/env bash - -set -e - -if ! [ -f _CoqProject ]; then - exit 0 -fi - -if [ "${TRAVIS}x" != "x" ]; then - exit 0 -fi - - -grep '\.v' _CoqProject | sort > build.files -find . -name '*.v' | sed 's!^\./!!' | sort > files - -comm -23 files build.files > files.missing.from.build -comm -13 files build.files > nonexistant.build.files - -EXIT_CODE=0 - -if [ -s files.missing.from.build ] -then - echo 'The following files are present but missing from Makefile.coq.' - echo 'Perhaps you have added a new file and should rerun ./configure?' - cat files.missing.from.build - EXIT_CODE=1 -fi - -if [ -s nonexistant.build.files ] -then - echo 'The following files are present in Makefile.coq but to not exist.' - echo 'Perhaps you have deleted a file and should rerun ./configure?' - cat nonexistant.build.files - EXIT_CODE=1 -fi - -rm -f files build.files files.missing.from.build nonexistant.build.files -exit $EXIT_CODE 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/core/DupDropReordering.v b/theories/Core/DupDropReordering.v similarity index 100% rename from core/DupDropReordering.v rename to theories/Core/DupDropReordering.v diff --git a/core/DynamicNetLemmas.v b/theories/Core/DynamicNetLemmas.v similarity index 100% rename from core/DynamicNetLemmas.v rename to theories/Core/DynamicNetLemmas.v diff --git a/core/GhostSimulations.v b/theories/Core/GhostSimulations.v similarity index 100% rename from core/GhostSimulations.v rename to theories/Core/GhostSimulations.v diff --git a/core/HandlerMonad.v b/theories/Core/HandlerMonad.v similarity index 100% rename from core/HandlerMonad.v rename to theories/Core/HandlerMonad.v diff --git a/core/InverseTraceRelations.v b/theories/Core/InverseTraceRelations.v similarity index 100% rename from core/InverseTraceRelations.v rename to theories/Core/InverseTraceRelations.v diff --git a/core/LabeledNet.v b/theories/Core/LabeledNet.v similarity index 100% rename from core/LabeledNet.v rename to theories/Core/LabeledNet.v diff --git a/core/NameOverlay.v b/theories/Core/NameOverlay.v similarity index 100% rename from core/NameOverlay.v rename to theories/Core/NameOverlay.v diff --git a/core/Net.v b/theories/Core/Net.v similarity index 100% rename from core/Net.v rename to theories/Core/Net.v diff --git a/core/PartialExtendedMapSimulations.v b/theories/Core/PartialExtendedMapSimulations.v similarity index 100% rename from core/PartialExtendedMapSimulations.v rename to theories/Core/PartialExtendedMapSimulations.v diff --git a/core/PartialMapExecutionSimulations.v b/theories/Core/PartialMapExecutionSimulations.v similarity index 100% rename from core/PartialMapExecutionSimulations.v rename to theories/Core/PartialMapExecutionSimulations.v diff --git a/core/PartialMapSimulations.v b/theories/Core/PartialMapSimulations.v similarity index 100% rename from core/PartialMapSimulations.v rename to theories/Core/PartialMapSimulations.v diff --git a/core/SingleSimulations.v b/theories/Core/SingleSimulations.v similarity index 100% rename from core/SingleSimulations.v rename to theories/Core/SingleSimulations.v diff --git a/core/StateMachineHandlerMonad.v b/theories/Core/StateMachineHandlerMonad.v similarity index 100% rename from core/StateMachineHandlerMonad.v rename to theories/Core/StateMachineHandlerMonad.v diff --git a/core/StatePacketPacketDecomposition.v b/theories/Core/StatePacketPacketDecomposition.v similarity index 100% rename from core/StatePacketPacketDecomposition.v rename to theories/Core/StatePacketPacketDecomposition.v diff --git a/core/TotalMapExecutionSimulations.v b/theories/Core/TotalMapExecutionSimulations.v similarity index 100% rename from core/TotalMapExecutionSimulations.v rename to theories/Core/TotalMapExecutionSimulations.v diff --git a/core/TotalMapSimulations.v b/theories/Core/TotalMapSimulations.v similarity index 100% rename from core/TotalMapSimulations.v rename to theories/Core/TotalMapSimulations.v diff --git a/core/TraceRelations.v b/theories/Core/TraceRelations.v similarity index 100% rename from core/TraceRelations.v rename to theories/Core/TraceRelations.v diff --git a/core/Verdi.v b/theories/Core/Verdi.v similarity index 100% rename from core/Verdi.v rename to theories/Core/Verdi.v diff --git a/core/VerdiHints.v b/theories/Core/VerdiHints.v similarity index 100% rename from core/VerdiHints.v rename to theories/Core/VerdiHints.v diff --git a/extraction/ExtrOcamlBasicExt.v b/theories/Extraction/ExtrOcamlBasicExt.v similarity index 100% rename from extraction/ExtrOcamlBasicExt.v rename to theories/Extraction/ExtrOcamlBasicExt.v diff --git a/extraction/ExtrOcamlBool.v b/theories/Extraction/ExtrOcamlBool.v similarity index 100% rename from extraction/ExtrOcamlBool.v rename to theories/Extraction/ExtrOcamlBool.v diff --git a/extraction/ExtrOcamlDiskOp.v b/theories/Extraction/ExtrOcamlDiskOp.v similarity index 100% rename from extraction/ExtrOcamlDiskOp.v rename to theories/Extraction/ExtrOcamlDiskOp.v diff --git a/extraction/ExtrOcamlFinInt.v b/theories/Extraction/ExtrOcamlFinInt.v similarity index 100% rename from extraction/ExtrOcamlFinInt.v rename to theories/Extraction/ExtrOcamlFinInt.v diff --git a/extraction/ExtrOcamlList.v b/theories/Extraction/ExtrOcamlList.v similarity index 100% rename from extraction/ExtrOcamlList.v rename to theories/Extraction/ExtrOcamlList.v diff --git a/extraction/ExtrOcamlNatIntExt.v b/theories/Extraction/ExtrOcamlNatIntExt.v similarity index 100% rename from extraction/ExtrOcamlNatIntExt.v rename to theories/Extraction/ExtrOcamlNatIntExt.v diff --git a/lib/FMapVeryWeak.v b/theories/Lib/FMapVeryWeak.v similarity index 100% rename from lib/FMapVeryWeak.v rename to theories/Lib/FMapVeryWeak.v diff --git a/lib/Ssrexport.v b/theories/Lib/Ssrexport.v similarity index 100% rename from lib/Ssrexport.v rename to theories/Lib/Ssrexport.v diff --git a/systems/Counter.v b/theories/Systems/Counter.v similarity index 100% rename from systems/Counter.v rename to theories/Systems/Counter.v diff --git a/systems/LiveLockServ.v b/theories/Systems/LiveLockServ.v similarity index 100% rename from systems/LiveLockServ.v rename to theories/Systems/LiveLockServ.v diff --git a/systems/LockServ.v b/theories/Systems/LockServ.v similarity index 100% rename from systems/LockServ.v rename to theories/Systems/LockServ.v diff --git a/systems/LockServSeqNum.v b/theories/Systems/LockServSeqNum.v similarity index 100% rename from systems/LockServSeqNum.v rename to theories/Systems/LockServSeqNum.v diff --git a/systems/Log.v b/theories/Systems/Log.v similarity index 100% rename from systems/Log.v rename to theories/Systems/Log.v diff --git a/systems/LogCorrect.v b/theories/Systems/LogCorrect.v similarity index 100% rename from systems/LogCorrect.v rename to theories/Systems/LogCorrect.v diff --git a/systems/PrimaryBackup.v b/theories/Systems/PrimaryBackup.v similarity index 100% rename from systems/PrimaryBackup.v rename to theories/Systems/PrimaryBackup.v diff --git a/systems/SeqNum.v b/theories/Systems/SeqNum.v similarity index 100% rename from systems/SeqNum.v rename to theories/Systems/SeqNum.v diff --git a/systems/SeqNumCorrect.v b/theories/Systems/SeqNumCorrect.v similarity index 100% rename from systems/SeqNumCorrect.v rename to theories/Systems/SeqNumCorrect.v diff --git a/systems/SerializedMsgParams.v b/theories/Systems/SerializedMsgParams.v similarity index 100% rename from systems/SerializedMsgParams.v rename to theories/Systems/SerializedMsgParams.v diff --git a/systems/SerializedMsgParamsCorrect.v b/theories/Systems/SerializedMsgParamsCorrect.v similarity index 100% rename from systems/SerializedMsgParamsCorrect.v rename to theories/Systems/SerializedMsgParamsCorrect.v diff --git a/systems/VarD.v b/theories/Systems/VarD.v similarity index 100% rename from systems/VarD.v rename to theories/Systems/VarD.v diff --git a/systems/VarDPrimaryBackup.v b/theories/Systems/VarDPrimaryBackup.v similarity index 100% rename from systems/VarDPrimaryBackup.v rename to theories/Systems/VarDPrimaryBackup.v diff --git a/theories/dune b/theories/dune new file mode 100644 index 00000000..0ad1482b --- /dev/null +++ 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)