Merge branch 'master' into onlyClaimVerificationMemoryPerModule

dafny-lang · Oct 16, 2024 · 896f87b · 896f87b
2 parents e65de8d + 7f08159
commit 896f87b
Show file tree

Hide file tree

Showing 12 changed files with 41 additions and 14 deletions.
diff --git 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
@@ -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
@@ -1,3 +1,3 @@
-module github.com/dafny-lang/DafnyRuntimeGo
+module github.com/dafny-lang/DafnyRuntimeGo/v4
 
 go 1.21
diff --git a/...TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go b/...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
@@ -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
+replace github.com/dafny-lang/DafnyRuntimeGo/v4 v4.0.0-20231204230030-1d44519b5706 => ../DafnyRuntimeGo
diff --git 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
@@ -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/publishedruntime/go.mod 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
@@ -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
@@ -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";
+ }
+}
diff --git a/...tegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect b/...tegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect
@@ -0,0 +1 @@
+Hello World
diff --git 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