Dafny files in the src/dafny directory define modules as Dafny.* (e.g. Dafny.FileIO). But because the Dafny runtime also uses Dafny as a top-level namespace, compiling these Dafny files into Golang results in Go module name collisions (when the Go code compiled from Dafny, is passed to the Go compiler):
$ dafny build --target:go src/dafny/FileIO/FileIO.dfy
src/dafny/FileIO/FileIO-go/src/System_/System_.go:7:3: found packages Dafny (dafny.go) and dafny (dafnyFromDafny.go) in /<snip>/src/dafny/FileIO/FileIO-go/src/dafny
src/dafny/FileIO/FileIO-go/src/FileIO.go:10:3: found packages Dafny (dafny.go) and dafny (dafnyFromDafny.go) in /<snip>/src/dafny/FileIO/FileIO-go/src/Dafny
Dafny files in the
src/dafnydirectory define modules asDafny.*(e.g.Dafny.FileIO). But because the Dafny runtime also usesDafnyas a top-level namespace, compiling these Dafny files into Golang results in Go module name collisions (when the Go code compiled from Dafny, is passed to the Go compiler):