feat: Update Simple Blob to use shared makefile (#128)

aws · Feb 2, 2023 · 1017965 · 1017965
1 parent 713357f
commit 1017965
Showing 1 changed file with 5 additions and 88 deletions.
diff --git a/TestModels/SimpleTypes/SimpleBlob/Makefile b/TestModels/SimpleTypes/SimpleBlob/Makefile
@@ -2,95 +2,12 @@
 # SPDX-License-Identifier: Apache-2.0
 
 CORES=2
-DAFNY_ROOT := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
-polymorph_dafny :
-	cd ../../../smithy-polymorph;\
-	./gradlew run --args="\
-	--output-dafny \
-	--include-dafny $(DAFNY_ROOT)/../../dafny-dependencies/StandardLibrary/src/Index.dfy \
-	--model $(DAFNY_ROOT)/Model \
-	--dependent-model $(DAFNY_ROOT)/../../dafny-dependencies/Model \
-	--namespace simple.types.blob"; \
-	./gradlew run --args="\
-	--output-dafny \
-	--output-local-service-test $(DAFNY_ROOT)/Model \
-	--include-dafny $(DAFNY_ROOT)/../../dafny-dependencies/StandardLibrary/src/Index.dfy \
-	--model $(DAFNY_ROOT)/Model \
-	--dependent-model $(DAFNY_ROOT)/../../dafny-dependencies/Model \
-	--namespace simple.types.blob"; \
+include ../../SharedMakefile.mk
 
-polymorph_net :
-	cd ../../../smithy-polymorph;\
-	./gradlew run --args="\
-	--output-dafny \
-	--include-dafny $(DAFNY_ROOT)/../../dafny-dependencies/StandardLibrary/src/Index.dfy \
-	--output-dotnet $(DAFNY_ROOT)/runtimes/net/Generated/ \
-	--model $(DAFNY_ROOT)/Model \
-	--dependent-model $(DAFNY_ROOT)/../../dafny-dependencies/Model \
-	--namespace simple.types.blob"; \
-	./gradlew run --args="\
-	--output-dafny \
-	--output-local-service-test $(DAFNY_ROOT)/Model \
-	--include-dafny $(DAFNY_ROOT)/../../dafny-dependencies/StandardLibrary/src/Index.dfy \
-	--output-dotnet $(DAFNY_ROOT)/runtimes/net/Generated/Wrapped \
-	--model $(DAFNY_ROOT)/Model \
-	--dependent-model $(DAFNY_ROOT)/../../dafny-dependencies/Model \
-	--namespace simple.types.blob"; \
-
-verify:
-	dafny \
-		-vcsCores:$(CORES) \
-		-compile:0 \
-		-definiteAssignment:3 \
-		-verificationLogger:csv \
-		-timeLimit:300 \
-		-trace \
-		`find . -name '*.dfy'`
-
-dafny-reportgenerator:
-	dafny-reportgenerator \
-		summarize-csv-results \
-		--max-resource-count 10000000 \
-		TestResults/*.csv
-
-transpile_net: | transpile_implementation_net transpile_test_net transpile_net_dependencies
-
-transpile_implementation_net:
-	dafny \
-		-vcsCores:$(CORES) \
-		-compileTarget:cs \
-		-spillTargetCode:3 \
-		-runAllTests:1 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-useRuntimeLib \
-		-out runtimes/net/ImplementationFromDafny \
-		./src/Index.dfy \
-		-library:../../dafny-dependencies/StandardLibrary/src/Index.dfy \
-
-
-transpile_test_net:
-	dafny \
-		-vcsCores:$(CORES) \
-		-compileTarget:cs \
-		-spillTargetCode:3 \
-		-runAllTests:1 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-useRuntimeLib \
-		-out runtimes/net/tests/TestsFromDafny \
-		`find ./test -name '*.dfy'` \
-		-library:src/Index.dfy
+NAMESPACE=simple.types.blob
 
+# This project has no dependencies 
+# DEPENDENT-MODELS:= 
+# LIBRARIES :=
 transpile_net_dependencies:
-	$(MAKE) -C ../../dafny-dependencies/StandardLibrary transpile_implementation_net \
-
-test_net:
-	dotnet run \
-		--project runtimes/net/tests/ \
-		--framework net6.0
-
-setup_net:
-	dotnet restore runtimes/net/
-