dafny: move to separate file

1 files changed, 61 insertions, 0 deletions

diff --git a/pkgs/applications/science/logic/dafny/default.nix b/pkgs/applications/science/logic/dafny/default.nix
new file mode 100644
index 0000000000000..962f9c8ae8cc2
--- /dev/null
+++ b/pkgs/applications/science/logic/dafny/default.nix
@@ -0,0 +1,61 @@
+{ lib
+, buildDotnetModule
+, fetchFromGitHub
+, writeScript
+, jdk11
+, z3
+}:
+
+buildDotnetModule rec {
+  pname = "Dafny";
+  version = "4.0.0";
+
+  src = fetchFromGitHub {
+    owner = "dafny-lang";
+    repo = "dafny";
+    rev = "v${version}";
+    sha256 = "sha256-7mVFDORbu9KsJ4IH8PrrpXE7xFrWVTyBmRaL8Kt/ghY=";
+  };
+
+  postPatch = ''
+    cp ${writeScript "fake-gradlew-for-dafny" ''
+      mkdir -p build/libs/
+      javac $(find -name "*.java" | grep "^./src/main") -d classes
+      jar cf build/libs/DafnyRuntime.jar -C classes dafny
+    ''} Source/DafnyRuntime/DafnyRuntimeJava/gradlew
+
+    # Needed to fix
+    # "error NETSDK1129: The 'Publish' target is not supported without specifying a target framework. The current project targets multiple frameworks, you must specify the framework for the published application."
+    substituteInPlace Source/DafnyRuntime/DafnyRuntime.csproj \
+      --replace TargetFrameworks TargetFramework \
+      --replace "netstandard2.0;net452" net6.0
+  '';
+
+  buildInputs = [ jdk11 ];
+  nugetDeps = ./deps.nix;
+
+  # Build just these projects. Building Source/Dafny.sln includes a bunch of
+  # unnecessary components like tests.
+  projectFile = [
+    "Source/Dafny/Dafny.csproj"
+    "Source/DafnyRuntime/DafnyRuntime.csproj"
+    "Source/DafnyLanguageServer/DafnyLanguageServer.csproj"
+  ];
+
+  executables = [ "Dafny" ];
+
+  # Help Dafny find z3
+  makeWrapperArgs = [ "--prefix PATH : ${lib.makeBinPath [ z3 ]}" ];
+
+  postFixup = ''
+    ln -s "$out/bin/Dafny" "$out/bin/dafny" || true
+  '';
+
+  meta = with lib; {
+    description = "A programming language with built-in specification constructs";
+    homepage = "https://research.microsoft.com/dafny";
+    maintainers = with maintainers; [ layus ];
+    license = licenses.mit;
+    platforms = with platforms; (linux ++ darwin);
+  };
+}