diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.mod b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.mod new file mode 100644 index 0000000000..d7739bd404 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.mod @@ -0,0 +1,5 @@ +module GoModule1 + +go 1.21 + +require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.sum b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.sum new file mode 100644 index 0000000000..6303870c71 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.sum @@ -0,0 +1,2 @@ +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0 h1:ttdCpTQKspK9A/tqE1qnipvjp9IrURS1kC2w47we6GM= +github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy new file mode 100644 index 0000000000..5dd4410774 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy @@ -0,0 +1,20 @@ +// This test consciously depends on the published version of the Go runtime +// at https://github.com/dafny-lang/DafnyRuntimeGo/v4, +// to ensure that copy works correctly. +// The other tests use `replace` directives to test against the local copy. +// That means if this test fails at some point because Dafny changes +// its compilation output, it may be necessary to +// publish a new tag on dafny-lang/DafnyRuntimeGo first before +// this test can pass, much less a new version of Dafny released. + +// RUN: %baredafny translate go --go-module-name=GoModule1 "%s" --output "%S/test" +// RUN: %cp -rf "%S/go.mod" "%S/test-go/go.mod" +// RUN: %cp -rf "%S/go.sum" "%S/test-go/go.sum" +// RUN: go run -C %S/test-go/ test.go > %t +// RUN: %diff "%s.expect" "%t" +module DafnyModule1 { + + method Main() { + print "Hello World"; + } +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect new file mode 100644 index 0000000000..5e1c309dae --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect @@ -0,0 +1 @@ +Hello World \ No newline at end of file