feat: Use semver4j to parse Dafny version and ignore build metadata (#13

)

Fixes #9

This allows you to just set dafnyVersion.set("4.9.1") instead of dafnyVersion.set("4.9.1+48e8bd498baaa0af79af008dbf0c34f14b9087b1") (as dafny --version currently outputs it)

Also updated the CI to test on the latest Dafny version. Would be worth testing on a range of supported Dafny versions soon as well.

.github/workflows/gradle.yml

@@ -20,10 +20,10 @@ jobs:
           java-version: '17'
           distribution: 'corretto'
       - name: Set up Dafny
-        uses: dafny-lang/setup-dafny-action@v1.6.1
+        uses: dafny-lang/setup-dafny-action@v1.8.0
         with:
-          dafny-version: "4.1.0"
+          dafny-version: "4.9.0"
       - name: Build with Gradle
         uses: gradle/gradle-build-action@v2
         with:
-          arguments: build
+          arguments: build --info --stacktrace

build.gradle.kts

@@ -7,8 +7,10 @@
  */
 
 plugins {
-    // Apply the Java Gradle plugin development plugin to add support for developing Gradle plugins
-    `java-gradle-plugin`
+    // Apply the Plugin Publish plugin to make plugin publication possible
+    // 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"
 
     `maven-publish`
 }
@@ -22,6 +24,7 @@ repositories {
 }
 
 dependencies {
+    implementation("org.semver4j:semver4j:5.4.1")
     // Use JUnit Jupiter for testing.
     testImplementation("org.junit.jupiter:junit-jupiter:5.9.1")
 }

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

@@ -5,12 +5,11 @@ plugins {
 dependencies {
     implementation(project(":producer"))
 
-    // TODO: Replace with 4.1.0 once released
-    implementation("org.dafny:DafnyRuntime:4.0.0")
+    implementation("org.dafny:DafnyRuntime:4.9.0")
 }
 
 dafny {
-    dafnyVersion.set("4.1.0")
+    dafnyVersion.set("4.9.0")
 
     optionsMap.put("unicode-char", true)
 }

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

@@ -5,12 +5,11 @@ plugins {
 }
 
 dependencies {
-    // TODO: Replace with 4.1.0 once released
-    implementation("org.dafny:DafnyRuntime:4.0.0")
+    implementation("org.dafny:DafnyRuntime:4.9.0")
 }
 
 dafny {
-    dafnyVersion.set("4.1.0")
+    dafnyVersion.set("4.9.0")
 
     optionsMap.put("unicode-char", false)
 }

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

@@ -3,12 +3,11 @@ plugins {
 }
 
 dafny {
-    dafnyVersion.set("4.1.0")
+    dafnyVersion.set("4.9.0")
 }
 
 dependencies {
     implementation(project(":producer"))
 
-    // TODO: Replace with 4.1.0 once released
-    implementation("org.dafny:DafnyRuntime:4.0.0")
+    implementation("org.dafny:DafnyRuntime:4.9.0")
 }

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

@@ -5,12 +5,11 @@ plugins {
 }
 
 dafny {
-    dafnyVersion.set("4.1.0")
+    dafnyVersion.set("4.9.0")
 
     optionsMap.put("function-syntax", 3)
 }
 
 dependencies {
-    // TODO: Replace with 4.1.0 once released
-    implementation("org.dafny:DafnyRuntime:4.0.0")
+    implementation("org.dafny:DafnyRuntime:4.9.0")
 }

examples/multi-project/producer/src/main/dafny/timesTwo.dfy

@@ -1,6 +1,6 @@
-module {:options "--function-syntax:4"} LibraryModule {
+module LibraryModule {
 
-  function TimesTwo(x: nat): nat {
+  function method TimesTwo(x: nat): nat {
     x * 2
   }
 }

examples/no-dafny/build.gradle.kts

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

examples/simple-verify/build.gradle.kts

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

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

@@ -31,9 +31,9 @@ class DafnyPluginFunctionalTest {
             .buildAndFail();
 
         Assertions.assertTrue(result.getOutput().contains(
-                "examples/simple-verify/src/main/dafny/simple.dfy(2,15): Error: assertion might not hold"));
+                "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,15): Error: assertion might not hold"));
+                "examples/simple-verify/src/main/dafny/nested/simple.dfy(2,9): Error: assertion might not hold"));
     }
 
     @Test void canReferenceDependencies() throws IOException {

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

@@ -4,6 +4,7 @@
 import org.gradle.api.provider.Property;
 import org.gradle.api.tasks.Input;
 import org.gradle.api.tasks.TaskAction;
+import org.semver4j.Semver;
 
 import java.io.IOException;
 import java.util.List;
@@ -18,9 +19,9 @@ public void checkVersion() throws IOException, InterruptedException {
         List<String> args = List.of("--version");
         DafnyCLIResult result = invokeDafnyCLI(args);
 
-        String expected = getRequiredVersion().get();
-        String actual = result.stdout().trim();
-        if (!expected.equals(actual)) {
+        Semver expected = Semver.parse(getRequiredVersion().get());
+        Semver actual = Semver.parse(result.stdout().trim());
+        if (!expected.isEquivalentTo(actual)) {
             throw new GradleException("Incorrect Dafny version: expected " + expected + ", found " + actual);
         }
     }