Improve dafny packaging (#300009)

NixOS · Dec 21, 2024 · d555634 · d555634
2 parents cd47784 + b2f59cd
commit d555634
Showing 1 changed file with 43 additions and 13 deletions.
diff --git a/pkgs/by-name/da/dafny/package.nix b/pkgs/by-name/da/dafny/package.nix
@@ -1,12 +1,41 @@
-{ lib
-, buildDotnetModule
-, fetchFromGitHub
-, writeScript
-, jdk11
-, z3
-, dotnetCorePackages
+{
+  lib,
+  buildDotnetModule,
+  fetchFromGitHub,
+  runCommand,
+  dafny,
+  writeScript,
+  jdk11,
+  z3,
+  dotnetCorePackages,
 }:
 
+let
+  examples = fetchFromGitHub {
+    owner = "gaberch";
+    repo = "Various-Algorithms-Verified-With-Dafny";
+    rev = "50e451bbcd15e52e27d5bbbf66b0b4c4abbff41c";
+    hash = "sha256-Ng5wve/4gQr/2hsFWUFFcTL3K2xH7dP9w8IrmvWMKyg=";
+  };
+
+  tests = {
+    verify = runCommand "dafny-test" { } ''
+      mkdir $out
+      cp ${examples}/SlowMax.dfy $out
+      ${dafny}/bin/dafny verify --allow-warnings $out/SlowMax.dfy
+    '';
+
+    # Broken, cannot compile generated .cs files for now
+    #run = runCommand "dafny-test" { } ''
+    #    mkdir $out
+    #    cp ${examples}/SlowMax.dfy $out
+    #    ${dafny}/bin/dafny run --allow-warnings $out/SlowMax.dfy
+    #  '';
+
+    # TODO: Ensure then tests that dafny can generate to and compile other
+    # languages (Java, Cpp, etc.)
+  };
+in
 buildDotnetModule rec {
   pname = "Dafny";
   version = "4.8.0";
@@ -24,12 +53,11 @@ buildDotnetModule rec {
       runtimeJarVersion = "4.6.0";
     in
     ''
-      cp ${
-        writeScript "fake-gradlew-for-dafny" ''
-          mkdir -p build/libs/
-          javac $(find -name "*.java" | grep "^./src/main") -d classes
-          jar cf build/libs/DafnyRuntime-${runtimeJarVersion}.jar -C classes dafny
-        ''} Source/DafnyRuntime/DafnyRuntimeJava/gradlew
+      cp ${writeScript "fake-gradlew-for-dafny" ''
+        mkdir -p build/libs/
+        javac $(find -name "*.java" | grep "^./src/main") -d classes
+        jar cf build/libs/DafnyRuntime-${runtimeJarVersion}.jar -C classes dafny
+      ''} Source/DafnyRuntime/DafnyRuntimeJava/gradlew
 
       # Needed to fix
       # "error NETSDK1129: The 'Publish' target is not supported without
@@ -62,6 +90,8 @@ buildDotnetModule rec {
     ln -s "$out/bin/Dafny" "$out/bin/dafny" || true
   '';
 
+  passthru.tests = tests;
+
   meta = with lib; {
     description = "Programming language with built-in specification constructs";
     homepage = "https://research.microsoft.com/dafny";