From 7769e32006a5af1155a862a96a7a2924243586a7 Mon Sep 17 00:00:00 2001
From: Guillaume Maudoux <layus.on@gmail.com>
Date: Tue, 3 Mar 2020 11:50:13 +0100
Subject: [PATCH 1/2] dafny: pin z3 and Boogie version

---
 pkgs/top-level/dotnet-packages.nix | 27 ++++++++++++++++++++-------
 1 file changed, 20 insertions(+), 7 deletions(-)

diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index f14ae3133b8..5c28b36763e 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -327,14 +327,14 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
 
   Boogie = buildDotnetPackage rec {
     baseName = "Boogie";
-    version = "2019-06-20";
-    name = "${baseName}-unstable-${version}";
+    version = "2.4.1";
+    name = "${baseName}-${version}";
 
     src = fetchFromGitHub {
       owner = "boogie-org";
       repo = "boogie";
-      rev = "2e8fae4dc1724d8f9e7b1f877116e56b0773337e";
-      sha256 = "01wjps3yfx8q0qy0zrmmfd1ixjxi2dhkn1wfazb5qm2slav39dp2";
+      rev = "v${version}";
+      sha256 = "13f6ifkh6gpy4bvx5zhgwmk3wd5rfxzl9wxwfhcj1c90fdrhwh1b";
     };
 
     # emulate `nuget restore Source/Boogie.sln`
@@ -379,7 +379,20 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     };
   };
 
-  Dafny = buildDotnetPackage rec {
+  Dafny = let
+    z3 = pkgs.z3.overrideAttrs (oldAttrs: with oldAttrs; rec {
+      version = "4.8.4";
+      name = "${pname}-${version}";
+
+      src = fetchFromGitHub {
+        owner = "Z3Prover";
+        repo = pname;
+        rev = "z3-${version}";
+        sha256 = "014igqm5vwswz0yhz0cdxsj3a6dh7i79hvhgc3jmmmz3z0xm1gyn";
+      };
+    });
+    boogie = assert dotnetPackages.Boogie.version == "2.4.1"; dotnetPackages.Boogie;
+  in buildDotnetPackage rec {
     baseName = "Dafny";
     version = "2.3.0";
 
@@ -396,7 +409,7 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     '';
 
     preBuild = ''
-      ln -s ${pkgs.z3} Binaries/z3
+      ln -s ${z3} Binaries/z3
     '';
 
     buildInputs = [ Boogie ];
@@ -415,7 +428,7 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     # 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
+      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

From 7b7efa47e769a06227ce151c1495dae3f1f01b3b Mon Sep 17 00:00:00 2001
From: Guillaume Maudoux <layus.on@gmail.com>
Date: Sat, 24 Oct 2020 17:03:20 +0200
Subject: [PATCH 2/2] dafny: use pinned z3 in the full closure

---
 pkgs/top-level/dotnet-packages.nix | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/pkgs/top-level/dotnet-packages.nix b/pkgs/top-level/dotnet-packages.nix
index 5c28b36763e..9c659e655e9 100644
--- a/pkgs/top-level/dotnet-packages.nix
+++ b/pkgs/top-level/dotnet-packages.nix
@@ -328,7 +328,6 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
   Boogie = buildDotnetPackage rec {
     baseName = "Boogie";
     version = "2.4.1";
-    name = "${baseName}-${version}";
 
     src = fetchFromGitHub {
       owner = "boogie-org";
@@ -380,18 +379,21 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
   };
 
   Dafny = let
-    z3 = pkgs.z3.overrideAttrs (oldAttrs: with oldAttrs; rec {
+    z3 = pkgs.z3.overrideAttrs (oldAttrs: rec {
       version = "4.8.4";
-      name = "${pname}-${version}";
+      name = "z3-${version}";
 
       src = fetchFromGitHub {
         owner = "Z3Prover";
-        repo = pname;
+        repo = "z3";
         rev = "z3-${version}";
         sha256 = "014igqm5vwswz0yhz0cdxsj3a6dh7i79hvhgc3jmmmz3z0xm1gyn";
       };
     });
-    boogie = assert dotnetPackages.Boogie.version == "2.4.1"; dotnetPackages.Boogie;
+    self' = pkgs.dotnetPackages.override ({
+      pkgs = pkgs // { inherit z3; };
+    });
+    Boogie = assert self'.Boogie.version == "2.4.1"; self'.Boogie;
   in buildDotnetPackage rec {
     baseName = "Dafny";
     version = "2.3.0";
@@ -428,7 +430,7 @@ let self = dotnetPackages // overrides; dotnetPackages = with self; {
     # 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
+      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