diff options
Diffstat (limited to 'pkgs/applications/science/logic')
26 files changed, 170 insertions, 76 deletions
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix index 6a20a68324f1e..6ac9dd64982f1 100644 --- a/pkgs/applications/science/logic/abc/default.nix +++ b/pkgs/applications/science/logic/abc/default.nix @@ -4,13 +4,13 @@ stdenv.mkDerivation rec { pname = "abc-verifier"; - version = "unstable-2022-11-09"; + version = "unstable-2023-02-04"; src = fetchFromGitHub { owner = "yosyshq"; repo = "abc"; - rev = "be9a35c0363174a7cef21d55ed80d92a9ef95ab1"; - hash = "sha256-IN9YgJONcC55N89OXMrMuNuznTdjXNWxR0IngH8OWC8="; + rev = "a8f0ef2368aa56b3ad20a52298a02e63b2a93e2d"; + hash = "sha256-48i6AKQhMG5hcnkS0vejOy1PqFbeb6FpU7Yx0rEvHDI="; }; nativeBuildInputs = [ cmake ]; diff --git a/pkgs/applications/science/logic/abella/default.nix b/pkgs/applications/science/logic/abella/default.nix index 3d752b7d7b931..1d0c72359cfcc 100644 --- a/pkgs/applications/science/logic/abella/default.nix +++ b/pkgs/applications/science/logic/abella/default.nix @@ -9,7 +9,9 @@ stdenv.mkDerivation rec { sha256 = "sha256-/eOiebMFHgrurtrSHPlgZO3xmmxBOUmyAzswXZLd3Yc="; }; - buildInputs = [ rsync ] ++ (with ocamlPackages; [ ocaml ocamlbuild findlib ]); + strictDeps = true; + + nativeBuildInputs = [ rsync ] ++ (with ocamlPackages; [ ocaml ocamlbuild findlib ]); installPhase = '' mkdir -p $out/bin diff --git a/pkgs/applications/science/logic/acgtk/default.nix b/pkgs/applications/science/logic/acgtk/default.nix index d4f0ac3e5044a..c627b8a3c8f5a 100644 --- a/pkgs/applications/science/logic/acgtk/default.nix +++ b/pkgs/applications/science/logic/acgtk/default.nix @@ -13,11 +13,19 @@ stdenv.mkDerivation { sha256 = "sha256-W/BDhbng5iYuiB7desMKvRtDFdhoaxiJNvNvtbLlA6E="; }; - buildInputs = [ dune_2 ] ++ (with ocamlPackages; [ - ocaml findlib ansiterminal cairo2 cmdliner fmt logs menhir menhirLib mtime sedlex yojson - ]); + strictDeps = true; - buildPhase = "dune build --profile=release"; + nativeBuildInputs = with ocamlPackages; [ menhir ocaml findlib dune_2 ]; + + buildInputs = with ocamlPackages; [ + ansiterminal cairo2 cmdliner fmt logs menhirLib mtime sedlex yojson + ]; + + buildPhase = '' + runHook preBuild + dune build --profile=release ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} + runHook postBuild + ''; installPhase = '' dune install --prefix $out --libdir $OCAMLFIND_DESTDIR diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix index 7077d56f8069b..75288b5ff80bf 100644 --- a/pkgs/applications/science/logic/alt-ergo/default.nix +++ b/pkgs/applications/science/logic/alt-ergo/default.nix @@ -9,8 +9,8 @@ let src = fetchFromGitHub { owner = "OCamlPro"; repo = pname; - rev = version; - sha256 = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc="; + rev = "refs/tags/${version}"; + hash = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc="; }; in diff --git a/pkgs/applications/science/logic/avy/default.nix b/pkgs/applications/science/logic/avy/default.nix index f6f43f1b0bb30..38fef51c56e6d 100644 --- a/pkgs/applications/science/logic/avy/default.nix +++ b/pkgs/applications/science/logic/avy/default.nix @@ -13,7 +13,7 @@ stdenv.mkDerivation rec { nativeBuildInputs = [ cmake ]; buildInputs = [ zlib boost.out boost.dev ]; - NIX_CFLAGS_COMPILE = toString ([ "-Wno-narrowing" ] + env.NIX_CFLAGS_COMPILE = toString ([ "-Wno-narrowing" ] # Squelch endless stream of warnings on same few things ++ lib.optionals stdenv.cc.isClang [ "-Wno-empty-body" diff --git a/pkgs/applications/science/logic/cbmc/default.nix b/pkgs/applications/science/logic/cbmc/default.nix index 4009761e8dc3c..ddfa999fcc7e3 100644 --- a/pkgs/applications/science/logic/cbmc/default.nix +++ b/pkgs/applications/science/logic/cbmc/default.nix @@ -13,13 +13,13 @@ stdenv.mkDerivation rec { pname = "cbmc"; - version = "5.74.0"; + version = "5.76.1"; src = fetchFromGitHub { owner = "diffblue"; repo = pname; rev = "${pname}-${version}"; - sha256 = "sha256-n4a/0Ak2psHDCXykVSPYavuIl22uq2ZP7LUcdSzg1ow="; + sha256 = "sha256-OVOoAfoqev33c7pIzBGK9HD+zgji/+BWKD33RYJaSDc="; }; nativeBuildInputs = [ @@ -60,9 +60,13 @@ stdenv.mkDerivation rec { --prefix PATH : "$out/share/cbmc" \ ''; - # fix "argument unused during compilation" - NIX_CFLAGS_COMPILE = lib.optionalString stdenv.cc.isClang - "-Wno-unused-command-line-argument"; + env.NIX_CFLAGS_COMPILE = toString (lib.optionals stdenv.cc.isGNU [ + # Needed with GCC 12 but breaks on darwin (with clang) + "-Wno-error=maybe-uninitialized" + ] ++ lib.optionals stdenv.cc.isClang [ + # fix "argument unused during compilation" + "-Wno-unused-command-line-argument" + ]); # TODO: add jbmc support cmakeFlags = [ "-DWITH_JBMC=OFF" "-Dsat_impl=cadical" "-Dcadical_INCLUDE_DIR=${cadical.dev}/include" ]; diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 8a40216c3ecba..49c9fc47fef26 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -66,10 +66,10 @@ let buildIde = args.buildIde or (!coqAtLeast "8.14"); ideFlags = optionalString (buildIde && !coqAtLeast "8.10") "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt"; - csdpPatch = if csdp != null then '' + csdpPatch = lib.optionalString (csdp != null) '' substituteInPlace plugins/micromega/sos.ml --replace "; csdp" "; ${csdp}/bin/csdp" substituteInPlace plugins/micromega/coq_micromega.ml --replace "System.is_in_system_path \"csdp\"" "true" - '' else ""; + ''; ocamlPackages = if !isNull customOCamlPackages then customOCamlPackages else with versions; switch coq-version [ { case = range "8.16" "8.17"; out = ocamlPackages_4_14; } @@ -91,7 +91,7 @@ self = stdenv.mkDerivation { passthru = { inherit coq-version; inherit ocamlPackages ocamlNativeBuildInputs; - inherit ocamlPropagatedBuildInputs ocamlPropagatedNativeBuildInputs; + inherit ocamlPropagatedBuildInputs; # For compatibility inherit (ocamlPackages) ocaml camlp5 findlib num ; emacsBufferSetup = pkgs: '' @@ -158,7 +158,7 @@ self = stdenv.mkDerivation { UNAME=$(type -tp uname) RM=$(type -tp rm) substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM" - ${if !coqAtLeast "8.7" then "substituteInPlace configure.ml --replace \"md5 -q\" \"md5sum\"" else ""} + ${lib.optionalString (!coqAtLeast "8.7") "substituteInPlace configure.ml --replace \"md5 -q\" \"md5sum\""} ${csdpPatch} ''; @@ -196,7 +196,7 @@ self = stdenv.mkDerivation { categories = [ "Development" "Science" "Math" "IDE" "GTK" ]; }); - postInstall = let suffix = if coqAtLeast "8.14" then "-core" else ""; in optionalString (!coqAtLeast "8.17") '' + postInstall = let suffix = optionalString (coqAtLeast "8.14") "-core"; in optionalString (!coqAtLeast "8.17") '' cp bin/votour $out/bin/ '' + '' ln -s $out/lib/coq${suffix} $OCAMLFIND_DESTDIR/coq${suffix} @@ -227,12 +227,12 @@ if coqAtLeast "8.17" then self.overrideAttrs(_: { buildPhase = '' runHook preBuild make dunestrap - dune build -p coq-core,coq-stdlib,coq,coqide-server${if buildIde then ",coqide" else ""} -j $NIX_BUILD_CORES + dune build -p coq-core,coq-stdlib,coq,coqide-server${lib.optionalString buildIde ",coqide"} -j $NIX_BUILD_CORES runHook postBuild ''; installPhase = '' runHook preInstall - dune install --prefix $out coq-core coq-stdlib coq coqide-server${if buildIde then " coqide" else ""} + dune install --prefix $out coq-core coq-stdlib coq coqide-server${lib.optionalString buildIde " coqide"} runHook postInstall ''; }) else self diff --git a/pkgs/applications/science/logic/cryptominisat/default.nix b/pkgs/applications/science/logic/cryptominisat/default.nix index 33de2d27dc90b..cd04d612b5290 100644 --- a/pkgs/applications/science/logic/cryptominisat/default.nix +++ b/pkgs/applications/science/logic/cryptominisat/default.nix @@ -1,32 +1,30 @@ -{ lib, stdenv, fetchFromGitHub, cmake, python3, xxd, boost, fetchpatch }: +{ lib +, stdenv +, fetchFromGitHub +, cmake +, python3 +, boost +}: stdenv.mkDerivation rec { pname = "cryptominisat"; - version = "5.8.0"; + version = "5.11.4"; src = fetchFromGitHub { - owner = "msoos"; - repo = "cryptominisat"; - rev = version; - sha256 = "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"; + owner = "msoos"; + repo = "cryptominisat"; + rev = version; + hash = "sha256-7JNfFKSYWgyyNnWNzXGLqWRwSW+5r6PBMelKeAmx8sc="; }; - patches = [ - (fetchpatch { - # https://github.com/msoos/cryptominisat/pull/621 - url = "https://github.com/msoos/cryptominisat/commit/11a97003b0bfbfb61ed6c4e640212110d390c28c.patch"; - sha256 = "0hdy345bwcbxz0jl1jdxfa6mmfh77s2pz9rnncsr0jzk11b3j0cw"; - }) - ]; - buildInputs = [ python3 boost ]; - nativeBuildInputs = [ cmake xxd ]; + nativeBuildInputs = [ cmake ]; meta = with lib; { description = "An advanced SAT Solver"; - homepage = "https://github.com/msoos/cryptominisat"; - license = licenses.mit; + homepage = "https://github.com/msoos/cryptominisat"; + license = licenses.mit; maintainers = with maintainers; [ mic92 ]; - platforms = platforms.unix; + platforms = platforms.unix; }; } diff --git a/pkgs/applications/science/logic/cryptoverif/default.nix b/pkgs/applications/science/logic/cryptoverif/default.nix index 195dd98aa3b4a..f056b3e433fbc 100644 --- a/pkgs/applications/science/logic/cryptoverif/default.nix +++ b/pkgs/applications/science/logic/cryptoverif/default.nix @@ -9,7 +9,9 @@ stdenv.mkDerivation rec { sha256 = "sha256-F5eVN5ATYo9Ivpi2eYh96ktuTWUeoqgWMR4BqHu8EFs="; }; - buildInputs = [ ocaml ]; + strictDeps = true; + + nativeBuildInputs = [ ocaml ]; /* Fix up the frontend to load the 'default' cryptoverif library ** from under $out/libexec. By default, it expects to find the files diff --git a/pkgs/applications/science/logic/cvc4/cvc4-bash-patsub-replacement.patch b/pkgs/applications/science/logic/cvc4/cvc4-bash-patsub-replacement.patch new file mode 100644 index 0000000000000..a97665c2f86c4 --- /dev/null +++ b/pkgs/applications/science/logic/cvc4/cvc4-bash-patsub-replacement.patch @@ -0,0 +1,39 @@ +Per https://bodhi.fedoraproject.org/updates/FEDORA-2022-dc47174c36: + +This update fixes a failure to build with source with bash 5.2. Bash's +`patsub_replacement` feature makes ampersand a special character when doing +variable substitution, which was not previously the case. This update instructs +bash to turn off the new behavior. + +The patch itself is adapted from +https://src.fedoraproject.org/rpms/cvc4/blob/f7c24c6ad72a8812d244313f13032fa23d393315/f/cvc4-bash-patsub-replacement.patch. +--- a/src/expr/mkexpr 2020-06-19 10:59:27.000000000 -0600 ++++ b/src/expr/mkexpr 2022-10-11 14:28:31.120453409 -0600 +@@ -16,6 +16,7 @@ + # + + copyright=2010-2014 ++shopt -u patsub_replacement + + filename=`basename "$1" | sed 's,_template,,'` + +--- a/src/expr/mkkind 2020-06-19 10:59:27.000000000 -0600 ++++ b/src/expr/mkkind 2022-10-11 14:34:17.008996126 -0600 +@@ -15,6 +15,7 @@ + # + + copyright=2010-2014 ++shopt -u patsub_replacement + + filename=`basename "$1" | sed 's,_template,,'` + +--- a/src/expr/mkmetakind 2020-06-19 10:59:27.000000000 -0600 ++++ b/src/expr/mkmetakind 2022-10-11 14:34:32.248020036 -0600 +@@ -18,6 +18,7 @@ + # + + copyright=2010-2014 ++shopt -u patsub_replacement + + cat <<EOF + /********************* */ diff --git a/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix index 873c3ca57c0c9..e9f04d2044dc7 100644 --- a/pkgs/applications/science/logic/cvc4/default.nix +++ b/pkgs/applications/science/logic/cvc4/default.nix @@ -28,6 +28,10 @@ stdenv.mkDerivation rec { patch -p1 -i ${./minisat-fenv.patch} -d src/prop/bvminisat ''; + patches = [ + ./cvc4-bash-patsub-replacement.patch + ]; + preConfigure = '' patchShebangs ./src/ ''; diff --git a/pkgs/applications/science/logic/cvc5/default.nix b/pkgs/applications/science/logic/cvc5/default.nix index 5bce776771d35..f0cb044b3beb3 100644 --- a/pkgs/applications/science/logic/cvc5/default.nix +++ b/pkgs/applications/science/logic/cvc5/default.nix @@ -1,18 +1,21 @@ -{ lib, stdenv, fetchFromGitHub, pkg-config, cmake, cadical, symfpu, gmp, git, python3, gtest, libantlr3c, antlr3_4, boost, jdk }: +{ lib, stdenv, fetchFromGitHub, pkg-config, cmake, flex, cadical, symfpu, gmp, python3, gtest, libantlr3c, antlr3_4, boost, jdk }: stdenv.mkDerivation rec { pname = "cvc5"; - version = "1.0.3"; + version = "1.0.4"; src = fetchFromGitHub { owner = "cvc5"; repo = "cvc5"; rev = "cvc5-${version}"; - sha256 = "sha256-CVXK6yehfUrSbo8R1Dk1oc/siCtmV9DjEp6q+aLuVQA="; + hash = "sha256-1yJZtPZ4nMg9Kn3jHpN8b5XeFZ8ZeVLrKYWh7Rp3/oQ="; }; - nativeBuildInputs = [ pkg-config cmake ]; - buildInputs = [ cadical.dev symfpu gmp git python3 python3.pkgs.toml gtest libantlr3c antlr3_4 boost jdk ]; + nativeBuildInputs = [ pkg-config cmake flex ]; + buildInputs = [ + cadical.dev symfpu gmp gtest libantlr3c antlr3_4 boost jdk + (python3.withPackages (ps: with ps; [ pyparsing toml ])) + ]; preConfigure = '' patchShebangs ./src/ diff --git a/pkgs/applications/science/logic/ekrhyper/default.nix b/pkgs/applications/science/logic/ekrhyper/default.nix index d6d9bb11a9a0a..187cbc9a92ae4 100644 --- a/pkgs/applications/science/logic/ekrhyper/default.nix +++ b/pkgs/applications/science/logic/ekrhyper/default.nix @@ -9,10 +9,8 @@ stdenv.mkDerivation rec { sha256 = "sha256-fEe0DIMGj7wO+79/BZf45kykgyTXpbZJsyFSt31XqpM="; }; - buildInputs = [ - ocaml - perl - ]; + strictDeps = true; + nativeBuildInputs = [ ocaml perl ]; setSourceRoot = "export sourceRoot=$(echo */ekrh/src/)"; preInstall = "export INSTALLDIR=$out"; postInstall = ''for i in "$out/casc"/*; do ln -s "$i" "$out/bin/ekrh-casc-$(basename $i)"; done ''; diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix index e66fe992e189a..4c105a40e20db 100644 --- a/pkgs/applications/science/logic/hol_light/default.nix +++ b/pkgs/applications/science/logic/hol_light/default.nix @@ -38,7 +38,9 @@ stdenv.mkDerivation { }) ]; - buildInputs = [ ocaml camlp5 ]; + strictDeps = true; + + nativeBuildInputs = [ ocaml camlp5 ]; propagatedBuildInputs = [ num ]; installPhase = '' diff --git a/pkgs/applications/science/logic/iprover/default.nix b/pkgs/applications/science/logic/iprover/default.nix index ff88586e0353b..6485681e3313f 100644 --- a/pkgs/applications/science/logic/iprover/default.nix +++ b/pkgs/applications/science/logic/iprover/default.nix @@ -9,7 +9,10 @@ stdenv.mkDerivation rec { sha256 = "0lik8p7ayhjwpkln1iwf0ri84ramhch74j5nj6z7ph6wfi92pgg8"; }; - buildInputs = [ ocaml eprover zlib ]; + strictDeps = true; + + nativeBuildInputs = [ ocaml eprover ]; + buildInputs = [ zlib ]; preConfigure = "patchShebangs ."; diff --git a/pkgs/applications/science/logic/klee/default.nix b/pkgs/applications/science/logic/klee/default.nix index 024e6e526c4e4..898e344f2a453 100644 --- a/pkgs/applications/science/logic/klee/default.nix +++ b/pkgs/applications/science/logic/klee/default.nix @@ -96,7 +96,7 @@ in stdenv.mkDerivation rec { ]; # Silence various warnings during the compilation of fortified bitcode. - NIX_CFLAGS_COMPILE = ["-Wno-macro-redefined"]; + env.NIX_CFLAGS_COMPILE = toString ["-Wno-macro-redefined"]; prePatch = '' patchShebangs . diff --git a/pkgs/applications/science/logic/leo2/default.nix b/pkgs/applications/science/logic/leo2/default.nix index cbc85c5544ccd..4087763aa0c54 100644 --- a/pkgs/applications/science/logic/leo2/default.nix +++ b/pkgs/applications/science/logic/leo2/default.nix @@ -9,8 +9,10 @@ stdenv.mkDerivation rec { sha256 = "sha256:1b2q7vsz6s9ighypsigqjm1mzjiq3xgnz5id5ssb4rh9zm190r82"; }; - nativeBuildInputs = [ makeWrapper ]; - buildInputs = [ eprover ocaml camlp4 perl zlib ]; + strictDeps = true; + + nativeBuildInputs = [ makeWrapper eprover ocaml camlp4 perl ]; + buildInputs = [ zlib ]; patches = [ (fetchpatch { url = "https://github.com/niklasso/minisat/commit/7eb6015313561a2586032574788fcb133eeaa19f.patch"; diff --git a/pkgs/applications/science/logic/ott/default.nix b/pkgs/applications/science/logic/ott/default.nix index bbc96b2b681cc..a00c565fb4e06 100644 --- a/pkgs/applications/science/logic/ott/default.nix +++ b/pkgs/applications/science/logic/ott/default.nix @@ -11,8 +11,11 @@ stdenv.mkDerivation rec { hash = "sha256-GzeEiok5kigcmfqf/K/UxvlKkl55zy0vOyiRZ2HyMiE="; }; - nativeBuildInputs = [ pkg-config opaline ]; - buildInputs = with ocamlPackages; [ ocaml findlib ocamlgraph ]; + + strictDeps = true; + + nativeBuildInputs = [ pkg-config opaline ] ++ (with ocamlPackages; [ findlib ocaml ]); + buildInputs = with ocamlPackages; [ ocamlgraph ]; installTargets = "ott.install"; diff --git a/pkgs/applications/science/logic/prooftree/default.nix b/pkgs/applications/science/logic/prooftree/default.nix index 2606b94f4bbb5..4e65c018d1a20 100644 --- a/pkgs/applications/science/logic/prooftree/default.nix +++ b/pkgs/applications/science/logic/prooftree/default.nix @@ -9,9 +9,10 @@ stdenv.mkDerivation rec { sha256 = "0z1z4wqbqwgppkh2bm89fgy07a0y2m6g4lvcyzs09sm1ysklk2dh"; }; - nativeBuildInputs = [ pkg-config ]; - buildInputs = [ ncurses ] ++ (with ocamlPackages; [ - ocaml findlib camlp5 lablgtk ]); + strictDeps = true; + + nativeBuildInputs = [ pkg-config ] ++ (with ocamlPackages; [ ocaml findlib camlp5 ]); + buildInputs = [ ncurses ] ++ (with ocamlPackages; [ lablgtk ]); dontAddPrefix = true; configureFlags = [ "--prefix" "$(out)" ]; diff --git a/pkgs/applications/science/logic/proverif/default.nix b/pkgs/applications/science/logic/proverif/default.nix index b6d15162fec35..57220aa523cf8 100644 --- a/pkgs/applications/science/logic/proverif/default.nix +++ b/pkgs/applications/science/logic/proverif/default.nix @@ -9,7 +9,9 @@ stdenv.mkDerivation rec { sha256 = "sha256:0xgwnp59779xc40sb7ck8rmfn620pilxyq79l3bymj9m7z0mwvm9"; }; - buildInputs = with ocamlPackages; [ ocaml findlib ]; + strictDeps = true; + + nativeBuildInputs = with ocamlPackages; [ ocaml findlib ]; buildPhase = "./build -nointeract"; installPhase = '' diff --git a/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix index 648ebee6550c0..af11cd0d6d8f9 100644 --- a/pkgs/applications/science/logic/satallax/default.nix +++ b/pkgs/applications/science/logic/satallax/default.nix @@ -3,8 +3,11 @@ stdenv.mkDerivation rec { pname = "satallax"; version = "2.7"; - nativeBuildInputs = [ makeWrapper ]; - buildInputs = [ ocaml zlib which eprover coq ]; + strictDeps = true; + + nativeBuildInputs = [ makeWrapper ocaml which eprover coq ]; + buildInputs = [ zlib ]; + src = fetchurl { url = "https://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${pname}-${version}.tar.gz"; sha256 = "1kvxn8mc35igk4vigi5cp7w3wpxk2z3bgwllfm4n3h2jfs0vkpib"; @@ -46,7 +49,7 @@ stdenv.mkDerivation rec { ''; # error: invalid suffix on literal; C++11 requires a space between literal and identifier - NIX_CFLAGS_COMPILE = lib.optionalString stdenv.isDarwin "-Wno-reserved-user-defined-literal"; + env.NIX_CFLAGS_COMPILE = lib.optionalString stdenv.isDarwin "-Wno-reserved-user-defined-literal"; installPhase = '' mkdir -p "$out/share/doc/satallax" "$out/bin" "$out/lib" "$out/lib/satallax" diff --git a/pkgs/applications/science/logic/statverif/default.nix b/pkgs/applications/science/logic/statverif/default.nix index 07365eef33fac..1f62389775517 100644 --- a/pkgs/applications/science/logic/statverif/default.nix +++ b/pkgs/applications/science/logic/statverif/default.nix @@ -14,7 +14,9 @@ stdenv.mkDerivation rec { sha256 = "113jjhi1qkcggbsmbw8fa9ln8vs7vy2r288szks7rn0jjn0wxmbw"; }; - buildInputs = [ ocaml ]; + strictDeps = true; + + nativeBuildInputs = [ ocaml ]; patchPhase = "patch -p1 < ${pf-patch}"; buildPhase = "./build"; diff --git a/pkgs/applications/science/logic/tlaplus/tlaps.nix b/pkgs/applications/science/logic/tlaplus/tlaps.nix index 14b3055ab36b0..59afbc094e40d 100644 --- a/pkgs/applications/science/logic/tlaplus/tlaps.nix +++ b/pkgs/applications/science/logic/tlaplus/tlaps.nix @@ -17,7 +17,9 @@ stdenv.mkDerivation rec { sha256 = "c296998acd14d5b93a8d5be7ee178007ef179957465966576bda26944b1b7fca"; }; - buildInputs = [ ocaml isabelle cvc3 perl wget which ]; + strictDeps = true; + + nativeBuildInputs = [ ocaml isabelle cvc3 perl wget which ]; installPhase = '' mkdir -pv "$out" diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix index 8ca2a6baa8890..55b59ff2e3b06 100644 --- a/pkgs/applications/science/logic/why3/default.nix +++ b/pkgs/applications/science/logic/why3/default.nix @@ -10,8 +10,16 @@ stdenv.mkDerivation rec { sha256 = "sha256-vNR7WeiSvg+763GcovoZBFDfncekJMeqNegP4fVw06I="; }; + strictDeps = true; + + nativeBuildInputs = with ocamlPackages; [ + ocaml findlib menhir + # Coq Support + coqPackages.coq + ]; + buildInputs = with ocamlPackages; [ - ocaml findlib ocamlgraph zarith menhir + ocamlgraph zarith # Emacs compilation of why3.el emacs # Documentation diff --git a/pkgs/applications/science/logic/yices/default.nix b/pkgs/applications/science/logic/yices/default.nix index fb14723241b81..83fbb6d6546b0 100644 --- a/pkgs/applications/science/logic/yices/default.nix +++ b/pkgs/applications/science/logic/yices/default.nix @@ -31,7 +31,7 @@ stdenv.mkDerivation rec { meta = with lib; { description = "A high-performance theorem prover and SMT solver"; - homepage = "http://yices.csl.sri.com"; + homepage = "https://yices.csl.sri.com"; license = licenses.gpl3; platforms = with platforms; linux ++ darwin; maintainers = with maintainers; [ thoughtpolice ]; diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index 75cfa2568f85a..f810a5a56739a 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -18,23 +18,26 @@ 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; }; - nativeBuildInputs = optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames; - buildInputs = [ python ] + strictDeps = true; + + nativeBuildInputs = [ python ] + ++ optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames ++ optional javaBindings jdk - ++ optionals ocamlBindings [ ocaml findlib zarith ] + ++ optionals ocamlBindings [ ocaml findlib ] ; - propagatedBuildInputs = [ python.pkgs.setuptools ]; + propagatedBuildInputs = [ python.pkgs.setuptools ] + ++ optionals ocamlBindings [ zarith ]; enableParallelBuilding = true; postPatch = optionalString ocamlBindings '' @@ -44,7 +47,7 @@ let common = { version, sha256, patches ? [ ] }: configurePhase = concatStringsSep " " ( - [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ] + [ "${python.pythonForBuild.interpreter} scripts/mk_make.py --prefix=$out" ] ++ optional javaBindings "--java" ++ optional ocamlBindings "--ml" ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}" @@ -92,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="; + }; } |