From ccb2d83980f3a871cf603ff00234020dd1d38add Mon Sep 17 00:00:00 2001
From: Guillaume Maudoux <layus.on@gmail.com>
Date: Mon, 6 Feb 2017 22:41:01 +0100
Subject: [PATCH 1/2] boogie: fix basename issues; promote to package

---
 pkgs/top-level/all-packages.nix    | 2 ++
 pkgs/top-level/dotnet-packages.nix | 7 ++++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index d38479b26d5..299e4d1b846 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -17007,6 +17007,8 @@ with pkgs;
 
   aspino = callPackage ../applications/science/logic/aspino {};
 
+  boogie = dotnetPackages.Boogie;
+
   coq_8_3 = callPackage ../applications/science/logic/coq/8.3.nix {
     make = pkgs.gnumake3;
     inherit (ocamlPackages_3_12_1) ocaml findlib;
diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index c3d8b861c76..0e53e820a39 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -221,8 +221,9 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
   # SOURCE PACKAGES
 
   Boogie = buildDotnetPackage rec {
-    baseName = "Boogie-unstable";
+    baseName = "Boogie";
     version = "2017-01-03";
+    name = "${baseName}-unstable-${version}";
 
     src = fetchFromGitHub {
       owner = "boogie-org";
@@ -238,8 +239,8 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     outputFiles = [ "Binaries/*" ];
 
     postInstall = ''
-        mkdir -pv "$out/lib/dotnet/Boogie"
-        ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/Boogie/z3.exe"
+        mkdir -pv "$out/lib/dotnet/${baseName}"
+        ln -sv "${pkgs.z3}/bin/z3" "$out/lib/dotnet/${baseName}/z3.exe"
     '';
 
     meta = with stdenv.lib; {

From aeaf893e5733cb333256cb46f3925d69be103e38 Mon Sep 17 00:00:00 2001
From: Guillaume Maudoux <layus.on@gmail.com>
Date: Thu, 1 Sep 2016 09:36:56 +0200
Subject: [PATCH 2/2] dafny: init at v1.9.8

---
 pkgs/top-level/all-packages.nix    |  2 ++
 pkgs/top-level/dotnet-packages.nix | 45 ++++++++++++++++++++++++++++++
 2 files changed, 47 insertions(+)

diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 299e4d1b846..e1cad0b7810 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -16993,6 +16993,8 @@ with pkgs;
 
   ### SCIENCE/PROGRAMMING
 
+  dafny = dotnetPackages.Dafny;
+
   plm = callPackage ../applications/science/programming/plm { };
 
   ### SCIENCE/LOGIC
diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index 0e53e820a39..30267a5ad96 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -252,6 +252,51 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     };
   };
 
+  Dafny = buildDotnetPackage rec {
+    baseName = "Dafny";
+    version = "1.9.8";
+
+    src = fetchurl {
+      url = "https://github.com/Microsoft/dafny/archive/v${version}.tar.gz";
+      sha256 = "0n4pk4cv7d2zsn4xmyjlxvpfl9avq79r06c7kzmrng24p3k4qj6s";
+    };
+
+    preBuild = ''
+      ln -s ${pkgs.z3} Binaries/z3
+    '';
+
+    buildInputs = [ Boogie ];
+
+    xBuildFiles = [ "Source/Dafny.sln" ];
+    xBuildFlags = [ ];
+
+    outputFiles = [ "Binaries/*" ];
+
+    # Do not wrap the z3 executable, only dafny-related ones.
+    exeFiles = [ "Dafny*.exe" ];
+
+    # Dafny needs mono in its path.
+    makeWrapperArgs = "--set PATH ${mono}/bin";
+
+    # Boogie as an input is not enough. Boogie libraries need to be at the same
+    # place as Dafny ones. Same for "*.dll.mdb". No idea why or how to fix.
+    postFixup = ''
+      for lib in ${Boogie}/lib/dotnet/${Boogie.baseName}/*.dll{,.mdb}; do
+        ln -s $lib $out/lib/dotnet/${baseName}/
+      done
+      # We generate our own executable scripts
+      rm -f $out/lib/dotnet/${baseName}/dafny{,-server}
+    '';
+
+    meta = {
+      description = "A programming language with built-in specification constructs";
+      homepage = "http://research.microsoft.com/dafny";
+      maintainers = with maintainers; [ layus ];
+      license = licenses.MIT;
+      platforms = with platforms; (linux ++ darwin);
+    };
+  };
+
   Deedle = buildDotnetPackage rec {
     baseName = "Deedle";
     version = "1.2.0";