Apply java and kotlin source formatting

build.gradle.kts

@@ -11,6 +11,7 @@ plugins {
     // The Plugin Publish plugin will in turn auto-apply the Gradle Plugin Development Plugin (java-gradle-plugin)
     // and the Maven Publish plugin (maven-publish)
     id("com.gradle.plugin-publish") version "1.2.0"
+    id("com.diffplug.spotless") version "7.0.1"
 
     `maven-publish`
 }
@@ -32,28 +33,39 @@ dependencies {
 gradlePlugin {
     website.set("https://github.com/dafny-lang/dafny-gradle-plugin")
     vcsUrl.set("https://github.com/dafny-lang/dafny-gradle-plugin")
-            
+
     // Define the plugin
     plugins {
         create("org.dafny.dafny") {
             id = "org.dafny.dafny"
             implementationClass = "org.dafny.gradle.plugin.DafnyPlugin"
             displayName = "Gradle plugin for Dafny"
             description = "This plugin offers tight integration of the " +
-                    "Dafny verification-aware programming language with Java: " +
-                    "automatically verifying Dafny source code and compiling it to Java source code, " +
-                    "which the Java plugin will then build together with any hand-written Java in the project. " +
-                    "It also provides a robust approach to distributing and managing Dafny dependencies " +
-                    "through Gradle-supported repositories such as Maven Central."
+                "Dafny verification-aware programming language with Java: " +
+                "automatically verifying Dafny source code and compiling it to Java source code, " +
+                "which the Java plugin will then build together with any hand-written Java in the project. " +
+                "It also provides a robust approach to distributing and managing Dafny dependencies " +
+                "through Gradle-supported repositories such as Maven Central."
             tags.set(listOf("dafny", "verification", "building"))
         }
     }
 }
 
-// Add a source set for the functional test suite
-val functionalTestSourceSet = sourceSets.create("functionalTest") {
+spotless {
+    java {
+        googleJavaFormat()
+    }
+    kotlin {
+        target("**/*.kts")
+        ktlint()
+    }
 }
 
+// Add a source set for the functional test suite
+val functionalTestSourceSet =
+    sourceSets.create("functionalTest") {
+    }
+
 configurations["functionalTestImplementation"].extendsFrom(configurations["testImplementation"])
 
 // Add a task to run the functional tests

examples/java/build.gradle.kts

@@ -9,4 +9,4 @@ repositories {
 
 dafny {
     dafnyVersion.set("4.9.1")
-}
+}

examples/java/settings.gradle.kts

@@ -0,0 +1 @@
+// Empty file

examples/multi-project-incompatible/consumer/build.gradle.kts

@@ -12,4 +12,4 @@ dafny {
     dafnyVersion.set("4.9.1")
 
     optionsMap.put("unicode-char", true)
-}
+}

examples/multi-project-incompatible/producer/build.gradle.kts

@@ -12,4 +12,4 @@ dafny {
     dafnyVersion.set("4.9.1")
 
     optionsMap.put("unicode-char", false)
-}
+}

examples/multi-project-incompatible/settings.gradle.kts

@@ -8,6 +8,6 @@ pluginManagement {
         mavenLocal()
         // Uncomment these to use the published version of the plugin from your preferred source.
         // gradlePluginPortal()
-         mavenCentral()
+        mavenCentral()
     }
 }

examples/multi-project/settings.gradle.kts

@@ -8,6 +8,6 @@ pluginManagement {
         mavenLocal()
         // Uncomment these to use the published version of the plugin from your preferred source.
         // gradlePluginPortal()
-         mavenCentral()
+        mavenCentral()
     }
 }

examples/no-dafny/settings.gradle.kts

@@ -0,0 +1 @@
+// Empty file

examples/simple-verify/build.gradle.kts

@@ -9,4 +9,4 @@ repositories {
 
 dafny {
     dafnyVersion.set("4.9.1")
-}
+}

examples/simple-verify/settings.gradle.kts

@@ -0,0 +1 @@
+// Empty file

examples/using-standard-libraries/settings.gradle.kts

@@ -0,0 +1 @@
+// Empty file

examples/wrong-dafny-version/build.gradle.kts

@@ -9,4 +9,4 @@ repositories {
 
 dafny {
     dafnyVersion.set("2.3.0")
-}
+}

examples/wrong-dafny-version/settings.gradle.kts

@@ -0,0 +1 @@
+// Empty file

src/functionalTest/java/org/dafny/gradle/plugin/DafnyPluginFunctionalTest.java

@@ -5,123 +5,129 @@
 
 import java.io.File;
 import java.io.IOException;
-import java.io.Writer;
-import java.io.FileWriter;
-
-import org.gradle.api.GradleException;
-import org.gradle.testkit.runner.GradleRunner;
 import org.gradle.testkit.runner.BuildResult;
-import org.gradle.testkit.runner.UnexpectedBuildFailure;
+import org.gradle.testkit.runner.GradleRunner;
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
-import org.junit.jupiter.api.io.TempDir;
-import static org.junit.jupiter.api.Assertions.*;
 
-/**
- * A simple functional test for the 'dafny.gradle.plugin.greeting' plugin.
- */
+/** A simple functional test for the 'dafny.gradle.plugin.greeting' plugin. */
 class DafnyPluginFunctionalTest {
 
-    @Test
-    void canVerify() throws IOException {
-        BuildResult result = GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("build")
-                .withProjectDir(new File("examples/simple-verify"))
-                .buildAndFail();
+  @Test
+  void canVerify() throws IOException {
+    BuildResult result =
+        GradleRunner.create()
+            .forwardOutput()
+            .withPluginClasspath()
+            .withArguments("build")
+            .withProjectDir(new File("examples/simple-verify"))
+            .buildAndFail();
 
-        Assertions.assertTrue(result.getOutput().contains(
+    Assertions.assertTrue(
+        result
+            .getOutput()
+            .contains(
                 "examples/simple-verify/src/main/dafny/simple.dfy(2,9): Error: assertion might not hold"));
-        Assertions.assertTrue(result.getOutput().contains(
+    Assertions.assertTrue(
+        result
+            .getOutput()
+            .contains(
                 "examples/simple-verify/src/main/dafny/nested/simple.dfy(2,9): Error: assertion might not hold"));
-    }
-
-    @Test
-    void canReferenceDependencies() throws IOException {
-        GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("clean", "build")
-                .withProjectDir(new File("examples/multi-project"))
-                .build();
-    }
+  }
 
-    // Expected to fail because the producer and consumer use different values of
-    // --unicode-char
-    @Test
-    void failsOnIncompatibleDependencies() throws IOException {
-        BuildResult result = GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("clean", "build")
-                .withProjectDir(new File("examples/multi-project-incompatible"))
-                .buildAndFail();
-        Assertions.assertTrue(result.getOutput().contains(
-                "--unicode-char is set locally to True, but the library was built with False"));
-    }
+  @Test
+  void canReferenceDependencies() throws IOException {
+    GradleRunner.create()
+        .forwardOutput()
+        .withPluginClasspath()
+        .withArguments("clean", "build")
+        .withProjectDir(new File("examples/multi-project"))
+        .build();
+  }
 
-    @Test
-    void succeedsWithNoDafnySourceFiles() throws IOException {
+  // Expected to fail because the producer and consumer use different values of
+  // --unicode-char
+  @Test
+  void failsOnIncompatibleDependencies() throws IOException {
+    BuildResult result =
         GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("clean", "build")
-                .withProjectDir(new File("examples/no-dafny"))
-                .build();
-    }
+            .forwardOutput()
+            .withPluginClasspath()
+            .withArguments("clean", "build")
+            .withProjectDir(new File("examples/multi-project-incompatible"))
+            .buildAndFail();
+    Assertions.assertTrue(
+        result
+            .getOutput()
+            .contains(
+                "--unicode-char is set locally to True, but the library was built with False"));
+  }
 
-    @Test
-    void failsOnWrongDafnyVersion() throws IOException {
-        BuildResult result = GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("clean", "build")
-                .withProjectDir(new File("examples/wrong-dafny-version"))
-                .buildAndFail();
-        Assertions.assertTrue(result.getOutput().contains(
-                "Incorrect Dafny version: expected 2.3.0, found"));
-    }
+  @Test
+  void succeedsWithNoDafnySourceFiles() throws IOException {
+    GradleRunner.create()
+        .forwardOutput()
+        .withPluginClasspath()
+        .withArguments("clean", "build")
+        .withProjectDir(new File("examples/no-dafny"))
+        .build();
+  }
 
-    // Regression test: this previously failed because the standard libraries
-    // end up included in the .doo file,
-    // so passing `--standard-libraries` again when translating led to duplicate
-    // definitions.
-    // Dafny has addressed this by not including the standard libraries which
-    // building .doo files.
-    @Test
-    void supportsStandardLibraries() throws IOException {
+  @Test
+  void failsOnWrongDafnyVersion() throws IOException {
+    BuildResult result =
         GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("clean", "build")
-                .withProjectDir(new File("examples/using-standard-libraries"))
-                .build();
-    }
+            .forwardOutput()
+            .withPluginClasspath()
+            .withArguments("clean", "build")
+            .withProjectDir(new File("examples/wrong-dafny-version"))
+            .buildAndFail();
+    Assertions.assertTrue(
+        result.getOutput().contains("Incorrect Dafny version: expected 2.3.0, found"));
+  }
 
-    @Test
-    void convertsToJava() throws IOException {
-        var dir = new File("examples/java");
-        // N.B. This path is set in DafnyPlugin.java, then Dafny adds "-java" suffix
-        var expected = dir.toPath().resolve("build/generated/sources/fromDafny/java/main-java/Foo/Bar.java").toFile();
+  // Regression test: this previously failed because the standard libraries
+  // end up included in the .doo file,
+  // so passing `--standard-libraries` again when translating led to duplicate
+  // definitions.
+  // Dafny has addressed this by not including the standard libraries which
+  // building .doo files.
+  @Test
+  void supportsStandardLibraries() throws IOException {
+    GradleRunner.create()
+        .forwardOutput()
+        .withPluginClasspath()
+        .withArguments("clean", "build")
+        .withProjectDir(new File("examples/using-standard-libraries"))
+        .build();
+  }
 
-        // Clean build
-        GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("clean", "translateDafnyToJava")
-                .withProjectDir(dir)
-                .build();
-        Assertions.assertTrue(expected.exists());
-        var firstTime = expected.lastModified();
+  @Test
+  void convertsToJava() throws IOException {
+    var dir = new File("examples/java");
+    // N.B. This path is set in DafnyPlugin.java, then Dafny adds "-java" suffix
+    var expected =
+        dir.toPath()
+            .resolve("build/generated/sources/fromDafny/java/main-java/Foo/Bar.java")
+            .toFile();
 
-        // (Force) an incremental re-build, and check the modified time moved
-        GradleRunner.create()
-                .forwardOutput()
-                .withPluginClasspath()
-                .withArguments("translateDafnyToJava", "--rerun-tasks")
-                .withProjectDir(dir)
-                .build();
-        Assertions.assertTrue(expected.lastModified() > firstTime);
-    }
+    // Clean build
+    GradleRunner.create()
+        .forwardOutput()
+        .withPluginClasspath()
+        .withArguments("clean", "translateDafnyToJava")
+        .withProjectDir(dir)
+        .build();
+    Assertions.assertTrue(expected.exists());
+    var firstTime = expected.lastModified();
+
+    // (Force) an incremental re-build, and check the modified time moved
+    GradleRunner.create()
+        .forwardOutput()
+        .withPluginClasspath()
+        .withArguments("translateDafnyToJava", "--rerun-tasks")
+        .withProjectDir(dir)
+        .build();
+    Assertions.assertTrue(expected.lastModified() > firstTime);
+  }
 }