Skip to content

Commit

Permalink
fix: Provide -compileSuffix to dafny when available (#280)
Browse files Browse the repository at this point in the history
  • Loading branch information
robin-aws authored Jul 17, 2023
1 parent d7b080a commit 32b6638
Showing 1 changed file with 14 additions and 0 deletions.
14 changes: 14 additions & 0 deletions TestModels/SharedMakefile.mk
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,18 @@ PROJECT_RELATIVE_ROOT := $(dir $(lastword $(MAKEFILE_LIST)))
# i.e. The specific library under consideration.
LIBRARY_ROOT = $(PWD)

# Later versions of Dafny no longer default to adding "_Compile"
# to the names of modules when translating.
# Our target language code still assumes it does,
# so IF the /compileSuffix option is available in our verion of Dafny
# we need to provide it.
COMPILE_SUFFIX_OPTION_CHECK_EXIT_CODE := $(shell dafny /help | grep -q /compileSuffix; echo $$?)
ifeq ($(COMPILE_SUFFIX_OPTION_CHECK_EXIT_CODE), 0)
COMPILE_SUFFIX_OPTION := -compileSuffix:1
else
COMPILE_SUFFIX_OPTION :=
endif

STANDARD_LIBRARY_PATH := $(PROJECT_ROOT)/dafny-dependencies/StandardLibrary
CODEGEN_CLI_ROOT := $(PROJECT_ROOT)/../codegen/smithy-dafny-codegen-cli
GRADLEW := $(PROJECT_ROOT)/../codegen/gradlew
Expand Down Expand Up @@ -92,6 +104,7 @@ transpile_implementation:
-spillTargetCode:3 \
-compile:0 \
-optimizeErasableDatatypeWrapper:0 \
$(COMPILE_SUFFIX_OPTION) \
-quantifierSyntax:3 \
-unicodeChar:0 \
-functionSyntax:3 \
Expand All @@ -109,6 +122,7 @@ transpile_test:
-runAllTests:1 \
-compile:0 \
-optimizeErasableDatatypeWrapper:0 \
$(COMPILE_SUFFIX_OPTION) \
-quantifierSyntax:3 \
-unicodeChar:0 \
-functionSyntax:3 \
Expand Down

0 comments on commit 32b6638

Please sign in to comment.