chore(Makefile): update make targets to new cli (#478)

.github/workflows/pull.yml

@@ -10,7 +10,7 @@ jobs:
     steps:
       - name: Populate Dafny versions list
         id: populate-dafny-versions-list
-        run: echo "dafny-versions-list=['4.2.0', '4.4.0', '4.8.0']" >> $GITHUB_OUTPUT
+        run: echo "dafny-versions-list=['4.5.0','4.8.0']" >> $GITHUB_OUTPUT
       - name: Populate Dafny versions list for "only new versions" languages (Python)
         id: populate-only-new-dafny-versions-list
         run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT

.github/workflows/push.yml

@@ -12,7 +12,7 @@ jobs:
     steps:
       - name: Populate Dafny versions list
         id: populate-dafny-versions-list
-        run: echo "dafny-versions-list=['4.2.0', '4.4.0', '4.8.0']" >> $GITHUB_OUTPUT
+        run: echo "dafny-versions-list=['4.5.0','4.8.0']" >> $GITHUB_OUTPUT
       - name: Populate Dafny versions list for "only new versions" languages (Python)
         id: populate-only-new-dafny-versions-list
         run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT

SmithyDafnyMakefile.mk

@@ -82,47 +82,47 @@ ENABLE_EXTERN_PROCESSING?=
 # Verify the entire project
 verify:Z3_PROCESSES=$(shell echo $$(( $(CORES) >= 3 ? 2 : 1 )))
 verify:DAFNY_PROCESSES=$(shell echo $$(( ($(CORES) - 1 ) / ($(CORES) >= 3 ? 2 : 1))))
+# TODO: remove dafny_options from all targets in the future
+# and leave it up to the UX to decide which options they want to add
+verify:DAFNY_OPTIONS=--allow-warnings
 verify:
-	find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny \
-		-vcsCores:$(Z3_PROCESSES) \
-		-compile:0 \
-		-definiteAssignment:3 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-verificationLogger:csv \
-		-timeLimit:$(VERIFY_TIMEOUT) \
-		-rlimit:$(MAX_RESOURCE_COUNT) \
+	find . -name '*.dfy' | xargs -n 1 -P $(DAFNY_PROCESSES) -I % dafny verify \
+		--cores $(Z3_PROCESSES) \
+		--unicode-char false \
+		--function-syntax 3 \
+		--log-format csv \
+		--verification-time-limit $(VERIFY_TIMEOUT) \
+		--resource-limit $(MAX_RESOURCE_COUNT) \
 		$(DAFNY_OPTIONS) \
 		%
 
 # Verify single file FILE with text logger.
 # This is useful for debugging resource count usage within a file.
 # Use PROC to further scope the verification
+verify_single:DAFNY_OPTIONS=--allow-warnings
 verify_single:
-	dafny \
-		-vcsCores:$(CORES) \
-		-compile:0 \
-		-definiteAssignment:3 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-verificationLogger:text \
-		-timeLimit:$(VERIFY_TIMEOUT) \
-		-rlimit:$(MAX_RESOURCE_COUNT) \
+	dafny verify \
+		--cores $(CORES) \
+		--unicode-char false \
+		--function-syntax 3 \
+		--log-format text \
+		--verification-time-limit $(VERIFY_TIMEOUT) \
+		--resource-limit $(MAX_RESOURCE_COUNT) \
 		$(DAFNY_OPTIONS) \
 		$(if ${PROC},-proc:*$(PROC)*,) \
 		$(FILE)
 
 #Verify only a specific namespace at env var $(SERVICE)
+verify_service:DAFNY_OPTIONS=--allow-warnings
 verify_service:
 	@: $(if ${SERVICE},,$(error You must pass the SERVICE to generate for));
-	dafny \
-		-vcsCores:$(CORES) \
-		-compile:0 \
-		-definiteAssignment:3 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-verificationLogger:csv \
-		-timeLimit:$(VERIFY_TIMEOUT) \
+	dafny verify \
+		--cores $(CORES) \
+		--unicode-char false \
+		--function-syntax 3 \
+		--log-format text \
+		--verification-time-limit $(VERIFY_TIMEOUT) \
+		--resource-limit $(MAX_RESOURCE_COUNT) \
 		$(DAFNY_OPTIONS) \
 		`find ./dafny/$(SERVICE) -name '*.dfy'` \
 
@@ -151,20 +151,16 @@ dafny-reportgenerator:
 clean-dafny-report:
 	rm TestResults/*.csv
 
+get_dafny_version:
+	DAFNY_VERSION=$(shell ./scripts/check_dafny_version.sh)
 # Dafny helper targets
 
 # Transpile the entire project's impl
 # For each index file listed in the project Makefile's PROJECT_INDEX variable,
 #   append a `-library:TestModels/$(PROJECT_INDEX) to the transpiliation target
-_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
-_transpile_implementation_all: transpile_implementation
+_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
+_transpile_implementation_all: get_dafny_version transpile_implementation 
 
-# TODO-new-cli: As part of supporting Dafny 4.8+, Java and NET SHOULD migrate to the new Dafny CLI,
-# the `transpile_implementation` target should start using the new Dafny CLI,
-# and the `transpile_implementation_new_cli` target should be removed
-# in favor of `transpile_implementation` using the new CLI.
-_transpile_implementation_all_new_cli: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
-_transpile_implementation_all_new_cli: transpile_implementation_new_cli
 
 # The `$(OUT)` and $(TARGET) variables are problematic.
 # Ideally they are different for every target call.
@@ -197,30 +193,6 @@ transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src
 # Also the expectation is that verification happens in the `verify` target
 # `find` looks for `Index.dfy` files in either V1 or V2-styled project directories (single vs. multiple model files).
 transpile_implementation:
-	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		-out $(OUT) \
-		$(DAFNY_OPTIONS) \
-		$(DAFNY_OTHER_FILES) \
-		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
-		$(TRANSPILE_DEPENDENCIES)
-
-# TODO-new-cli: As part of supporting Dafny 4.8+, Java and NET SHOULD migrate to the new Dafny CLI,
-# the `transpile_implementation` target should start using the new Dafny CLI,
-# and the `transpile_implementation_new_cli` target should be removed
-# in favor of `transpile_implementation` using the new CLI.
-transpile_implementation_new_cli: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
-transpile_implementation_new_cli:
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
 	translate $(TARGET) \
 		--stdin \
@@ -229,7 +201,6 @@ transpile_implementation_new_cli:
 		--optimize-erasable-datatype-wrapper:false \
 		--unicode-char:false \
 		--function-syntax:3 \
-		--allow-warnings \
 		--output $(OUT) \
 		$(DAFNY_OPTIONS) \
 		$(DAFNY_OTHER_FILES) \
@@ -255,54 +226,19 @@ _transpile_test_all: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
 #     append `-library:/path/to/Index.dfy` to the transpile target
 # Else: (i.e. single model/service in project), then:
 #   append `-library:/path/to/Index.dfy` to the transpile target
-_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, -library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), -library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
+_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, --library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), --library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
 # Transpile the entire project's tests
-_transpile_test_all: transpile_test
-
-# TODO-new-cli: As part of supporting Dafny 4.8+, Java and NET SHOULD migrate to the new Dafny CLI,
-# the `transpile_implementation` target should start using the new Dafny CLI,
-# and the `transpile_implementation_new_cli` target should be removed
-# in favor of `transpile_implementation` using the new CLI.
-_transpile_test_all_new_cli: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
-_transpile_test_all_new_cli: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
-_transpile_test_all_new_cli: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, --library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), --library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
-_transpile_test_all_new_cli: transpile_test_new_cli
+_transpile_test_all: get_dafny_version transpile_test
 
 transpile_test:
-	find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-runAllTests:1 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		-out $(OUT) \
-		$(DAFNY_OPTIONS) \
-		$(DAFNY_OTHER_FILES) \
-		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
-		$(TRANSPILE_DEPENDENCIES) \
-
-# TODO-new-cli: As part of supporting Dafny 4.8+, Java and NET SHOULD migrate to the new Dafny CLI,
-# the `transpile_implementation` target should start using the new Dafny CLI,
-# and the `transpile_implementation_new_cli` target should be removed
-# in favor of `transpile_implementation` using the new CLI.
-transpile_test_new_cli:
 	find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
 		translate $(TARGET) \
 		--stdin \
 		--no-verify \
 		--cores:$(CORES) \
-		--include-test-runner \
 		--optimize-erasable-datatype-wrapper:false \
 		--unicode-char:false \
 		--function-syntax:3 \
-		--allow-warnings \
 		--output $(OUT) \
 		$(DAFNY_OPTIONS) \
 		$(DAFNY_OTHER_FILES) \
@@ -392,7 +328,7 @@ _polymorph_dependencies:
 # Not including Rust until is it more fully implemented.
 .PHONY: polymorph_code_gen
 polymorph_code_gen: POLYMORPH_LANGUAGE_TARGET=code_gen
-polymorph_code_gen: _polymorph_dependencies
+polymorph_code_gen: get_dafny_version _polymorph_dependencies
 polymorph_code_gen:
 	set -e; for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
@@ -417,7 +353,7 @@ check_polymorph_diff:
 # Generates dafny code for all namespaces in this project
 .PHONY: polymorph_dafny
 polymorph_dafny: POLYMORPH_LANGUAGE_TARGET=dafny
-polymorph_dafny: _polymorph_dependencies
+polymorph_dafny: get_dafny_version _polymorph_dependencies
 polymorph_dafny:
 	set -e; for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
@@ -435,7 +371,7 @@ _polymorph_dafny: _polymorph
 # Generates dotnet code for all namespaces in this project
 .PHONY: polymorph_dotnet
 polymorph_dotnet: POLYMORPH_LANGUAGE_TARGET=dotnet
-polymorph_dotnet: _polymorph_dependencies
+polymorph_dotnet: get_dafny_version _polymorph_dependencies
 polymorph_dotnet:
 	set -e; for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
@@ -453,7 +389,7 @@ _polymorph_dotnet: _polymorph
 # Generates java code for all namespaces in this project
 .PHONY: polymorph_java
 polymorph_java: POLYMORPH_LANGUAGE_TARGET=java
-polymorph_java: _polymorph_dependencies
+polymorph_java: get_dafny_version _polymorph_dependencies
 polymorph_java:
 	set -e; for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
@@ -471,7 +407,7 @@ _polymorph_java: _polymorph
 # Generates python code for all namespaces in this project
 .PHONY: polymorph_python
 polymorph_python: POLYMORPH_LANGUAGE_TARGET=python
-polymorph_python: _polymorph_dependencies
+polymorph_python: get_dafny_version _polymorph_dependencies
 polymorph_python:
 	set -e; for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
@@ -497,7 +433,7 @@ setup_prettier:
 # so we assume that is run first!
 .PHONY: polymorph_rust
 polymorph_rust: POLYMORPH_LANGUAGE_TARGET=rust
-polymorph_rust: _polymorph_dependencies
+polymorph_rust: get_dafny_version _polymorph_dependencies
 polymorph_rust:
 	set -e; for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
@@ -520,11 +456,13 @@ transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, )
 
 transpile_implementation_net: TARGET=cs
 transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny
+transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix
 transpile_implementation_net: SRC_INDEX=$(NET_SRC_INDEX)
 transpile_implementation_net: _transpile_implementation_all
 
 transpile_test_net: SRC_INDEX=$(NET_SRC_INDEX)
 transpile_test_net: TEST_INDEX=$(NET_TEST_INDEX)
+transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix
 transpile_test_net: TARGET=cs
 transpile_test_net: OUT=runtimes/net/tests/TestsFromDafny
 transpile_test_net: _transpile_test_all
@@ -569,10 +507,12 @@ transpile_java: | transpile_implementation_java transpile_test_java transpile_de
 transpile_java: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, )
 
 transpile_implementation_java: TARGET=java
+transpile_implementation_java: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix
 transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny
 transpile_implementation_java: _transpile_implementation_all _mv_implementation_java
 
 transpile_test_java: TARGET=java
+transpile_test_java: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix
 transpile_test_java: OUT=runtimes/java/TestsFromDafny
 transpile_test_java: _transpile_test_all _mv_test_java
 
@@ -623,7 +563,7 @@ transpile_implementation_rust: SRC_INDEX=$(RUST_SRC_INDEX)
 transpile_implementation_rust: TEST_INDEX=$(RUST_TEST_INDEX)
 # The Dafny Rust code generator is not complete yet,
 # so we want to emit code even if there are unsupported features in the input.
-transpile_implementation_rust: DAFNY_OPTIONS=-emitUncompilableCode
+transpile_implementation_rust: DAFNY_OPTIONS=--emit-uncompilable-code --allow-warnings --compile-suffix
 # The Dafny Rust code generator only supports a single crate for everything,
 # so we inline all dependencies by not passing `-library` to Dafny.
 transpile_implementation_rust: TRANSPILE_DEPENDENCIES=
@@ -696,20 +636,22 @@ transpile_python: $(if $(ENABLE_EXTERN_PROCESSING), _no_extern_pre_transpile, )
 transpile_python: | transpile_dependencies_python transpile_implementation_python transpile_test_python
 transpile_python: $(if $(ENABLE_EXTERN_PROCESSING), _no_extern_post_transpile, )
 
+transpile_implementation_python: DAFNY_OPTIONS=--allow-warnings --include-test-runner
 transpile_implementation_python: TARGET=py
 transpile_implementation_python: OUT=runtimes/python/dafny_src
 transpile_implementation_python: SRC_INDEX=$(PYTHON_SRC_INDEX)
 transpile_implementation_python: TRANSPILE_MODULE_NAME=--python-module-name=$(PYTHON_MODULE_NAME).internaldafny.generated
 transpile_implementation_python: TRANSLATION_RECORD=$(TRANSLATION_RECORD_PYTHON)
-transpile_implementation_python: _transpile_implementation_all_new_cli _mv_implementation_python
+transpile_implementation_python: _transpile_implementation_all _mv_implementation_python
 
 transpile_test_python: TARGET=py
 transpile_test_python: OUT=runtimes/python/dafny_test
+transpile_test_python: DAFNY_OPTIONS=--allow-warnings --include-test-runner
 transpile_test_python: SRC_INDEX=$(PYTHON_SRC_INDEX)
 transpile_test_python: TEST_INDEX=$(PYTHON_TEST_INDEX)
 transpile_test_python: TRANSLATION_RECORD=$(TRANSLATION_RECORD_PYTHON)
 transpile_test_python: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/python/src/$(PYTHON_MODULE_NAME)/internaldafny/generated/dafny_src-py.dtr
-transpile_test_python: _transpile_test_all_new_cli _mv_test_python
+transpile_test_python: _transpile_test_all _mv_test_python
 
 # Move Dafny-generated code into its expected location in the Python module
 _mv_implementation_python:

TestModels/dafny-dependencies/StandardLibrary/Makefile

@@ -82,29 +82,8 @@ transpile_dependencies:
 
 # Override SharedMakefile's transpile_implementation to not reference
 # StandardLibrary as a Library
+transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
 transpile_implementation:
-	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		$(DAFNY_OPTIONS) \
-		$(DAFNY_OTHER_FILES) \
-		-out $(OUT)
-
-# TODO-new-cli: As part of supporting Dafny 4.8+, Java and NET SHOULD migrate to the new Dafny CLI,
-# the `transpile_implementation` target should start using the new Dafny CLI,
-# and the `transpile_implementation_new_cli` target should be removed
-# in favor of `transpile_implementation` using the new CLI.
-transpile_implementation_new_cli: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
-transpile_implementation_new_cli:
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
 	translate $(TARGET) \
 		--stdin \
@@ -113,7 +92,6 @@ transpile_implementation_new_cli:
 		--optimize-erasable-datatype-wrapper:false \
 		--unicode-char:false \
 		--function-syntax:3 \
-		--allow-warnings \
 		--output $(OUT) \
 		$(DAFNY_OPTIONS) \
 		$(DAFNY_OTHER_FILES) \
@@ -147,4 +125,4 @@ dafny_benerate:
 	# diff -u $(DAFNY_RUST_OUTPUT_RS) $(DAFNY_RUST_IMPL) | wc -l
 	mv $(DAFNY_RUST_OUTPUT_RS) $(DAFNY_RUST_IMPL)
 	rm $(DAFNY_RUST_OUTPUT_RS_DTR);
-	rm -r $(DAFNY_RUST_OUTPUT_FOLDER);
+	rm -r $(DAFNY_RUST_OUTPUT_FOLDER);

codegen/smithy-dafny-codegen/src/test/java/software/amazon/polymorph/smithyjava/ForEachDafnyTest.java

@@ -13,12 +13,6 @@ public abstract class ForEachDafnyTest {
 
   @Parameterized.Parameters(name = "dafnyVersion = {0}")
   public static Collection dafnies() {
-    return Arrays.asList(
-      new Object[][] {
-        { new DafnyVersion(4, 1, 0) },
-        { new DafnyVersion(4, 3, 0) },
-        { new DafnyVersion(4, 8, 0) },
-      }
-    );
+    return Arrays.asList(new Object[][] { { new DafnyVersion(4, 8, 0) } });
   }
 }