ocamlPackages.z3: init at 4.8.9
This commit is contained in:
parent
0c56c7357f
commit
cc739e1c67
|
@ -1,10 +1,13 @@
|
|||
{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames
|
||||
, javaBindings ? false
|
||||
, ocamlBindings ? false
|
||||
, pythonBindings ? true
|
||||
, jdk ? null
|
||||
, ocaml ? null, findlib ? null, zarith ? null
|
||||
}:
|
||||
|
||||
assert javaBindings -> jdk != null;
|
||||
assert ocamlBindings -> ocaml != null && findlib != null && zarith != null;
|
||||
|
||||
with stdenv.lib;
|
||||
|
||||
|
@ -19,13 +22,22 @@ stdenv.mkDerivation rec {
|
|||
sha256 = "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx";
|
||||
};
|
||||
|
||||
buildInputs = [ python fixDarwinDylibNames ] ++ optional javaBindings jdk;
|
||||
buildInputs = [ python fixDarwinDylibNames ]
|
||||
++ optional javaBindings jdk
|
||||
++ optionals ocamlBindings [ ocaml findlib zarith ]
|
||||
;
|
||||
propagatedBuildInputs = [ python.pkgs.setuptools ];
|
||||
enableParallelBuilding = true;
|
||||
|
||||
postPatch = optionalString ocamlBindings ''
|
||||
export OCAMLFIND_DESTDIR=$ocaml/lib/ocaml/${ocaml.version}/site-lib
|
||||
mkdir -p $OCAMLFIND_DESTDIR/stublibs
|
||||
'';
|
||||
|
||||
configurePhase = concatStringsSep " " (
|
||||
[ "${python.interpreter} scripts/mk_make.py --prefix=$out" ]
|
||||
++ optional javaBindings "--java"
|
||||
++ optional ocamlBindings "--ml"
|
||||
++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}"
|
||||
) + "\n" + "cd build";
|
||||
|
||||
|
@ -39,7 +51,9 @@ stdenv.mkDerivation rec {
|
|||
ln -sf $lib/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary} $python/${python.sitePackages}/z3/lib/libz3${stdenv.hostPlatform.extensions.sharedLibrary}
|
||||
'';
|
||||
|
||||
outputs = [ "out" "lib" "dev" "python" ];
|
||||
outputs = [ "out" "lib" "dev" "python" ]
|
||||
++ optional ocamlBindings "ocaml"
|
||||
;
|
||||
|
||||
meta = {
|
||||
description = "A high-performance theorem prover and SMT solver";
|
||||
|
|
29
pkgs/development/ocaml-modules/z3/default.nix
Normal file
29
pkgs/development/ocaml-modules/z3/default.nix
Normal file
|
@ -0,0 +1,29 @@
|
|||
{ stdenv, ocaml, findlib, zarith, z3 }:
|
||||
|
||||
let z3-with-ocaml = z3.override {
|
||||
ocamlBindings = true;
|
||||
inherit ocaml findlib zarith;
|
||||
}; in
|
||||
|
||||
stdenv.mkDerivation {
|
||||
|
||||
pname = "ocaml${ocaml.version}-z3";
|
||||
inherit (z3-with-ocaml) version;
|
||||
|
||||
phases = [ "installPhase" "fixupPhase" ];
|
||||
|
||||
installPhase = ''
|
||||
runHook preInstall
|
||||
mkdir -p $OCAMLFIND_DESTDIR
|
||||
cp -r ${z3-with-ocaml.ocaml}/lib/ocaml/${ocaml.version}/site-lib/stublibs $OCAMLFIND_DESTDIR
|
||||
cp -r ${z3-with-ocaml.ocaml}/lib/ocaml/${ocaml.version}/site-lib/Z3 $OCAMLFIND_DESTDIR/z3
|
||||
runHook postInstall
|
||||
'';
|
||||
|
||||
buildInputs = [ findlib ];
|
||||
propagatedBuildInputs = [ zarith ];
|
||||
|
||||
meta = z3.meta // {
|
||||
description = "Z3 Theorem Prover (OCaml API)";
|
||||
};
|
||||
}
|
|
@ -993,6 +993,10 @@ let
|
|||
|
||||
yojson = callPackage ../development/ocaml-modules/yojson { };
|
||||
|
||||
z3 = callPackage ../development/ocaml-modules/z3 {
|
||||
inherit (pkgs) z3;
|
||||
};
|
||||
|
||||
zarith = callPackage ../development/ocaml-modules/zarith { };
|
||||
|
||||
zed = callPackage ../development/ocaml-modules/zed { };
|
||||
|
|
Loading…
Reference in a new issue