diff --git a/.github/workflows/gradle.yml b/.github/workflows/gradle.yml index cd8fdaa..f9b1036 100644 --- a/.github/workflows/gradle.yml +++ b/.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: diff --git a/examples/multi-project-incompatible/consumer/build.gradle.kts b/examples/multi-project-incompatible/consumer/build.gradle.kts index 63dbb6c..a7f18d0 100644 --- a/examples/multi-project-incompatible/consumer/build.gradle.kts +++ b/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) } \ No newline at end of file diff --git a/examples/multi-project-incompatible/producer/build.gradle.kts b/examples/multi-project-incompatible/producer/build.gradle.kts index b12c6cb..396cf77 100644 --- a/examples/multi-project-incompatible/producer/build.gradle.kts +++ b/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) } \ No newline at end of file diff --git a/examples/multi-project/consumer/build.gradle.kts b/examples/multi-project/consumer/build.gradle.kts index 1bbf47a..48291c9 100644 --- a/examples/multi-project/consumer/build.gradle.kts +++ b/examples/multi-project/consumer/build.gradle.kts @@ -3,7 +3,7 @@ plugins { } dafny { - dafnyVersion.set("4.9.0") + dafnyVersion.set("4.9.1") } dependencies { diff --git a/examples/multi-project/producer/build.gradle.kts b/examples/multi-project/producer/build.gradle.kts index 288d175..4d17af7 100644 --- a/examples/multi-project/producer/build.gradle.kts +++ b/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) } diff --git a/examples/no-dafny/build.gradle.kts b/examples/no-dafny/build.gradle.kts index d9d97c7..6ce8a9c 100644 --- a/examples/no-dafny/build.gradle.kts +++ b/examples/no-dafny/build.gradle.kts @@ -8,5 +8,5 @@ repositories { } dafny { - dafnyVersion.set("4.9.0") + dafnyVersion.set("4.9.1") } diff --git a/examples/simple-verify/build.gradle.kts b/examples/simple-verify/build.gradle.kts index 8fb977b..49b1c7c 100644 --- a/examples/simple-verify/build.gradle.kts +++ b/examples/simple-verify/build.gradle.kts @@ -8,5 +8,5 @@ repositories { } dafny { - dafnyVersion.set("4.9.0") + dafnyVersion.set("4.9.1") } \ No newline at end of file diff --git a/examples/using-standard-libraries/build.gradle.kts b/examples/using-standard-libraries/build.gradle.kts index 9b7329b..89fc497 100644 --- a/examples/using-standard-libraries/build.gradle.kts +++ b/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) -} \ No newline at end of file +} + +dependencies { + implementation("org.dafny:DafnyRuntime:4.9.0") +} diff --git a/src/functionalTest/java/org/dafny/gradle/plugin/DafnyPluginFunctionalTest.java b/src/functionalTest/java/org/dafny/gradle/plugin/DafnyPluginFunctionalTest.java index 1bfb8ec..91904dd 100644 --- a/src/functionalTest/java/org/dafny/gradle/plugin/DafnyPluginFunctionalTest.java +++ b/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)")); } } diff --git a/src/main/java/org/dafny/gradle/plugin/DafnyTranslateTask.java b/src/main/java/org/dafny/gradle/plugin/DafnyTranslateTask.java index 3181205..eac8fc8 100644 --- a/src/main/java/org/dafny/gradle/plugin/DafnyTranslateTask.java +++ b/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 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; - } }