Commit 113cdbd2 authored by Ricardo M. Correia's avatar Ricardo M. Correia
Browse files

fstar: use proper z3 version and build .checked files

parent e75e7234

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

+7 −2
Original line number Diff line number Diff line
@@ -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

+3 −6
Original line number Diff line number Diff line
@@ -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

+5 −2
Original line number Diff line number Diff line
@@ -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 {};