Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add /v4 to references to dafny-lang/DafnyRuntimeGo #5826

Merged
merged 3 commits into from
Oct 15, 2024
Merged

Add /v4 to references to dafny-lang/DafnyRuntimeGo #5826

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fa543cc
Add /v4 to references to dafny-lang/DafnyRuntimeGo
robin-aws Oct 11, 2024
25673bf
Add explicit test of published dafny-lang/DafnyRuntimeGo
robin-aws Oct 15, 2024
b284122
Merge branch 'master' into fix-go-runtime-module-path
robin-aws Oct 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyRuntime/DafnyRuntimeGo-gomod/System_/System_.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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__
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyRuntime/DafnyRuntimeGo-gomod/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
module github.com/dafny-lang/DafnyRuntimeGo
module github.com/dafny-lang/DafnyRuntimeGo/v4

go 1.21
4 changes: 2 additions & 2 deletions ...TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/DafnyModule1/DafnyModule1.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/DafnyModule1/test.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/multimodule/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
5 changes: 5 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module GoModule1

go 1.21

require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
2 changes: 2 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/go.sum
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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=
20 changes: 20 additions & 0 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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";
}
}
1 change: 1 addition & 0 deletions ...tegrationTests/TestFiles/LitTests/LitTest/gomodule/publishedruntime/helloworld.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Hello World
4 changes: 2 additions & 2 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/gomodule/singlemodule/dafnysource/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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