fix: CI

smithy-lang · Oct 21, 2024 · fa6b4c6 · fa6b4c6
1 parent d874f1b
commit fa6b4c6
Show file tree

Hide file tree

Showing 14 changed files with 718 additions and 237 deletions.
diff --git a/TestModels/Dependencies/runtimes/go/TestsFromDafny-go/go.mod b/TestModels/Dependencies/runtimes/go/TestsFromDafny-go/go.mod
@@ -20,9 +20,6 @@ require (
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Dependencies v0.0.0 => ../ImplementationFromDafny-go
 
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
-
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Constraints v0.0.0 => ../../../../Constraints/runtimes/go/ImplementationFromDafny-go

diff --git a/...go/ExternConstructor/ExternConstructor.go → ...nFromDafny-go/ExternConstructor/extern.go b/...go/ExternConstructor/ExternConstructor.go → ...nFromDafny-go/ExternConstructor/extern.go
@@ -3,10 +3,9 @@ package ExternConstructor
 import (
 	"fmt"
 
-	"github.com/Smithy-dafny/TestModels/Extern/simpledafnyexterninternaldafnytypes"
-	"github.com/Smithy-dafny/TestModels/Extern/simpledafnyexterntypes"
-	"github.com/dafny-lang/DafnyRuntimeGo/dafny"
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
 	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+	"github.com/smithy-lang/smithy-dafny/TestModels/Extern/SimpleDafnyExternTypes"
 )
 
 type ExternConstructorClass struct {
@@ -25,9 +24,9 @@ var Companion_ExternConstructorClass_ = CompanionStruct_ExternConstructorClass_{
 func (CompanionStruct_ExternConstructorClass_) Build(input dafny.Sequence) Wrappers.Result {
 	if input.Equals(dafny.SeqOfChars([]dafny.Char("Error")...)) {
 		return Wrappers.Companion_Result_.Create_Failure_(
-			simpledafnyexterninternaldafnytypes.Companion_Error_.Create_Opaque_(simpledafnyexterntypes.OpaqueError{
-				ErrObject: fmt.Errorf("Exception"),
-			}))
+			SimpleDafnyExternTypes.Companion_Error_.Create_Opaque_(
+				fmt.Errorf("Exception"), dafny.SeqOfChars([]dafny.Char("ExceptionMessage")...)),
+		)
 	}
 	return Wrappers.Companion_Result_.Create_Success_(&ExternConstructorClass{func() *string {
 		var s string

diff --git a/TestModels/Extern/runtimes/go/ImplementationFromDafny-go/SimpleExternImpl/extern.go b/TestModels/Extern/runtimes/go/ImplementationFromDafny-go/SimpleExternImpl/extern.go
@@ -0,0 +1,21 @@
+package SimpleExternImpl
+
+import (
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+	"github.com/smithy-lang/smithy-dafny/TestModels/Extern/SimpleDafnyExternTypes"
+)
+
+func (CompanionStruct_Default___) GetExtern(c Config, input SimpleDafnyExternTypes.GetExternInput) Wrappers.Result {
+	return Wrappers.Companion_Result_.Create_Success_(SimpleDafnyExternTypes.Companion_GetExternOutput_.Create_GetExternOutput_(input.Dtor_blobValue(),
+		input.Dtor_booleanValue(),
+		input.Dtor_stringValue(),
+		input.Dtor_integerValue(),
+		input.Dtor_longValue()))
+
+}
+func (CompanionStruct_Default___) ExternMustError(c Config, input SimpleDafnyExternTypes.ExternMustErrorInput) Wrappers.Result {
+	return Wrappers.Companion_Result_.Create_Failure_(
+		SimpleDafnyExternTypes.Companion_Error_.Create_Opaque_(
+			input.Dtor_value(), dafny.SeqOfChars([]dafny.Char("ExceptionMessage")...)))
+}
diff --git a/TestModels/Extern/runtimes/go/ImplementationFromDafny-go/go.mod b/TestModels/Extern/runtimes/go/ImplementationFromDafny-go/go.mod
@@ -2,11 +2,9 @@ module github.com/smithy-lang/smithy-dafny/TestModels/Extern
 
 go 1.23.0
 
-require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
-
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
diff --git a/TestModels/Extern/runtimes/go/SimpleExternImpl/SimpleExternImpl.go b/TestModels/Extern/runtimes/go/SimpleExternImpl/SimpleExternImpl.go
diff --git a/TestModels/Extern/runtimes/go/TestsFromDafny-go/WrappedSimpleExternService/shim.go b/TestModels/Extern/runtimes/go/TestsFromDafny-go/WrappedSimpleExternService/shim.go
diff --git a/TestModels/Extern/runtimes/go/TestsFromDafny-go/go.mod b/TestModels/Extern/runtimes/go/TestsFromDafny-go/go.mod
@@ -5,13 +5,10 @@ go 1.23.0
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
 require (
-	github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/smithy-lang/smithy-dafny/TestModels/Extern v0.0.0
 )
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Extern v0.0.0 => ../ImplementationFromDafny-go
 
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
-
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
diff --git a/TestModels/aws-sdks/ddbv2/Makefile b/TestModels/aws-sdks/ddbv2/Makefile
@@ -51,6 +51,14 @@ PYTHON_MODULE_NAME=com_amazonaws_dynamodb
 TRANSLATION_RECORD_PYTHON := \
     --translation-record ../../dafny-dependencies/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/generated/dafny_src-py.dtr
 
+GO_MODULE_NAME="github.com/smithy-lang/smithy-dafny/ddbv2"
+
+GO_DEPENDENCY_MODULE_NAMES := \
+	--dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \
+
+TRANSLATION_RECORD_GO := \
+	dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
+
 # Constants for languages that drop extern names (Python, Go)
 
 TYPES_FILE_PATH=Model/ComAmazonawsDynamodbTypes.dfy