From d4f814d956f6d5b6d498cb0ce645d1bc3a87a1e1 Mon Sep 17 00:00:00 2001
From: whonore <wolfhonore@gmail.com>
Date: Sat, 29 Apr 2023 13:10:44 -0400
Subject: [PATCH] dafny: move to separate file

---
 .../science/logic/dafny/default.nix           | 61 +++++++++++++++++++
 .../science/logic/dafny/deps.nix}             |  0
 pkgs/top-level/all-packages.nix               |  2 +-
 pkgs/top-level/dotnet-packages.nix            | 54 ----------------
 4 files changed, 62 insertions(+), 55 deletions(-)
 create mode 100644 pkgs/applications/science/logic/dafny/default.nix
 rename pkgs/{development/dotnet-modules/dafny-deps.nix => applications/science/logic/dafny/deps.nix} (100%)

diff --git a/pkgs/applications/science/logic/dafny/default.nix b/pkgs/applications/science/logic/dafny/default.nix
new file mode 100644
index 000000000000..962f9c8ae8cc
--- /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);
+  };
+}
diff --git a/pkgs/development/dotnet-modules/dafny-deps.nix b/pkgs/applications/science/logic/dafny/deps.nix
similarity index 100%
rename from pkgs/development/dotnet-modules/dafny-deps.nix
rename to pkgs/applications/science/logic/dafny/deps.nix
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index ab2a07cf481e..9b6aeaae0574 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -37678,7 +37678,7 @@ with pkgs;
 
   ### SCIENCE/PROGRAMMING
 
-  dafny = dotnetPackages.Dafny;
+  dafny = callPackage ../applications/science/logic/dafny { };
 
   groove = callPackage ../applications/science/programming/groove { };
 
diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index 8789a82ec049..5445b9cbcb49 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -172,60 +172,6 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     };
   };
 
-  Dafny = buildDotnetModule rec {
-    pname = "Dafny";
-    version = "4.0.0";
-
-    src = fetchFromGitHub {
-      owner = "dafny-lang";
-      repo = "dafny";
-      rev = "v${version}";
-      sha256 = "sha256-7mVFDORbu9KsJ4IH8PrrpXE7xFrWVTyBmRaL8Kt/ghY=";
-    };
-
-    postPatch = ''
-      cp ${pkgs.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 = [ pkgs.jdk11 ];
-    nugetDeps = ../development/dotnet-modules/dafny-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);
-    };
-  };
-
   MonoAddins = buildDotnetPackage rec {
     pname = "Mono.Addins";
     version = "1.2";