Go compiler emits unused imports to extern modules

[robin-aws]

To workaround the fact that the Go compiler considers unused imports an error, the Dafny to Go compiler inserts a reference to a Dummy__ symbol in each imported module. However, this is skipped for {:extern} modules under the assumption that such modules won't have that symbol, which means it's very easy to hit the Go compiler error.

It's not ideal to just have dafny pass the -unused_pkgs option to the Go compiler to suppress this error, because Go packages are usually distributed only as source and therefore consumers of Dafny-compiled Go would also have to disable this checking.

The solution is likely to only emit Go import statements for modules that are actually used. Requiring external modules define Dummy__ as well would break existing code bases and be a major inconvenience for importing existing Go modules into Dafny code.

[tchajed]

For what it's worth I've been fixing this by running goimports over the output of Dafny, which automatically removes unused imports. See this line in the Makefile. This runs after a bunch of other magic, including a script to make the output module aware and gofmt -r '(a) -> a' to remove unnecessary parentheses.

I would certainly find defining Dummy__ to be extremely inconvenient.