No change needed any more!

.github/workflows/gradle.yml

@@ -22,7 +22,7 @@ jobs:
       - name: Set up Dafny
         uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
-          dafny-version: "4.9.0"
+          dafny-version: "4.9.1"
       - 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

@@ -8,7 +8,11 @@ repositories {
 }
 
 dafny {
-    dafnyVersion.set("4.9.0")
+    dafnyVersion.set("4.9.1")
 
     optionsMap.put("standard-libraries", true)
-}
+}
+
+dependencies {
+    implementation("org.dafny:DafnyRuntime:4.9.0")
+}

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")
@@ -80,13 +80,13 @@ class DafnyPluginFunctionalTest {
     // 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 {
-        BuildResult result = GradleRunner.create()
+        GradleRunner.create()
                 .forwardOutput()
                 .withPluginClasspath()
                 .withArguments("clean", "build")
                 .withProjectDir(new File("examples/using-standard-libraries"))
                 .build();
-        Assertions.assertTrue(result.getOutput().contains("Some(4)"));
     }
 }

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

@@ -34,7 +34,7 @@ public void translateToJava() throws IOException, InterruptedException {
         args.add("translate");
         args.add("java");
         args.add(dooFile.getPath());
-        args.addAll(Utils.getCommonArguments(getClasspath().get(), getOptionsForTranslate()));
+        args.addAll(Utils.getCommonArguments(getClasspath().get(), getOptions().get()));
 
         args.add("-o");
         args.add(outputDir.getPath());
@@ -45,19 +45,4 @@ public void translateToJava() throws IOException, InterruptedException {
         File outputDirWithJava = new File(outputDir.getParentFile(), outputDir.getName() + "-java");
         outputDirWithJava.renameTo(outputDir);
     }
-
-    private Map<String, Object> getOptionsForTranslate() {
-        // --standard-libraries needs special handling,
-        // since we first build a .doo file and then translate that.
-        // That means the standard library code is already in the source .doo file,
-        // and if we pass --standard-libraries against we end up with duplicate definitions.
-        //
-        // Note that there will also be options that can only be passed to `translate` and not `verify`.
-        // Rather than duplicate the metadata about which options apply to which command,
-        // we should generate a project file and pass it to Dafny,
-        // because then Dafny itself will select the applicable subset for us.
-        var options = new HashMap<>(getOptions().get());
-        options.remove("standard-libraries");
-        return options;
-    }
 }