chore: Optionally remove extern names when compiling to certain langu…

…ages (#512)

SmithyDafnyMakefile.mk

@@ -56,14 +56,16 @@ SMITHY_MODEL_ROOT := $(LIBRARY_ROOT)/Model
 CODEGEN_CLI_ROOT := $(SMITHY_DAFNY_ROOT)/codegen/smithy-dafny-codegen-cli
 GRADLEW := $(SMITHY_DAFNY_ROOT)/codegen/gradlew
 
-########################## Dafny targets
+include $(SMITHY_DAFNY_ROOT)/SmithyDafnySedMakefile.mk
+
+# This flag enables pre-processing on extern module names.
+# This pre-processing is required to compile to Python and Go.
+# This is disabled by default.
+# This should be enabled in each individual project's Makefile if that project compiles to Python or Go.
+# This can be enabled by setting this variable to any nonempty value (ex. true, 1)
+ENABLE_EXTERN_PROCESSING?=
 
-# TODO: This target will not work for projects that use `replaceable` 
-#       module syntax with multiple language targets.
-# It will fail with error:
-# Error: modules 'A' and 'B' both have CompileName 'same.extern.name'
-# We need to come up with some way to verify files per-language.
-# Rewrite this as part of Java implementation of LanguageSpecificLogic TestModel.
+########################## Dafny targets
 
 # Proof of correctness for the math below
 #  function Z3_PROCESSES(cpus:nat): nat
@@ -426,7 +428,9 @@ _polymorph_rust: $(if $(RUST_BENERATED), , _polymorph)
 
 ########################## .NET targets
 
+transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_pre_transpile, )
 transpile_net: | transpile_implementation_net transpile_test_net transpile_dependencies_net
+transpile_net: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, )
 
 transpile_implementation_net: TARGET=cs
 transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny
@@ -474,7 +478,9 @@ format_net-check:
 build_java: transpile_java mvn_local_deploy_dependencies
 	$(GRADLEW) -p runtimes/java build
 
+transpile_java: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_pre_transpile, )
 transpile_java: | transpile_implementation_java transpile_test_java transpile_dependencies_java
+transpile_java: $(if $(ENABLE_EXTERN_PROCESSING), _with_extern_post_transpile, )
 
 transpile_implementation_java: TARGET=java
 transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny

SmithyDafnySedMakefile.mk

@@ -0,0 +1,83 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+# These are make targets that use sed to replace extern names.
+# Some Smithy-Dafny modules declare extern attributes with names that do not work in all languages.
+# These targets can remove or add those extern names based on the target language.
+# A target language SHOULD declare use of these targets.
+
+# These should eventually be replaced by replaceable modules that declare per-langauge extern names.
+# See https://github.com/smithy-lang/smithy-dafny/issues/528.
+# Eventually, the replaceable modules should be removed (or, their extern names should be removed),
+# and should be replaced by per-language package/namespace prefixes.
+
+# On macOS, sed requires an extra parameter of ""
+OS := $(shell uname)
+ifeq ($(OS), Darwin)
+  SED_PARAMETER := ""
+else
+  SED_PARAMETER :=
+endif
+
+# Before transpiling to a target language that does not expect externs,
+# remove any extern attributes.
+_no_extern_pre_transpile: _no_extern_pre_transpile_dependencies _sed_types_file_remove_extern _sed_index_file_remove_extern _sed_wrapped_types_file_remove_extern
+# After transpiling to a target language that does not expect externs,
+# then add back any extern attributes,
+# because the expected committed state has extern attributes.
+_no_extern_post_transpile: _no_extern_post_transpile_dependencies _sed_types_file_add_extern _sed_index_file_add_extern _sed_wrapped_types_file_add_extern
+# Before transpiling to a target language that does expect externs,
+# add back any extern attributes if they are not present.
+_with_extern_pre_transpile: _with_extern_pre_transpile_dependencies _sed_types_file_add_extern _sed_index_file_add_extern _sed_wrapped_types_file_add_extern
+# After transpiling to a target language that does expect externs,
+# add back any extern attributes if they are not present for any reason.
+_with_extern_post_transpile: _with_extern_post_transpile_dependencies _sed_types_file_add_extern _sed_index_file_add_extern _sed_wrapped_types_file_add_extern
+
+_no_extern_pre_transpile_dependencies:
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _no_extern_pre_transpile;, $(PROJECT_DEPENDENCIES))
+
+_no_extern_post_transpile_dependencies:
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _no_extern_post_transpile;, $(PROJECT_DEPENDENCIES))
+
+_with_extern_pre_transpile_dependencies:
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _with_extern_pre_transpile;, $(PROJECT_DEPENDENCIES))
+
+_with_extern_post_transpile_dependencies:
+	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% _with_extern_post_transpile;, $(PROJECT_DEPENDENCIES))
+
+_sed_types_file_remove_extern:
+	@if [ -z $(TYPES_FILE_PATH) ] || [ -z $(TYPES_FILE_WITH_EXTERN_STRING) ] || [ -z $(TYPES_FILE_WITHOUT_EXTERN_STRING) ]; then \
+		echo "Error: All variables TYPES_FILE_PATH, TYPES_FILE_WITH_EXTERN_STRING, and TYPES_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \
+		exit 1; \
+	fi
+	$(MAKE) _sed_file SED_FILE_PATH=$(TYPES_FILE_PATH) SED_BEFORE_STRING=$(TYPES_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(TYPES_FILE_WITHOUT_EXTERN_STRING)
+
+_sed_index_file_remove_extern:
+	@if [ -z $(INDEX_FILE_PATH) ] || [ -z $(INDEX_FILE_WITH_EXTERN_STRING) ] || [ -z $(INDEX_FILE_WITHOUT_EXTERN_STRING) ]; then \
+		echo "Error: All variables INDEX_FILE_PATH, INDEX_FILE_WITH_EXTERN_STRING, and INDEX_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \
+		exit 1; \
+	fi
+	$(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING)
+
+_sed_wrapped_types_file_remove_extern:
+	$(if $(strip $(WRAPPED_INDEX_FILE_PATH)), $(MAKE) _sed_file SED_FILE_PATH=$(WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(WRAPPED_INDEX_FILE_WITH_EXTERN_STRING) SED_AFTER_STRING=$(WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING), )
+
+_sed_types_file_add_extern:
+	@if [ -z $(TYPES_FILE_PATH) ] || [ -z $(TYPES_FILE_WITH_EXTERN_STRING) ] || [ -z $(TYPES_FILE_WITHOUT_EXTERN_STRING) ]; then \
+		echo "Error: All variables TYPES_FILE_PATH, TYPES_FILE_WITH_EXTERN_STRING, and TYPES_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \
+		exit 1; \
+	fi
+	$(MAKE) _sed_file SED_FILE_PATH=$(TYPES_FILE_PATH) SED_BEFORE_STRING=$(TYPES_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(TYPES_FILE_WITH_EXTERN_STRING)
+
+_sed_index_file_add_extern:
+	@if [ -z $(INDEX_FILE_PATH) ] || [ -z $(INDEX_FILE_WITH_EXTERN_STRING) ] || [ -z $(INDEX_FILE_WITHOUT_EXTERN_STRING) ]; then \
+		echo "Error: All variables INDEX_FILE_PATH, INDEX_FILE_WITH_EXTERN_STRING, and INDEX_FILE_WITHOUT_EXTERN_STRING must be set and non-empty."; \
+		exit 1; \
+	fi
+	$(MAKE) _sed_file SED_FILE_PATH=$(INDEX_FILE_PATH) SED_BEFORE_STRING=$(INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(INDEX_FILE_WITH_EXTERN_STRING)
+
+_sed_wrapped_types_file_add_extern:
+	$(if $(strip $(WRAPPED_INDEX_FILE_PATH)), $(MAKE) _sed_file SED_FILE_PATH=$(WRAPPED_INDEX_FILE_PATH) SED_BEFORE_STRING=$(WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING) SED_AFTER_STRING=$(WRAPPED_INDEX_FILE_WITH_EXTERN_STRING), )
+
+_sed_file:
+	$(SMITHY_DAFNY_ROOT)/scripts/sed_replace.sh

TestModels/Aggregate/Makefile

@@ -3,6 +3,7 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
 RUST_BENERATED=1
 
 include ../SharedMakefile.mk
@@ -19,3 +20,16 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 # This project has no dependencies 
 # DEPENDENT-MODELS:= 
 
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleAggregateTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.aggregate.internaldafny.types\" } SimpleAggregateTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleAggregateTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.aggregate.internaldafny\"} SimpleAggregate refines AbstractSimpleAggregateService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleAggregate refines AbstractSimpleAggregateService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleAggregateImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.aggregate.internaldafny.wrapped\"} WrappedSimpleAggregateService refines WrappedAbstractSimpleAggregateService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleAggregateService refines WrappedAbstractSimpleAggregateService {"

TestModels/CodegenPatches/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \
@@ -22,3 +24,17 @@ clean: _clean
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleCodegenpatchesTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.codegenpatches.internaldafny.types\" } SimpleCodegenpatchesTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleCodegenpatchesTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.codegenpatches.internaldafny\" } CodegenPatches refines AbstractSimpleCodegenpatchesService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleCodegenpatches refines AbstractSimpleCodegenpatchesService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedCodegenPatchesImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.codegenpatches.internaldafny.wrapped\"} WrappedSimpleCodegenPatchesService refines WrappedAbstractSimpleCodegenpatchesService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleCodegenpatchesService refines WrappedAbstractSimpleCodegenpatchesService {"

TestModels/Constraints/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \
@@ -24,3 +26,17 @@ polymorph:
 	make polymorph_dafny
 	make polymorph_java
 	make polymorph_dotnet
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleConstraintsTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constraints.internaldafny.types\" } SimpleConstraintsTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleConstraintsTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constraints.internaldafny\" } SimpleConstraints refines AbstractSimpleConstraintsService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleConstraints refines AbstractSimpleConstraintsService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleConstraintsImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constraints.internaldafny.wrapped\"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {"

TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs

@@ -3,11 +3,14 @@
 using Wrappers_Compile;
 using Simple.Constraints;
 using Simple.Constraints.Wrapped;
-using TypeConversion = Simple.Constraints.TypeConversion ;
+using TypeConversion = Simple.Constraints.TypeConversion;
 namespace simple.constraints.internaldafny.wrapped
 {
-    public partial class __default {
-        public static _IResult<types.ISimpleConstraintsClient, types._IError> WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) {
+    public partial class __default
+    {
+        [System.Obsolete]
+        public static _IResult<types.ISimpleConstraintsClient, types._IError> WrappedSimpleConstraints(types._ISimpleConstraintsConfig config)
+        {
             var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_constraints__S23_SimpleConstraintsConfig(config);
             var impl = new SimpleConstraints(wrappedConfig);
             var wrappedClient = new SimpleConstraintsShim(impl);

TestModels/Constructor/Makefile

@@ -3,6 +3,7 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
 RUST_BENERATED=1
 
 include ../SharedMakefile.mk
@@ -20,3 +21,17 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 
 # This project has no dependencies 
 # DEPENDENT-MODELS:= 
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleConstructorTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constructor.internaldafny.types\" } SimpleConstructorTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleConstructorTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constructor.internaldafny\" } SimpleConstructor refines AbstractSimpleConstructorService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleConstructor refines AbstractSimpleConstructorService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleConstructorImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.constructor.internaldafny.wrapped\"} WrappedSimpleConstructorService refines WrappedAbstractSimpleConstructorService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleConstructorService refines WrappedAbstractSimpleConstructorService {"

TestModels/Dependencies/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \
@@ -39,3 +41,15 @@ clean: _clean
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
+
+TYPES_FILE_PATH=Model/SimpleDependenciesTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dependencies.internaldafny.types\" } SimpleDependenciesTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleDependenciesTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dependencies.internaldafny\" } SimpleDependencies refines AbstractSimpleDependenciesService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleDependencies refines AbstractSimpleDependenciesService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleDependenciesImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.dependencies.internaldafny.wrapped\"} WrappedSimpleDependenciesService refines WrappedAbstractSimpleDependenciesService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleDependenciesService refines WrappedAbstractSimpleDependenciesService {"

TestModels/Dependencies/runtimes/net/Extern/WrappedSimpleDependenciesService.cs

@@ -3,11 +3,13 @@
 using Wrappers_Compile;
 using Simple.Dependencies;
 using Simple.Dependencies.Wrapped;
-using TypeConversion = Simple.Dependencies.TypeConversion ;
+using TypeConversion = Simple.Dependencies.TypeConversion;
 namespace simple.dependencies.internaldafny.wrapped
 {
-    public partial class __default {
-        public static _IResult<types.ISimpleDependenciesClient, types._IError> WrappedSimpleDependencies(types._ISimpleDependenciesConfig config) {
+    public partial class __default
+    {
+        public static _IResult<types.ISimpleDependenciesClient, types._IError> WrappedSimpleDependencies(types._ISimpleDependenciesConfig config)
+        {
             var wrappedConfig = TypeConversion.FromDafny_N6_simple__N12_dependencies__S24_SimpleDependenciesConfig(config);
             var impl = new SimpleDependencies(wrappedConfig);
             var wrappedClient = new SimpleDependenciesShim(impl);

TestModels/Documentation/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \
@@ -18,3 +20,17 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 # DEPENDENT-MODELS:= 
 
 POLYMORPH_OPTIONS=--generate client-constructors,project-files
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleDocumentationTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.documentation.internaldafny.types\" } SimpleDocumentationTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleDocumentationTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.documentation.internaldafny\" } SimpleDocumentation refines AbstractSimpleDocumentationService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleDocumentation refines AbstractSimpleDocumentationService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleDocumentationImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:options \"--function-syntax:4\"} {:extern \"simple.documentation.internaldafny.wrapped\"} WrappedSimpleDocumentationService refines WrappedAbstractSimpleDocumentationService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module {:options \"--function-syntax:4\"} WrappedSimpleDocumentationService refines WrappedAbstractSimpleDocumentationService {"

TestModels/Errors/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefile.mk
 
 PROJECT_SERVICES := \
@@ -21,3 +23,17 @@ clean: _clean
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleErrorsTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.errors.internaldafny.types\" } SimpleErrorsTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleErrorsTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.errors.internaldafny\" } SimpleErrors refines AbstractSimpleErrorsService {"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleErrors refines AbstractSimpleErrorsService {"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleErrorsImpl.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.errors.internaldafny.wrapped\"} WrappedSimpleErrorsService refines WrappedAbstractSimpleErrorsService {"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleErrorsService refines WrappedAbstractSimpleErrorsService {"

TestModels/Errors/runtimes/net/Extern/WrappedSimpleErrorsService.cs

@@ -3,11 +3,14 @@
 using Wrappers_Compile;
 using Simple.Errors;
 using Simple.Errors.Wrapped;
-using TypeConversion = Simple.Errors.TypeConversion ;
+using TypeConversion = Simple.Errors.TypeConversion;
 namespace simple.errors.internaldafny.wrapped
 {
-    public partial class __default {
-        public static _IResult<types.ISimpleErrorsClient, types._IError> WrappedSimpleErrors(types._ISimpleErrorsConfig config) {
+    public partial class __default
+    {
+        [System.Obsolete]
+        public static _IResult<types.ISimpleErrorsClient, types._IError> WrappedSimpleErrors(types._ISimpleErrorsConfig config)
+        {
             var wrappedConfig = TypeConversion.FromDafny_N6_simple__N6_errors__S18_SimpleErrorsConfig(config);
             var impl = new SimpleErrors(wrappedConfig);
             var wrappedClient = new SimpleErrorsShim(impl);

TestModels/Extendable/Makefile

@@ -3,6 +3,8 @@
 
 CORES=2
 
+ENABLE_EXTERN_PROCESSING=1
+
 include ../SharedMakefile.mk
 
 NAMESPACE=simple.extendable.resources
@@ -27,3 +29,17 @@ clean: _clean
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 	rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
+
+# Constants for languages that drop extern names (Python, Go)
+
+TYPES_FILE_PATH=Model/SimpleExtendableResourcesTypes.dfy
+TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.extendable.resources.internaldafny.types\" } SimpleExtendableResourcesTypes"
+TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleExtendableResourcesTypes"
+
+INDEX_FILE_PATH=src/Index.dfy
+INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.extendable.resources.internaldafny\"} SimpleExtendableResources refines AbstractSimpleExtendableResourcesService"
+INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleExtendableResources refines AbstractSimpleExtendableResourcesService"
+
+WRAPPED_INDEX_FILE_PATH=src/WrappedIndex.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.extendable.resources.internaldafny.wrapped\"} WrappedSimpleExtendableResources refines WrappedAbstractSimpleExtendableResourcesService"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleExtendableResources refines WrappedAbstractSimpleExtendableResourcesService"