Fix incremental build Java generation. (#16)

Translate task is requested to put generated source into a target
directory "main", however dafny actually places it into a directory
callled "main-java" and the translate task performs a rename at the
end to compensate. The problem is this rename can fail, for example
on an incremental build, when the target directory already exists.

Instead keep "main-java" as target and pass this modified target
onto subsequent gradle tasks as new source to be compiled.

examples/java/build.gradle.kts

@@ -0,0 +1,12 @@
+plugins {
+    id("org.dafny.dafny")
+}
+
+repositories {
+    mavenLocal()
+    mavenCentral()
+}
+
+dafny {
+    dafnyVersion.set("4.9.1")
+}

examples/java/src/main/dafny/Foo.dfy

@@ -0,0 +1,5 @@
+module Foo {
+  datatype Bar = Create(baz: string) {
+    const x: string := baz
+  }
+}

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

@@ -22,71 +22,106 @@
  */
 class DafnyPluginFunctionalTest {
 
-    @Test void canVerify() throws IOException {
+    @Test
+    void canVerify() throws IOException {
         BuildResult result = GradleRunner.create()
-            .forwardOutput()
-            .withPluginClasspath()
-            .withArguments("build")
-            .withProjectDir(new File("examples/simple-verify"))
-            .buildAndFail();
+                .forwardOutput()
+                .withPluginClasspath()
+                .withArguments("build")
+                .withProjectDir(new File("examples/simple-verify"))
+                .buildAndFail();
 
         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(
                 "examples/simple-verify/src/main/dafny/nested/simple.dfy(2,9): Error: assertion might not hold"));
     }
 
-    @Test void canReferenceDependencies() throws IOException {
+    @Test
+    void canReferenceDependencies() throws IOException {
         GradleRunner.create()
-            .forwardOutput()
-            .withPluginClasspath()
-            .withArguments("clean", "build")
-            .withProjectDir(new File("examples/multi-project"))
-            .build();
+                .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 {
+    // 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();
+                .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 succeedsWithNoDafnySourceFiles() throws IOException {
+    @Test
+    void succeedsWithNoDafnySourceFiles() throws IOException {
         GradleRunner.create()
-            .forwardOutput()
-            .withPluginClasspath()
-            .withArguments("clean", "build")
-            .withProjectDir(new File("examples/no-dafny"))
-            .build();
+                .forwardOutput()
+                .withPluginClasspath()
+                .withArguments("clean", "build")
+                .withProjectDir(new File("examples/no-dafny"))
+                .build();
     }
 
-    @Test void failsOnWrongDafnyVersion() throws IOException {
+    @Test
+    void failsOnWrongDafnyVersion() throws IOException {
         BuildResult result = GradleRunner.create()
-            .forwardOutput()
-            .withPluginClasspath()
-            .withArguments("clean", "build")
-            .withProjectDir(new File("examples/wrong-dafny-version"))
-            .buildAndFail();
+                .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"));
     }
 
     // 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 {
+    // 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();
     }
+
+    @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();
+
+        // 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);
+    }
 }

src/main/java/org/dafny/gradle/plugin/DafnyPlugin.java

@@ -74,7 +74,8 @@ public void apply(Project project) {
 
         // Register the Dafny-generated code to be compiled
         JavaPluginExtension javaExt = project.getExtensions().findByType(JavaPluginExtension.class);
-        javaExt.getSourceSets().findByName("main").getJava().srcDir(translatedJavaDir);
+        // Annoyingly, Dafny adds "-java" to the supplied directory name
+        javaExt.getSourceSets().findByName("main").getJava().srcDir(new File(translatedJavaDir.getPath() + "-java"));
 
         // Make sure the Dafny-generated code is generated before compiling
         project.getTasks().withType(JavaCompile.class, javaCompile ->

src/main/java/org/dafny/gradle/plugin/DafnyTranslateTask.java

@@ -40,9 +40,5 @@ public void translateToJava() throws IOException, InterruptedException {
         args.add(outputDir.getPath());
 
         invokeDafnyCLI(args);
-
-        // Annoyingly, Dafny adds "-java" to the directory, so rename it
-        File outputDirWithJava = new File(outputDir.getParentFile(), outputDir.getName() + "-java");
-        outputDirWithJava.renameTo(outputDir);
     }
 }