makefile adjustments

Author: palmskog

Core/Makefile

@@ -8,9 +8,8 @@ default: Makefile.coq
 install: Makefile.coq
 	$(MAKE) -f Makefile.coq install
 
-clean:
-	if [ -f Makefile.coq ]; then \
-	  $(MAKE) -f Makefile.coq clean; fi
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq cleanall
 	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: Make

Examples/Make

@@ -1,23 +1,26 @@
 -Q . DiSeL
 -arg "-w -notation-overridden,-local-declaration,-redundant-canonical-projection,-projection-no-head-constant"
 
-SeqLib.v
-Greeter/Greeter.v
-Querying/QueryProtocol.v
-Querying/QueryHooked.v
-Calculator/CalculatorProtocol.v
+Calculator/CalculatorExtraction.v
 Calculator/CalculatorInvariant.v
-Calculator/CalculatorClientLib.v
-Calculator/CalculatorServerLib.v
-Calculator/SimpleCalculatorServers.v
 Calculator/DelegatingCalculatorServer.v
+Calculator/SimpleCalculatorServers.v
+Calculator/CalculatorClientLib.v
+Calculator/CalculatorProtocol.v
 Calculator/SimpleCalculatorApp.v
-TwoPhaseCommit/TwoPhaseProtocol.v
-TwoPhaseCommit/TwoPhaseCoordinator.v
-TwoPhaseCommit/TwoPhaseParticipant.v
+Calculator/CalculatorServerLib.v
+SeqLib.v
+LockResource/ResourceProtocol.v
+LockResource/LockProtocol.v
 TwoPhaseCommit/SimpleTPCApp.v
 TwoPhaseCommit/TwoPhaseInductiveInv.v
-TwoPhaseCommit/TwoPhaseInductiveProof.v 
+TwoPhaseCommit/TwoPhaseClient.v
+TwoPhaseCommit/TwoPhaseInductiveProof.v
+TwoPhaseCommit/TwoPhaseParticipant.v
+TwoPhaseCommit/TwoPhaseExtraction.v
+TwoPhaseCommit/TwoPhaseProtocol.v
+TwoPhaseCommit/TwoPhaseCoordinator.v
+Greeter/Greeter.v
 Querying/QueryPlusTPC.v
-LockResource/LockProtocol.v
-LockResource/ResourceProtocol.v
+Querying/QueryProtocol.v
+Querying/QueryHooked.v

Examples/Makefile

@@ -8,9 +8,8 @@ default: Makefile.coq
 install: Makefile.coq
 	$(MAKE) -f Makefile.coq install
 
-clean:
-	if [ -f Makefile.coq ]; then \
-	  $(MAKE) -f Makefile.coq clean; fi
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq cleanall
 	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: Make

Examples/TwoPhaseCommit/TwoPhaseClient.v

@@ -4,11 +4,12 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding domain.
-Require Import State DepMaps Protocols Worlds NetworkSem Rely.
-Require Import HoareTriples InferenceRules.
-Require Import While.
-Require Import TwoPhaseProtocol TwoPhaseInductiveInv TwoPhaseCoordinator TwoPhaseParticipant.
+From fcsl
+Require Import pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL
+Require Import State DepMaps Protocols Worlds NetworkSem Rely HoareTriples InferenceRules.
+From DiSeL
+Require Import While TwoPhaseProtocol TwoPhaseInductiveInv TwoPhaseCoordinator TwoPhaseParticipant.
 
 Section TwoPhaseClient.
 

Makefile

@@ -8,9 +8,8 @@ default: Makefile.coq
 install: Makefile.coq
 	$(MAKE) -f Makefile.coq install
 
-clean:
-	if [ -f Makefile.coq ]; then \
-	  $(MAKE) -f Makefile.coq clean; fi
+clean: Makefile.coq
+	$(MAKE) -f Makefile.coq cleanall
 	rm -f Makefile.coq Makefile.coq.conf
 
 Makefile.coq: _CoqProject

_CoqProject

@@ -40,7 +40,8 @@ Examples/TwoPhaseCommit/TwoPhaseParticipant.v
 Examples/TwoPhaseCommit/SimpleTPCApp.v
 Examples/TwoPhaseCommit/TwoPhaseExtraction.v
 Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
-Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v 
+Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
+Examples/TwoPhaseCommit/TwoPhaseClient.v
 Examples/Querying/QueryPlusTPC.v
 Examples/LockResource/LockProtocol.v
 Examples/LockResource/ResourceProtocol.v