feat(Optimize Go imports): run goimports on Go target code

.github/workflows/integration-tests-reusable.yml

@@ -87,6 +87,22 @@ jobs:
  with:
  java-version: 18
  distribution: corretto
+ - name: Set up newest supported Go
+ if: matrix.target-language-version == 'newest'
+ uses: actions/setup-go@v4
+ with:
+ go-version: '1.20'
+ - name: Set up oldest supported Go
+ if: matrix.target-language-version != 'newest'
+ uses: actions/setup-go@v4
+ with:
+ go-version: '1.11'
+ - name: Set up goimports using GOPATH
+ if: matrix.target-language-version != 'newest'
+ run: go get golang.org/x/tools/cmd/goimports
+ - name: Set up goimports using GO MODULE
+ if: matrix.target-language-version == 'newest'
+ run: go install golang.org/x/tools/cmd/goimports@latest
  - name: Set up Python
  uses: actions/setup-python@v4
  with: 

.github/workflows/runtime-tests.yml

@@ -29,6 +29,12 @@ jobs:
  with:
  java-version: 18
  distribution: corretto
+ - name: Set up Go
+ uses: actions/setup-go@v4
+ with:
+ go-version: '1.20'
+ - name: Set up goimports
+ run: go install golang.org/x/tools/cmd/goimports@latest
  - name: Build Dafny
  run: dotnet build Source/Dafny.sln
  - name: Get Z3

.github/workflows/standard-libraries.yml

@@ -27,6 +27,12 @@ jobs:
  with:
  java-version: 18
  distribution: corretto
+ - name: Set up Go
+ uses: actions/setup-go@v4
+ with:
+ go-version: '1.20'
+ - name: Set up goimports
+ run: go install golang.org/x/tools/cmd/goimports@latest
  - name: Build Dafny
  run: dotnet build Source/Dafny.sln
  - name: Get Z3

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -90,9 +90,9 @@ SinglePassCompiler Compiler {
  }
  }
 
- public override void OnPostCompile() {
- base.OnPostCompile();
+ public override bool OnPostCompile(string dafnyProgramName, string targetFilename, TextWriter outputWriter) {
  Compiler.Coverage.WriteLegendFile();
+ return true;
  }
 
  protected abstract SinglePassCompiler CreateCompiler();

Source/DafnyCore/Compilers/GoLang/GoBackend.cs

@@ -23,6 +23,21 @@ protected override SinglePassCompiler CreateCompiler() {
  return new GoCompiler(Options, Reporter);
  }
 
+ public override bool OnPostCompile(string dafnyProgramName, string targetFilename, TextWriter outputWriter) {
+ return base.OnPostCompile(dafnyProgramName, targetFilename, outputWriter) && OptimizeImports(targetFilename, outputWriter);
+ }
+
+ public bool OptimizeImports(string targetFilename, TextWriter outputWriter) {
+ var goArgs = new List<string> {
+ "-w",
+ targetFilename
+ };
+
+ var psi = PrepareProcessStartInfo("goimports", goArgs);
+
+ return 0 == RunProcess(psi, outputWriter, outputWriter);
+ }
+
  public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain,
  string/*?*/ targetFilename, ReadOnlyCollection<string> otherFileNames,
  bool runAfterCompile, TextWriter outputWriter, out object compilationResult) {

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -57,8 +57,9 @@ protected override SinglePassCompiler CreateCompiler() {
  return null;
  }
 
- public override void OnPostCompile() {
+ public override bool OnPostCompile(string dafnyProgramName, string targetFilename, TextWriter outputWriter) {
  // Not calling base.OnPostCompile() since it references `compiler`
+ return true;
  }
 
  public override string PublicIdProtect(string name) {

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -128,9 +128,9 @@ public virtual void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<stri
  }
 
  /// <summary>
- /// Perform any required cleanups after generating code with <c>Compile</c> and <c>EmitCallToMain</c>.
+ /// Perform any required processing after generating code with <c>Compile</c> and <c>EmitCallToMain</c>.
  /// </summary>
- public virtual void OnPostCompile() { }
+ public abstract bool OnPostCompile(string dafnyProgramName, string targetFilename, TextWriter outputWriter);
 
  /// <summary>
  /// Remove previously generated source files. This is only applicable to compilers that put sources in a separate

Source/DafnyDriver/CompilerDriver.cs

@@ -535,8 +535,6 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
  Contract.Assert(hasMain == (callToMain != null));
  bool targetProgramHasErrors = dafnyProgram.Reporter.Count(ErrorLevel.Error) != oldErrorCount;
 
- compiler.OnPostCompile();
-
  // blurt out the code to a file, if requested, or if other target-language files were specified on the command line.
  var targetPaths = GenerateTargetPaths(options, dafnyProgramName);
  if (options.SpillTargetCode > 0 || otherFileNames.Count > 0 || (invokeCompiler && !compiler.SupportsInMemoryCompilation) ||
@@ -545,7 +543,7 @@ public static async Task<bool> CompileDafnyProgram(Program dafnyProgram, string
  WriteDafnyProgramToFiles(options, targetPaths, targetProgramHasErrors, targetProgramText, callToMain, otherFiles, outputWriter);
  }
 
- if (targetProgramHasErrors) {
+ if (targetProgramHasErrors || !compiler.OnPostCompile(dafnyProgramName, targetPaths.SourceDirectory, outputWriter)) {
  return false;
  }
  // If we got here, compilation succeeded
@@ -608,6 +606,9 @@ public override string PublicIdProtect(string name) {
  public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
  throw new NotSupportedException();
  }
+ public override bool OnPostCompile(string dafnyProgramName, string targetFilename, TextWriter outputWriter) {
+ throw new NotSupportedException();
+ }
 
  public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree) {
  throw new NotSupportedException();

Source/DafnyRuntime/DafnyRuntimeGo/System_/System_.go

@@ -4,47 +4,47 @@
 package _System
 
 import (
- _dafny "dafny"
- os "os"
+ _dafny "dafny"
+ os "os"
 )
+
 var _ _dafny.Dummy__
 var _ = os.Args
 
 type Dummy__ struct{}
 
-
 // Definition of class Nat
 type Nat struct {
 }
 
 func New_Nat_() *Nat {
- _this := Nat{}
+ _this := Nat{}
 
- return &_this
+ return &_this
 }
 
 type CompanionStruct_Nat_ struct {
 }
-var Companion_Nat_ = CompanionStruct_Nat_ {
-}
+
+var Companion_Nat_ = CompanionStruct_Nat_{}
 
 func (*Nat) String() string {
- return "_System.Nat"
+ return "_System.Nat"
 }
+
 // End of class Nat
 
 func Type_Nat_() _dafny.TypeDescriptor {
- return type_Nat_{}
+ return type_Nat_{}
 }
 
 type type_Nat_ struct {
 }
 
 func (_this type_Nat_) Default() interface{} {
- return _dafny.Zero
+ return _dafny.Zero
 }
 
 func (_this type_Nat_) String() string {
- return "_System.Nat"
+ return "_System.Nat"
 }
-