Modules with extern names containing periods produce malformed Go code

[robin-aws]

module {:extern "A.B"} A.B {}

$ dafny src/Scratch.dfy /compileTarget:go

Dafny program verifier finished with 0 verified, 0 errors
Wrote textual form of target program to Scratch-go/src/Scratch.go
Additional target code written to Scratch-go/src/dafny/dafny.go
Additional target code written to Scratch-go/src/System_/System_.go
Additional target code written to Scratch-go/src/A_Compile/A_Compile.go
src/Scratch-go/src/Scratch.go:7:4: expected 'STRING', found '.'

Scratch.go contains:

// Dafny program Scratch.dfy compiled into Go
package Scratch

import (
  _dafny "dafny"
  _System "System_"
  A.B "A.B"
  A_Compile "A_Compile"
)
var _ _dafny.Dummy__
var _ _System.Dummy__
var _ A_Compile.Dummy__

Arguably this isn't a bug, because this is literally the symbol the user asked for. The intent is just to disable the name mangling that normally adds _Compile, though. The given external name works for other target languages, and there doesn't seem to be a way to preserve the original name that does work for Go.

[cpitclaudel]

Note that you can write module {:extern "A", "A.B"} A.B {}, which produces A "A.B"

[robin-aws]

Apologies for leaving this open: we decided that it wasn't reasonable to expect a single {:extern} attribute to work over multiple languages, so this isn't a bug. See #4322 for a related feature we added instead.