From fa543cc2f0e6f12376e1c80048db049f566a515c Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 10 Oct 2024 17:28:38 -0700 Subject: [PATCH 1/2] Add /v4 to references to dafny-lang/DafnyRuntimeGo --- Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs | 3 +-- Source/DafnyRuntime/DafnyRuntimeGo-gomod/System_/System_.go | 2 +- Source/DafnyRuntime/DafnyRuntimeGo-gomod/go.mod | 2 +- .../multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go | 4 ++-- .../LitTests/LitTest/gomodule/multimodule/DafnyModule1/go.mod | 4 ++-- .../LitTest/gomodule/multimodule/DafnyModule1/test.go | 4 ++-- .../TestFiles/LitTests/LitTest/gomodule/multimodule/go.mod | 4 ++-- .../LitTests/LitTest/gomodule/singlemodule/dafnysource/go.mod | 4 ++-- 8 files changed, 13 insertions(+), 14 deletions(-) diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 7ee7455d38b..e3e9cd3b215 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -20,8 +20,7 @@ namespace Microsoft.Dafny.Compilers { class GoCodeGenerator : SinglePassCodeGenerator { protected override bool RequiresAllVariablesToBeUsed => true; - //TODO: This is tentative, update this to point to public module once available. - private string DafnyRuntimeGoModule = "github.com/dafny-lang/DafnyRuntimeGo/"; + private string DafnyRuntimeGoModule = "github.com/dafny-lang/DafnyRuntimeGo/v4/"; private bool GoModuleMode; private string GoModuleName; diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/System_/System_.go b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/System_/System_.go index 47efbe032b6..f2772409381 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/System_/System_.go +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/System_/System_.go @@ -6,7 +6,7 @@ package _System import ( os "os" - _dafny "github.com/dafny-lang/DafnyRuntimeGo/dafny" + _dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) var _ _dafny.Dummy__ diff --git a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/go.mod b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/go.mod index 5aa34e4cdcc..113f3e90309 100644 --- a/Source/DafnyRuntime/DafnyRuntimeGo-gomod/go.mod +++ b/Source/DafnyRuntime/DafnyRuntimeGo-gomod/go.mod @@ -1,3 +1,3 @@ -module github.com/dafny-lang/DafnyRuntimeGo +module github.com/dafny-lang/DafnyRuntimeGo/v4 go 1.21 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go index 36d7533ca2e..5a7cbef181d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go @@ -6,8 +6,8 @@ package DafnyModule1 import ( os "os" - _System "github.com/dafny-lang/DafnyRuntimeGo/System_" - _dafny "github.com/dafny-lang/DafnyRuntimeGo/dafny" + _System "github.com/dafny-lang/DafnyRuntimeGo/v4/System_" + _dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) var _ = os.Args diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/go.mod b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/go.mod index f30079ec90f..57a08d40f42 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/go.mod +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/go.mod @@ -2,6 +2,6 @@ module GoModule1 go 1.21 -require github.com/dafny-lang/DafnyRuntimeGo v0.0.0-20231204230030-1d44519b5706 +require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 -replace github.com/dafny-lang/DafnyRuntimeGo v0.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo \ No newline at end of file +replace github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/test.go b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/test.go index fb0a412a301..3c4daa57aa8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/test.go +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/test.go @@ -5,8 +5,8 @@ import ( DafnyModule1 "GoModule1/DafnyModule1" os "os" - _System "github.com/dafny-lang/DafnyRuntimeGo/System_" - _dafny "github.com/dafny-lang/DafnyRuntimeGo/dafny" + _System "github.com/dafny-lang/DafnyRuntimeGo/v4/System_" + _dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny" ) var _ = os.Args diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/go.mod b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/go.mod index 165af73f139..26efbdd330b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/go.mod +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/go.mod @@ -2,10 +2,10 @@ module GoModule2 go 1.21 -require github.com/dafny-lang/DafnyRuntimeGo v0.0.0-20231204230030-1d44519b5706 +require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 require GoModule1 v0.0.0 -replace github.com/dafny-lang/DafnyRuntimeGo v0.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo-gomod +replace github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo-gomod replace GoModule1 v0.0.0 => ./DafnyModule1 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/go.mod b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/go.mod index feb8522cff0..3d95a821d7b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/go.mod +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/go.mod @@ -2,6 +2,6 @@ module GoModule1 go 1.21 -require github.com/dafny-lang/DafnyRuntimeGo v0.0.0-20231204230030-1d44519b5706 +require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 -replace github.com/dafny-lang/DafnyRuntimeGo v0.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo-gomod +replace github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo-gomod From 25673bff8c321b920c126a4b644128e5443cc8ad Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 15 Oct 2024 12:26:59 -0700 Subject: [PATCH 2/2] Add explicit test of published dafny-lang/DafnyRuntimeGo --- .../LitTest/gomodule/publishedruntime/go.mod | 5 +++++ .../LitTest/gomodule/publishedruntime/go.sum | 2 ++ .../gomodule/publishedruntime/helloworld.dfy | 20 +++++++++++++++++++ .../publishedruntime/helloworld.dfy.expect | 1 + 4 files changed, 28 insertions(+) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.mod create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.sum create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect 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 00000000000..d7739bd404e --- /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 00000000000..6303870c71b --- /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 00000000000..5dd4410774a --- /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 00000000000..5e1c309dae7 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect @@ -0,0 +1 @@ +Hello World \ No newline at end of file