Merge pull request #210627 from wizeman/u/fix-fstar

pkgs/applications/science/logic/z3/default.nix

@@ -18,14 +18,14 @@ assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
 
 with lib;
 
-let common = { version, sha256, patches ? [ ] }:
+let common = { version, sha256, patches ? [ ], tag ? "z3" }:
   stdenv.mkDerivation rec {
     pname = "z3";
     inherit version sha256 patches;
     src = fetchFromGitHub {
       owner = "Z3Prover";
       repo = pname;
-      rev = "z3-${version}";
+      rev = "${tag}-${version}";
       sha256 = sha256;
     };
 
@@ -95,4 +95,9 @@ in
     version = "4.8.15";
     sha256 = "0xkwqz0y5d1lfb6kfqy8wn8n2dqalzf4c8ghmjsajc1bpdl70yc5";
   };
+  z3_4_8_5 = common {
+    tag = "Z3";
+    version = "4.8.5";
+    sha256 = "sha256-ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
+  };
 }

pkgs/development/compilers/fstar/default.nix

@@ -14,6 +14,7 @@ stdenv.mkDerivation rec {
   strictDeps = true;
 
   nativeBuildInputs = [
+    z3
     makeWrapper
     installShellFiles
     removeReferencesTo
@@ -24,9 +25,7 @@ stdenv.mkDerivation rec {
     menhir
   ]);
 
-  buildInputs = [
-    z3
-  ] ++ (with ocamlPackages; [
+  buildInputs = with ocamlPackages; [
     batteries
     zarith
     stdint
@@ -39,12 +38,10 @@ stdenv.mkDerivation rec {
     ppx_deriving
     ppx_deriving_yojson
     process
-  ]);
+  ];
 
   makeFlags = [ "PREFIX=$(out)" ];
 
-  buildFlags = [ "libs" ];
-
   enableParallelBuilding = true;
 
   postPatch = ''

pkgs/top-level/all-packages.nix

@@ -14979,7 +14979,9 @@ with pkgs;
 
   fsharp = callPackage ../development/compilers/fsharp { };
 
-  fstar = callPackage ../development/compilers/fstar { };
+  fstar = callPackage ../development/compilers/fstar {
+    z3 = z3_4_8_5;
+  };
 
   dotnetPackages = recurseIntoAttrs (callPackage ./dotnet-packages.nix {});
 
@@ -37073,7 +37075,8 @@ with pkgs;
 
   inherit (callPackages ../applications/science/logic/z3 { python = python3; })
     z3_4_11
-    z3_4_8;
+    z3_4_8
+    z3_4_8_5;
   z3 = z3_4_8;
   z3-tptp = callPackage ../applications/science/logic/z3/tptp.nix {};