feat: Allow --standard-libraries

.github/workflows/gradle.yml

@@ -22,7 +22,9 @@ jobs:
       - name: Set up Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: "4.9.0"
+          # Using a nightly for now because --standard-libraries
+          # doesn't work without an unreleased fix
+          dafny-version: "nightly-2024-12-19-7df92c2"
       - name: Build with Gradle
         uses: gradle/gradle-build-action@v2
         with:

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

@@ -9,7 +9,7 @@ dependencies {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 
     optionsMap.put("unicode-char", true)
 }

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

@@ -9,7 +9,7 @@ dependencies {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 
     optionsMap.put("unicode-char", false)
 }

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

@@ -3,7 +3,7 @@ plugins {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 }
 
 dependencies {

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

@@ -5,7 +5,7 @@ plugins {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 
     optionsMap.put("function-syntax", 3)
 }

examples/no-dafny/build.gradle.kts

@@ -8,5 +8,5 @@ repositories {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 }

examples/simple-verify/build.gradle.kts

@@ -8,5 +8,5 @@ repositories {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 }

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

@@ -0,0 +1,18 @@
+plugins {
+    id("org.dafny.dafny")
+}
+
+repositories {
+    mavenLocal()
+    mavenCentral()
+}
+
+dafny {
+    dafnyVersion.set("4.9.1")
+
+    optionsMap.put("standard-libraries", true)
+}
+
+dependencies {
+    implementation("org.dafny:DafnyRuntime:4.9.0")
+}

examples/using-standard-libraries/src/main/dafny/UsesStdLibs.dfy

@@ -0,0 +1,7 @@
+
+import opened Std.Wrappers
+import opened Std.Collections.Seq
+
+method Main() {
+  print IndexOfOption([1, 1, 2, 3, 5, 8, 13, 21], 5);
+}

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

@@ -37,7 +37,7 @@ class DafnyPluginFunctionalTest {
     }
 
     @Test void canReferenceDependencies() throws IOException {
-        BuildResult result = GradleRunner.create()
+        GradleRunner.create()
             .forwardOutput()
             .withPluginClasspath()
             .withArguments("clean", "build")
@@ -58,7 +58,7 @@ class DafnyPluginFunctionalTest {
     }
 
     @Test void succeedsWithNoDafnySourceFiles() throws IOException {
-        BuildResult result = GradleRunner.create()
+        GradleRunner.create()
             .forwardOutput()
             .withPluginClasspath()
             .withArguments("clean", "build")
@@ -76,4 +76,17 @@ class DafnyPluginFunctionalTest {
         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 {
+        GradleRunner.create()
+                .forwardOutput()
+                .withPluginClasspath()
+                .withArguments("clean", "build")
+                .withProjectDir(new File("examples/using-standard-libraries"))
+                .build();
+    }
 }

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

@@ -9,7 +9,9 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 
 public abstract class DafnyTranslateTask extends DafnyBaseTask {