diff options
author | Alyssa Ross <hi@alyssa.is> | 2021-08-04 10:43:07 +0000 |
---|---|---|
committer | Alyssa Ross <hi@alyssa.is> | 2021-08-04 10:43:07 +0000 |
commit | 62614cbef7da005c1eda8c9400160f6bcd6546b8 (patch) | |
tree | c2630f69080637987b68acb1ee8676d2681fe304 /pkgs/applications/science/logic/z3 | |
parent | d9c82ed3044c72cecf01c6ea042489d30914577c (diff) | |
parent | e24069138dfec3ef94f211f1da005bb5395adc11 (diff) | |
download | nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.gz nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.bz2 nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.lz nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.xz nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.tar.zst nixpkgs-62614cbef7da005c1eda8c9400160f6bcd6546b8.zip |
Merge branch 'nixpkgs-update' into master
Diffstat (limited to 'pkgs/applications/science/logic/z3')
-rw-r--r-- | pkgs/applications/science/logic/z3/4.4.0.nix | 41 | ||||
-rw-r--r-- | pkgs/applications/science/logic/z3/default.nix | 66 | ||||
-rw-r--r-- | pkgs/applications/science/logic/z3/tptp.nix | 7 |
3 files changed, 90 insertions, 24 deletions
diff --git a/pkgs/applications/science/logic/z3/4.4.0.nix b/pkgs/applications/science/logic/z3/4.4.0.nix new file mode 100644 index 00000000000..9b7dabeb720 --- /dev/null +++ b/pkgs/applications/science/logic/z3/4.4.0.nix @@ -0,0 +1,41 @@ +{ lib, stdenv, fetchFromGitHub, python }: + +stdenv.mkDerivation rec { + name = "z3-${version}"; + version = "4.4.0"; + + src = fetchFromGitHub { + owner = "Z3Prover"; + repo = "z3"; + rev = "7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152"; + sha256 = "1xllvq9fcj4cz34biq2a9dn2sj33bdgrzyzkj26hqw70wkzv1kzx"; + }; + + buildInputs = [ python ]; + enableParallelBuilding = true; + + configurePhase = "python scripts/mk_make.py --prefix=$out && cd build"; + + # z3's install phase is stupid because it tries to calculate the + # python package store location itself, meaning it'll attempt to + # write files into the nix store, and fail. + soext = if stdenv.system == "x86_64-darwin" then ".dylib" else ".so"; + installPhase = '' + mkdir -p $out/bin $out/lib/${python.libPrefix}/site-packages $out/include + cp ../src/api/z3*.h $out/include + cp ../src/api/c++/z3*.h $out/include + cp z3 $out/bin + cp libz3${soext} $out/lib + cp libz3${soext} $out/lib/${python.libPrefix}/site-packages + cp z3*.pyc $out/lib/${python.libPrefix}/site-packages + cp ../src/api/python/*.py $out/lib/${python.libPrefix}/site-packages + ''; + + meta = { + description = "A high-performance theorem prover and SMT solver"; + homepage = "https://github.com/Z3Prover/z3"; + license = lib.licenses.mit; + platforms = lib.platforms.x86_64; + maintainers = with lib.maintainers; [ thoughtpolice ttuegel ]; + }; +} diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index 350a4f99af8..e482a071bb4 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -1,51 +1,77 @@ -{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames +{ lib +, 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; +with lib; stdenv.mkDerivation rec { pname = "z3"; - version = "4.8.8"; + version = "4.8.10"; src = fetchFromGitHub { - owner = "Z3Prover"; - repo = pname; - rev = "z3-${version}"; - sha256 = "1rn538ghqwxq0v8i6578j8mflk6fyv0cp4hjfqynzvinjbps56da"; + owner = "Z3Prover"; + repo = pname; + rev = "z3-${version}"; + sha256 = "1w1ym2l0gipvjx322npw7lhclv8rslq58gnj0d9i96masi3gbycf"; }; - buildInputs = [ python fixDarwinDylibNames ] ++ optional javaBindings jdk; + nativeBuildInputs = optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames; + buildInputs = [ python ] + ++ optional javaBindings jdk + ++ optionals ocamlBindings [ ocaml findlib zarith ] + ; propagatedBuildInputs = [ python.pkgs.setuptools ]; enableParallelBuilding = true; - configurePhase = concatStringsSep " " ( - [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ] - ++ optional javaBindings "--java" - ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}" - ) + "\n" + "cd build"; + 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"; postInstall = '' mkdir -p $dev $lib - mv $out/lib $lib/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" ]; + outputs = [ "out" "lib" "dev" "python" ] + ++ optional javaBindings "java" + ++ optional ocamlBindings "ocaml"; - meta = { + meta = with lib; { description = "A high-performance theorem prover and SMT solver"; - homepage = "https://github.com/Z3Prover/z3"; - license = stdenv.lib.licenses.mit; - platforms = stdenv.lib.platforms.x86_64; - maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; + homepage = "https://github.com/Z3Prover/z3"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ thoughtpolice ttuegel ]; }; } diff --git a/pkgs/applications/science/logic/z3/tptp.nix b/pkgs/applications/science/logic/z3/tptp.nix index 34449542abb..23136ddf7a7 100644 --- a/pkgs/applications/science/logic/z3/tptp.nix +++ b/pkgs/applications/science/logic/z3/tptp.nix @@ -1,4 +1,4 @@ -{stdenv, z3, cmake}: +{lib, stdenv, z3, cmake}: stdenv.mkDerivation rec { pname = "z3-tptp"; version = z3.version; @@ -23,9 +23,8 @@ stdenv.mkDerivation rec { ''; meta = { - inherit version; inherit (z3.meta) license homepage platforms; - description = ''TPTP wrapper for Z3 prover''; - maintainers = [stdenv.lib.maintainers.raskin]; + description = "TPTP wrapper for Z3 prover"; + maintainers = [lib.maintainers.raskin]; }; } |