feat: Updates to use shared makefile (#129)

aws · Feb 3, 2023 · b1331dc · b1331dc
1 parent 1017965
commit b1331dc
Show file tree

Hide file tree

Showing 6 changed files with 30 additions and 533 deletions.
diff --git a/TestModels/Aggregate/Makefile b/TestModels/Aggregate/Makefile
@@ -2,92 +2,12 @@
 # SPDX-License-Identifier: Apache-2.0
 
 CORES=2
-DAFNY_ROOT := $(shell pwd)
 
-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.aggregate"; \
-	./gradlew run --args="\
-	--output-dafny $(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.aggregate --output-local-service-test $(DAFNY_ROOT)/Model"; \
+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.aggregate"; \
-	./gradlew run --args="\
-	--output-dafny $(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.aggregate --output-local-service-test $(DAFNY_ROOT)/Model"; \
-
-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.aggregate
 
+# 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/
diff --git a/TestModels/SimpleTypes/BigDecimal/Makefile b/TestModels/SimpleTypes/BigDecimal/Makefile
@@ -1,97 +1,13 @@
 # Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0
 
-DAFNY_ROOT := $(shell pwd)
 CORES=2
 
-# Note: This build target fails. polymorph.smithydafny does not support generation for BigDecimal types.
-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.bigDecimal"; \
-	./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.bigDecimal"; \
+include ../../SharedMakefile.mk
 
-# Note: This build target fails. polymorph.smithydotnet does not support generation for BigDecimal types.
-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.bigDecimal"; \
-	./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.bigDecimal"; \
-
-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.bigDecimal
 
+# 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/
diff --git a/TestModels/SimpleTypes/SimpleFloat/Makefile b/TestModels/SimpleTypes/SimpleFloat/Makefile
@@ -2,97 +2,12 @@
 # SPDX-License-Identifier: Apache-2.0
 
 CORES=2
-DAFNY_ROOT := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
-# Note: This build target fails. polymorph.smithydafny does not support generation for Float types.
-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.float"; \
-	./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.float"; \
+include ../../SharedMakefile.mk
 
-# Note: This build target fails. polymorph.smithydotnet does not support generation for Float types.
-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.float"; \
-	./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.float"; \
-
-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.float
 
+# 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/
-