search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Top-level `Dafny` namespace collides with Dafny runtime #141

Open alex-chew opened 10 months ago

alex-chew commented 10 months ago

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
alex-chew commented 10 months ago

Instead of unifying the Dafny code in this repo under the Dafny namespace/module, we might want to use a name like Dafny.Lib or similar. In the same vein, we might also consider changing the Dafny runtime to use a namespace like Dafny.Runtime or similar (though perhaps the Dafny runtime is the most "deserving" of the unqualified Dafny namespace... but then again doing so would probably prevent similar issues down the line.)

Also, even though unifying library code under a single namespace is a good idea, and we'll want to keep the documentation that's been added in the src/dafny tree, we should be wary of having a second copy of the code without mechanisms to ensure it stays in sync and is maintained to our quality standards.

MikaelMayer commented 10 months ago

Good remarks. In a test branch, I'm also using a copy of the C# runtime in DafnyCore itself but in C#, namespaces don't conflict as in Go. Moreover, we use the namespace Microsoft.Dafny whereas the runtime can be accessed using global::Dafny.

Could this issue just be fixed in Go so that every other language does not have to deal with two different namespaces?