Skip to content

Commit

Permalink
Add explicit test of published dafny-lang/DafnyRuntimeGo
Browse files Browse the repository at this point in the history
  • Loading branch information
robin-aws committed Oct 15, 2024
1 parent fa543cc commit 25673bf
Show file tree
Hide file tree
Showing 4 changed files with 28 additions and 0 deletions.
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
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=
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";
}
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Hello World

0 comments on commit 25673bf

Please sign in to comment.