diff --git a/pkgs/by-name/da/dafny/package.nix b/pkgs/by-name/da/dafny/package.nix index d0fd3c1db9350..54f88b7b36c63 100644 --- 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";