mirror of
https://github.com/NixOS/nixpkgs.git
synced 2025-02-09 21:53:24 +00:00
2bfa93e01c
It won't be enough to fix cross in all cases, but it is in at least one: pywayland. I've only made the change in cases I'm confident it's correct, as it would be wrong to change this when python.interpreter is used in wrappers, and possibly when it's used for running tests.
104 lines
2.9 KiB
Nix
104 lines
2.9 KiB
Nix
{ lib
|
|
, stdenv
|
|
, fetchFromGitHub
|
|
, python
|
|
, fixDarwinDylibNames
|
|
, javaBindings ? false
|
|
, ocamlBindings ? false
|
|
, pythonBindings ? true
|
|
, jdk ? null
|
|
, ocaml ? null
|
|
, findlib ? null
|
|
, zarith ? null
|
|
, writeScript
|
|
}:
|
|
|
|
assert javaBindings -> jdk != null;
|
|
assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
|
|
|
|
with lib;
|
|
|
|
let common = { version, sha256, patches ? [ ], tag ? "z3" }:
|
|
stdenv.mkDerivation rec {
|
|
pname = "z3";
|
|
inherit version sha256 patches;
|
|
src = fetchFromGitHub {
|
|
owner = "Z3Prover";
|
|
repo = pname;
|
|
rev = "${tag}-${version}";
|
|
sha256 = sha256;
|
|
};
|
|
|
|
strictDeps = true;
|
|
|
|
nativeBuildInputs = [ python ]
|
|
++ optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames
|
|
++ optional javaBindings jdk
|
|
++ optionals ocamlBindings [ ocaml findlib ]
|
|
;
|
|
propagatedBuildInputs = [ python.pkgs.setuptools ]
|
|
++ optionals ocamlBindings [ zarith ];
|
|
enableParallelBuilding = true;
|
|
|
|
postPatch = optionalString ocamlBindings ''
|
|
export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
|
|
mkdir -p $OCAMLFIND_DESTDIR/stublibs
|
|
'';
|
|
|
|
configurePhase = concatStringsSep " "
|
|
(
|
|
[ "${python.pythonForBuild.interpreter} scripts/mk_make.py --prefix=$out" ]
|
|
++ optional javaBindings "--java"
|
|
++ optional ocamlBindings "--ml"
|
|
++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}"
|
|
) + "\n" + "cd build";
|
|
|
|
doCheck = true;
|
|
checkPhase = ''
|
|
make test
|
|
./test-z3 -a
|
|
'';
|
|
|
|
postInstall = ''
|
|
mkdir -p $dev $lib
|
|
mv $out/lib $lib/lib
|
|
mv $out/include $dev/include
|
|
'' + optionalString pythonBindings ''
|
|
mkdir -p $python/lib
|
|
mv $lib/lib/python* $python/lib/
|
|
ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
|
|
'' + optionalString javaBindings ''
|
|
mkdir -p $java/share/java
|
|
mv com.microsoft.z3.jar $java/share/java
|
|
moveToOutput "lib/libz3java.${stdenv.hostPlatform.extensions.sharedLibrary}" "$java"
|
|
'';
|
|
|
|
outputs = [ "out" "lib" "dev" "python" ]
|
|
++ optional javaBindings "java"
|
|
++ optional ocamlBindings "ocaml";
|
|
|
|
meta = with lib; {
|
|
description = "A high-performance theorem prover and SMT solver";
|
|
homepage = "https://github.com/Z3Prover/z3";
|
|
license = licenses.mit;
|
|
platforms = platforms.unix;
|
|
maintainers = with maintainers; [ thoughtpolice ttuegel ];
|
|
};
|
|
};
|
|
in
|
|
{
|
|
z3_4_11 = common {
|
|
version = "4.11.0";
|
|
sha256 = "sha256-ItmtZHDhCeLAVtN7K80dqyAh20o7TM4xk2sTb9QgHvk=";
|
|
};
|
|
z3_4_8 = common {
|
|
version = "4.8.15";
|
|
sha256 = "0xkwqz0y5d1lfb6kfqy8wn8n2dqalzf4c8ghmjsajc1bpdl70yc5";
|
|
};
|
|
z3_4_8_5 = common {
|
|
tag = "Z3";
|
|
version = "4.8.5";
|
|
sha256 = "sha256-ytG5O9HczbIVJAiIGZfUXC/MuYH7d7yLApaeTRlKXoc=";
|
|
};
|
|
}
|