z3-tptp: init

Z3 ships a TPTP-supporting wrapper as an example; allow building it
This commit is contained in:
Michael Raskin 2019-01-22 16:50:30 +01:00
parent f3e2348805
commit ebb370f680
2 changed files with 32 additions and 0 deletions

View File

@ -0,0 +1,31 @@
{stdenv, z3, cmake}:
stdenv.mkDerivation rec {
pname = "z3-tptp";
version = z3.version;
src = z3.src;
sourceRoot = "source/examples/tptp";
nativeBuildInputs = [cmake];
buildInputs = [z3];
preConfigure = ''
echo 'set(Z3_LIBRARIES "-lz3")' >> CMakeLists.new
cat CMakeLists.txt | grep -E 'add_executable|project|link_libraries' >> CMakeLists.new
mv CMakeLists.new CMakeLists.txt
'';
installPhase = ''
mkdir -p "$out/bin"
cp "z3_tptp5" "$out/bin/"
ln -s "z3_tptp5" "$out/bin/z3-tptp"
'';
meta = {
inherit version;
inherit (z3.meta) license homepage platforms;
description = ''TPTP wrapper for Z3 prover'';
maintainers = [stdenv.lib.maintainers.raskin];
};
}

View File

@ -21949,6 +21949,7 @@ in
};
z3 = callPackage ../applications/science/logic/z3 { python = python2; };
z3-tptp = callPackage ../applications/science/logic/z3/tptp.nix {};
tlaplus = callPackage ../applications/science/logic/tlaplus {};
tlaps = callPackage ../applications/science/logic/tlaplus/tlaps.nix {