From 21bdd580ed7b7fda3548b5cfa0600888fcac9110 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 13 Jul 2023 16:39:08 -0700 Subject: [PATCH] fix: Provide -compileSuffix to dafny when available --- SharedMakefile.mk | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/SharedMakefile.mk b/SharedMakefile.mk index f7fbd3e02..721a4abf5 100644 --- a/SharedMakefile.mk +++ b/SharedMakefile.mk @@ -45,6 +45,18 @@ LIBRARY_ROOT := $(PWD) # but still build everything in their local library directory. SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model +# 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 + ########################## Dafny targets # Verify the entire project @@ -152,6 +164,7 @@ transpile_implementation: -spillTargetCode:3 \ -compile:0 \ -optimizeErasableDatatypeWrapper:0 \ + $(COMPILE_SUFFIX_OPTION) \ -quantifierSyntax:3 \ -unicodeChar:0 \ -functionSyntax:3 \ @@ -174,6 +187,7 @@ transpile_test: -runAllTests:1 \ -compile:0 \ -optimizeErasableDatatypeWrapper:0 \ + $(COMPILE_SUFFIX_OPTION) \ -quantifierSyntax:3 \ -unicodeChar:0 \ -functionSyntax:3 \