From 113cdbd29d6b90bf430a0e32364cd9ed8775d25f Mon Sep 17 00:00:00 2001
From: "Ricardo M. Correia" <rcorreia@wizy.org>
Date: Sat, 14 Jan 2023 03:37:45 +0000
Subject: [PATCH] fstar: use proper z3 version and build .checked files

---
 pkgs/applications/science/logic/z3/default.nix | 9 +++++++--
 pkgs/development/compilers/fstar/default.nix   | 9 +++------
 pkgs/top-level/all-packages.nix                | 7 +++++--
 3 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
index 928c0b6abebc..9ad48e79c933 100644
--- a/pkgs/applications/science/logic/z3/default.nix
+++ b/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=";
+  };
 }
diff --git a/pkgs/development/compilers/fstar/default.nix b/pkgs/development/compilers/fstar/default.nix
index 748869ea63c5..a21aa31ef407 100644
--- a/pkgs/development/compilers/fstar/default.nix
+++ b/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 = ''
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 8ad2ba05d011..401d0c042981 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -14861,7 +14861,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 {});
 
@@ -36876,7 +36878,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 {};