diff options
Diffstat (limited to 'pkgs/applications/science/logic')
26 files changed, 205 insertions, 144 deletions
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix index a33cc92c7ce..29d727d988e 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 = "2020.03.05"; + version = "2020.06.22"; src = fetchFromGitHub { owner = "berkeley-abc"; repo = "abc"; - rev = "ed90ce20df9c7c4d6e1db5d3f786f9b52e06bab1"; - sha256 = "01sw67pkrb6wzflkxbkxzwsnli3nvp0yxwp3j1ngb3c0j86ri437"; + rev = "341db25668f3054c87aa3372c794e180f629af5d"; + sha256 = "14cgv34vz5ljkcms6nrv19vqws2hs8bgjgffk5q03cbxnm2jxv5s"; }; nativeBuildInputs = [ cmake ]; diff --git a/pkgs/applications/science/logic/boolector/cmake-gtest.patch b/pkgs/applications/science/logic/boolector/cmake-gtest.patch new file mode 100644 index 00000000000..61a64d3abbb --- /dev/null +++ b/pkgs/applications/science/logic/boolector/cmake-gtest.patch @@ -0,0 +1,16 @@ +diff --git a/cmake/googletest-download.cmake b/cmake/googletest-download.cmake +index 0ec4d558..d0910313 100644 +--- a/cmake/googletest-download.cmake ++++ b/cmake/googletest-download.cmake +@@ -9,10 +9,7 @@ ExternalProject_Add( + googletest + SOURCE_DIR "@GOOGLETEST_DOWNLOAD_ROOT@/googletest-src" + BINARY_DIR "@GOOGLETEST_DOWNLOAD_ROOT@/googletest-build" +- GIT_REPOSITORY +- https://github.com/google/googletest.git +- GIT_TAG +- release-1.10.0 ++ URL REPLACEME + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND "" diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix index 105e911ed4f..aedc8e3484a 100644 --- a/pkgs/applications/science/logic/boolector/default.nix +++ b/pkgs/applications/science/logic/boolector/default.nix @@ -1,37 +1,31 @@ -{ stdenv, fetchFromGitHub, fetchpatch -, cmake, lingeling, btor2tools +{ stdenv, fetchFromGitHub, lib, python3 +, cmake, lingeling, btor2tools, gtest, gmp }: stdenv.mkDerivation rec { pname = "boolector"; - version = "3.0.0"; + version = "3.2.1"; src = fetchFromGitHub { owner = "boolector"; repo = "boolector"; rev = "refs/tags/${version}"; - sha256 = "15i3ni5klss423m57wcy1gx0m5wfrjmglapwg85pm7fb3jj1y7sz"; + sha256 = "0jkmaw678njqgkflzj9g374yk1mci8yqvsxkrqzlifn6bwhwb7ci"; }; - patches = [ - (fetchpatch { - name = "CVE-2019-7560.patch"; - url = "https://github.com/Boolector/boolector/commit/8d979d02e0482c7137c9f3a34e6d430dbfd1f5c5.patch"; - sha256 = "1a1g02mk8b0azzjcigdn5zpshn0dn05fciwi8sd5q38yxvnvpbbi"; - }) - ]; + postPatch = '' + sed s@REPLACEME@file://${gtest.src}@ ${./cmake-gtest.patch} | patch -p1 + ''; nativeBuildInputs = [ cmake ]; - buildInputs = [ lingeling btor2tools ]; + buildInputs = [ lingeling btor2tools gmp ]; cmakeFlags = - [ "-DSHARED=ON" + [ "-DBUILD_SHARED_LIBS=ON" "-DUSE_LINGELING=YES" - "-DBTOR2_INCLUDE_DIR=${btor2tools.dev}/include" - "-DBTOR2_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so" - "-DLINGELING_INCLUDE_DIR=${lingeling.dev}/include" - "-DLINGELING_LIBRARIES=${lingeling.lib}/lib/liblgl.a" - ]; + "-DBtor2Tools_INCLUDE_DIR=${btor2tools.dev}/include" + "-DBtor2Tools_LIBRARIES=${btor2tools.lib}/lib/libbtor2parser.so" + ] ++ (lib.optional (gmp != null) "-DUSE_GMP=YES"); installPhase = '' mkdir -p $out/bin $lib/lib $dev/include @@ -39,13 +33,22 @@ stdenv.mkDerivation rec { cp -vr bin/* $out/bin cp -vr lib/* $lib/lib - rm -rf $out/bin/{examples,test} + rm -rf $out/bin/{examples,tests} + # we don't care about gtest related libs + rm -rf $lib/lib/libg* cd ../src find . -iname '*.h' -exec cp --parents '{}' $dev/include \; rm -rf $dev/include/tests ''; + checkInputs = [ python3 ]; + doCheck = true; + preCheck = '' + export LD_LIBRARY_PATH=$(readlink -f lib) + patchShebangs .. + ''; + outputs = [ "out" "dev" "lib" ]; meta = with stdenv.lib; { diff --git a/pkgs/applications/science/logic/btor2tools/default.nix b/pkgs/applications/science/logic/btor2tools/default.nix index 2aedfb1d07e..714ab49524b 100644 --- a/pkgs/applications/science/logic/btor2tools/default.nix +++ b/pkgs/applications/science/logic/btor2tools/default.nix @@ -1,24 +1,24 @@ -{ stdenv, fetchFromGitHub }: +{ stdenv, cmake, fetchFromGitHub }: -stdenv.mkDerivation { +stdenv.mkDerivation rec { pname = "btor2tools"; - version = "pre55_8c150b39"; + version = "1.0.0-pre_${src.rev}"; src = fetchFromGitHub { owner = "boolector"; repo = "btor2tools"; - rev = "8c150b39cdbcdef4247344acf465d75ef642365d"; - sha256 = "1r5pid4x567nms02ajjrz3v0zj18k0fi5pansrmc2907rnx2acxx"; + rev = "9831f9909fb283752a3d6d60d43613173bd8af42"; + sha256 = "0mfqmkgvyw8fa2c09kww107dmk180ch1hp98r5kv41vnc04iqb0s"; }; - configurePhase = "./configure.sh -shared"; + nativeBuildInputs = [ cmake ]; installPhase = '' mkdir -p $out $dev/include/btor2parser/ $lib/lib cp -vr bin $out - cp -v src/btor2parser/btor2parser.h $dev/include/btor2parser - cp -v build/libbtor2parser.* $lib/lib + cp -v ../src/btor2parser/btor2parser.h $dev/include/btor2parser + cp -v lib/libbtor2parser.* $lib/lib ''; outputs = [ "out" "dev" "lib" ]; diff --git a/pkgs/applications/science/logic/cadical/default.nix b/pkgs/applications/science/logic/cadical/default.nix index 5e6c0d55b7d..e3707ff7dab 100644 --- a/pkgs/applications/science/logic/cadical/default.nix +++ b/pkgs/applications/science/logic/cadical/default.nix @@ -2,16 +2,18 @@ stdenv.mkDerivation rec { pname = "cadical"; - version = "1.2.1"; + version = "1.3.0"; src = fetchFromGitHub { owner = "arminbiere"; repo = "cadical"; rev = "rel-${version}"; - hash = "sha256:1a66xkw42ad330fvw8i0sawrmg913m8wrq5c85lw5qandkwvxdi6"; + sha256 = "05lvnvapjawgkky38xknb9lgaliiwan4kggmb9yggl4ifpjrh8qf"; }; + doCheck = true; dontAddPrefix = true; + installPhase = '' install -Dm0755 build/cadical "$out/bin/cadical" install -Dm0755 build/mobical "$out/bin/mobical" diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index 315900d42b9..946cba41b14 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -5,11 +5,10 @@ # - The exact version can be specified through the `version` argument to # the derivation; it defaults to the latest stable version. -{ stdenv, fetchFromGitHub, writeText, pkgconfig +{ stdenv, fetchFromGitHub, writeText, pkgconfig, gnumake42 , ocamlPackages, ncurses , buildIde ? !(stdenv.isDarwin && stdenv.lib.versionAtLeast version "8.10") , glib, gnome3, wrapGAppsHook -, darwin , csdp ? null , version }: @@ -34,6 +33,8 @@ let "8.10.2" = "0znxmpy71bfw0p6x47i82jf5k7v41zbz9bdpn901ysn3ir8l3wrz"; "8.11.0" = "1rfdic6mp7acx2zfwz7ziqk12g95bl9nyj68z4n20a5bcjv2pxpn"; "8.11.1" = "0qriy9dy36dajsv5qmli8gd6v55mah02ya334nw49ky19v7518m0"; + "8.11.2" = "0f77ccyxdgbf1nrj5fa8qvrk1cyfy06fv8gj9kzfvlcgn0cf48sa"; + "8.12.0" = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz"; }.${version}; coq-version = stdenv.lib.versions.majorMinor version; versionAtLeast = stdenv.lib.versionAtLeast coq-version; @@ -105,16 +106,19 @@ self = stdenv.mkDerivation { inherit sha256; }; - nativeBuildInputs = [ pkgconfig ]; + nativeBuildInputs = [ pkgconfig ] + ++ stdenv.lib.optional (!versionAtLeast "8.6") gnumake42 + ; buildInputs = [ ncurses ocamlPackages.ocaml ocamlPackages.findlib ] ++ stdenv.lib.optional (!versionAtLeast "8.10") ocamlPackages.camlp5 - ++ [ ocamlPackages.num ] + ++ stdenv.lib.optional (!versionAtLeast "8.12") ocamlPackages.num ++ stdenv.lib.optionals buildIde (if versionAtLeast "8.10" then [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook ] - ++ stdenv.lib.optional stdenv.isDarwin darwin.apple_sdk.frameworks.Cocoa else [ ocamlPackages.lablgtk ]); + propagatedBuildInputs = stdenv.lib.optional (versionAtLeast "8.12") ocamlPackages.num; + postPatch = '' UNAME=$(type -tp uname) RM=$(type -tp rm) diff --git a/pkgs/applications/science/logic/cryptominisat/default.nix b/pkgs/applications/science/logic/cryptominisat/default.nix index 8c1b3bd0369..ddbb140c9ba 100644 --- a/pkgs/applications/science/logic/cryptominisat/default.nix +++ b/pkgs/applications/science/logic/cryptominisat/default.nix @@ -1,16 +1,24 @@ -{ stdenv, fetchFromGitHub, cmake, python3, xxd, boost }: +{ stdenv, fetchFromGitHub, cmake, python3, xxd, boost, fetchpatch }: stdenv.mkDerivation rec { pname = "cryptominisat"; - version = "5.7.0"; + version = "5.8.0"; src = fetchFromGitHub { owner = "msoos"; repo = "cryptominisat"; rev = version; - sha256 = "0ny5ln8fc0irprs04qw01c9mppps8q27lkx01a549zazwhj4b5rm"; + sha256 = "00hmxdlyhn7pwk9jlvc5g0l5z5xqfchjzf5jgn3pkj9xhl8yqq50"; }; + 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 ]; diff --git a/pkgs/applications/science/logic/cvc4/default.nix b/pkgs/applications/science/logic/cvc4/default.nix index a6e9bc69a12..54a2f022551 100644 --- a/pkgs/applications/science/logic/cvc4/default.nix +++ b/pkgs/applications/science/logic/cvc4/default.nix @@ -1,19 +1,20 @@ -{ stdenv, fetchurl, cln, gmp, swig, pkgconfig -, readline, libantlr3c, boost, jdk, autoreconfHook -, python3, antlr3_4 +{ stdenv, fetchFromGitHub, cmake, cln, gmp, git, swig, pkgconfig +, readline, libantlr3c, boost, jdk, python3, antlr3_4 }: stdenv.mkDerivation rec { pname = "cvc4"; - version = "1.6"; + version = "1.8"; - src = fetchurl { - url = "https://cvc4.cs.stanford.edu/downloads/builds/src/cvc4-${version}.tar.gz"; - sha256 = "1iw793zsi48q91lxpf8xl8lnvv0jsj4whdad79rakywkm1gbs62w"; + src = fetchFromGitHub { + owner = "cvc4"; + repo = "cvc4"; + rev = version; + sha256 = "1rhs4pvzaa1wk00czrczp58b2cxfghpsnq534m0l3snnya2958jp"; }; - nativeBuildInputs = [ autoreconfHook pkgconfig ]; - buildInputs = [ gmp cln readline swig libantlr3c antlr3_4 boost jdk python3 ]; + nativeBuildInputs = [ pkgconfig cmake ]; + buildInputs = [ gmp git python3.pkgs.toml cln readline swig libantlr3c antlr3_4 boost jdk python3 ]; configureFlags = [ "--enable-language-bindings=c,c++,java" "--enable-gpl" @@ -30,6 +31,10 @@ stdenv.mkDerivation rec { preConfigure = '' patchShebangs ./src/ ''; + cmakeFlags = [ + "-DCMAKE_BUILD_TYPE=Production" + ]; + enableParallelBuilding = true; diff --git a/pkgs/applications/science/logic/drat-trim/default.nix b/pkgs/applications/science/logic/drat-trim/default.nix index 4099236e628..81e20df3342 100644 --- a/pkgs/applications/science/logic/drat-trim/default.nix +++ b/pkgs/applications/science/logic/drat-trim/default.nix @@ -1,13 +1,14 @@ { stdenv, fetchFromGitHub }: stdenv.mkDerivation { - name = "drat-trim-2017-08-31"; + pname = "drat-trim-unstable"; + version = "2020-06-05"; src = fetchFromGitHub { owner = "marijnheule"; repo = "drat-trim"; - rev = "37ac8f874826ffa3500a00698910e137498defac"; - sha256 = "1m9q47dfnvdli1z3kb1jvvbm0dgaw725k1aw6h9w00bggqb91bqh"; + rev = "9afad0f7156a1e9c6ce19dce5d72cf1cb9a3ef27"; + sha256 = "1zq585igfaknwqbvv2cji744016zxadbvr0ifr5l6yq13m0vvn3b"; }; postPatch = '' @@ -15,7 +16,7 @@ stdenv.mkDerivation { ''; installPhase = '' - install -Dt $out/bin drat-trim + install -Dt $out/bin drat-trim lrat-check ''; meta = with stdenv.lib; { @@ -31,6 +32,10 @@ stdenv.mkDerivation { annual SAT Competition in recent years, in order to check competing SAT solvers' work when they claim that a SAT instance is unsatisfiable. + + This package also contains the related tool LRAT-check, which checks a + proof format called LRAT which extends DRAT with hint statements to speed + up the checking process. ''; homepage = "https://www.cs.utexas.edu/~marijn/drat-trim/"; license = licenses.mit; diff --git a/pkgs/applications/science/logic/elan/default.nix b/pkgs/applications/science/logic/elan/default.nix index 743bbf163c2..7a7da2c5f5d 100644 --- a/pkgs/applications/science/logic/elan/default.nix +++ b/pkgs/applications/science/logic/elan/default.nix @@ -2,16 +2,16 @@ rustPlatform.buildRustPackage rec { pname = "elan"; - version = "0.10.0"; + version = "0.10.2"; src = fetchFromGitHub { owner = "kha"; repo = "elan"; rev = "v${version}"; - sha256 = "0aw538shvpfbk481y0gw3z97nsazdnk8qh8fwsb6ji62p2r51v6f"; + sha256 = "0ycw1r364g5gwh8796dpv1israpg7zqwx8mcvnacv2lqj5iijmby"; }; - cargoSha256 = "0zg3q31z516049v9fhli4yxldx9fg31k2qfx4ag8rmyvpgy9xh6c"; + cargoSha256 = "0hcaiy046d2gnkp6sfpnkkprb3nd94i9q8dgqxxpwrc1j157x6z9"; nativeBuildInputs = [ pkgconfig ]; diff --git a/pkgs/applications/science/logic/eprover/default.nix b/pkgs/applications/science/logic/eprover/default.nix index f19d7e35c3e..a3844dc3700 100644 --- a/pkgs/applications/science/logic/eprover/default.nix +++ b/pkgs/applications/science/logic/eprover/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "eprover"; - version = "2.4"; + version = "2.5"; src = fetchurl { url = "https://wwwlehre.dhbw-stuttgart.de/~sschulz/WORK/E_DOWNLOAD/V_${version}/E.tgz"; - sha256 = "1xn5yypy6w36amsb3kvj1srlbv6v5dl51k64cd264asz2n469dxw"; + sha256 = "0jj0zkiqpcx9xp16spkskrv3jycprz7jg1g97i67j43c4yvxylwa"; }; buildInputs = [ which ]; diff --git a/pkgs/applications/science/logic/fast-downward/default.nix b/pkgs/applications/science/logic/fast-downward/default.nix index ed757e444b7..a4654209537 100644 --- a/pkgs/applications/science/logic/fast-downward/default.nix +++ b/pkgs/applications/science/logic/fast-downward/default.nix @@ -1,12 +1,13 @@ { stdenv, lib, fetchhg, cmake, which, python3, osi, cplex }: stdenv.mkDerivation { - name = "fast-downward-2019-05-13"; + version = "19.12"; + pname = "fast-downward"; src = fetchhg { url = "http://hg.fast-downward.org/"; - rev = "090f5df5d84a"; - sha256 = "14pcjz0jfzx5269axg66iq8js7lm2w3cnqrrhhwmz833prjp945g"; + rev = "41688a4f16b3"; + sha256 = "08m4k1mkx4sz7c2ab7xh7ip6b67zxv7kl68xrvwa83xw1yigqkna"; }; nativeBuildInputs = [ cmake which ]; @@ -17,19 +18,22 @@ stdenv.mkDerivation { enableParallelBuilding = true; + configurePhase = '' + python build.py release + ''; + postPatch = '' - cd src # Needed because the package tries to be too smart. export CC="$(which $CC)" export CXX="$(which $CXX)" ''; installPhase = '' - install -Dm755 bin/downward $out/libexec/fast-downward/downward - cp -r ../translate $out/libexec/fast-downward/ - install -Dm755 ../../fast-downward.py $out/bin/fast-downward + install -Dm755 builds/release/bin/downward $out/libexec/fast-downward/downward + cp -r builds/release/bin/translate $out/libexec/fast-downward/ + install -Dm755 fast-downward.py $out/bin/fast-downward mkdir -p $out/${python3.sitePackages} - cp -r ../../driver $out/${python3.sitePackages} + cp -r driver $out/${python3.sitePackages} wrapPythonProgramsIn $out/bin "$out $pythonPath" wrapPythonProgramsIn $out/libexec/fast-downward/translate "$out $pythonPath" @@ -43,13 +47,16 @@ stdenv.mkDerivation { echo "Moving $i to $dest" mv "$i" "$dest" done + + substituteInPlace $out/${python3.sitePackages}/driver/arguments.py \ + --replace 'args.build = "release"' "args.build = \"$out/libexec/fast-downward\"" ''; meta = with stdenv.lib; { description = "A domain-independent planning system"; homepage = "http://www.fast-downward.org/"; license = licenses.gpl3Plus; - platforms = platforms.linux; + platforms = with platforms; (linux ++ darwin); maintainers = with maintainers; [ abbradar ]; }; } diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index d2e49d81783..a12d75eabbe 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -3,18 +3,18 @@ stdenv.mkDerivation rec { pname = "isabelle"; - version = "2018"; + version = "2020"; dirname = "Isabelle${version}"; src = if stdenv.isDarwin then fetchurl { - url = "http://isabelle.in.tum.de/website-${dirname}/dist/${dirname}.dmg"; - sha256 = "0jwnvsf5whklq14ihaxs7b9nbic94mm56nvxljrdbvl6y628j9r5"; + url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz"; + sha256 = "1sfr5filsaqj93g5y4p9n8g5652dhr4whj25x4lifdxr2pp560xx"; } else fetchurl { url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz"; - sha256 = "1928lwrw1v1p9s23kix30ncpqm8djmrnjixj82f3ni2a8sc3hrsp"; + sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3"; }; buildInputs = [ perl polyml z3 ] @@ -42,14 +42,14 @@ stdenv.mkDerivation rec { ML_SOURCES="\$POLYML_HOME/src" EOF - cat >contrib/jdk/etc/settings <<EOF + cat >contrib/jdk*/etc/settings <<EOF ISABELLE_JAVA_PLATFORM=${stdenv.system} ISABELLE_JDK_HOME=${java} EOF echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings - for comp in contrib/jdk contrib/polyml-* contrib/z3-*; do + for comp in contrib/jdk* contrib/polyml-* contrib/z3-*; do rm -rf $comp/x86* done '' + (if ! stdenv.isLinux then "" else '' @@ -66,7 +66,7 @@ stdenv.mkDerivation rec { bin/isabelle install $out/bin ''; - meta = { + meta = with stdenv.lib; { description = "A generic proof assistant"; longDescription = '' @@ -74,9 +74,9 @@ stdenv.mkDerivation rec { to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. ''; - homepage = "http://isabelle.in.tum.de/"; - license = "LGPL"; - maintainers = [ stdenv.lib.maintainers.jwiegley ]; - platforms = stdenv.lib.platforms.linux; + homepage = "https://isabelle.in.tum.de/"; + license = licenses.bsd3; + maintainers = [ maintainers.jwiegley ]; + platforms = platforms.linux; }; } diff --git a/pkgs/applications/science/logic/lean/default.nix b/pkgs/applications/science/logic/lean/default.nix index c80c163562b..224795f2a66 100644 --- a/pkgs/applications/science/logic/lean/default.nix +++ b/pkgs/applications/science/logic/lean/default.nix @@ -1,14 +1,14 @@ -{ stdenv, fetchFromGitHub, cmake, gmp }: +{ stdenv, fetchFromGitHub, cmake, gmp, coreutils }: stdenv.mkDerivation rec { pname = "lean"; - version = "3.10.0"; + version = "3.18.4"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "lean"; rev = "v${version}"; - sha256 = "0nmh09x3scfqg0bg1qf8b7z67s11hbfd7kr1h6k1zw94fyn2mg8q"; + sha256 = "1pmc2wi1pa346w89ayrrjv9xk6v6myg2zmx1wj4pd9qxv7ivrbsn"; }; nativeBuildInputs = [ cmake ]; @@ -19,6 +19,11 @@ stdenv.mkDerivation rec { cd src ''; + postInstall = stdenv.lib.optionalString stdenv.isDarwin '' + substituteInPlace $out/bin/leanpkg \ + --replace "greadlink" "${coreutils}/bin/readlink" + ''; + meta = with stdenv.lib; { description = "Automatic and interactive theorem prover"; homepage = "https://leanprover.github.io/"; diff --git a/pkgs/applications/science/logic/ltl2ba/default.nix b/pkgs/applications/science/logic/ltl2ba/default.nix index 02e9844115e..b5d13db3b9a 100644 --- a/pkgs/applications/science/logic/ltl2ba/default.nix +++ b/pkgs/applications/science/logic/ltl2ba/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "ltl2ba"; - version = "1.2"; + version = "1.3"; src = fetchurl { url = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/${pname}-${version}.tar.gz"; - sha256 = "0vzv5g7v87r41cvdafxi6yqnk7glzxrzgavy8213k59f6v11dzlx"; + sha256 = "1bz9gjpvby4mnvny0nmxgd81rim26mqlcnjlznnxxk99575pfa4i"; }; hardeningDisable = [ "format" ]; diff --git a/pkgs/applications/science/logic/mcy/default.nix b/pkgs/applications/science/logic/mcy/default.nix index a9366d56058..eba910e07eb 100644 --- a/pkgs/applications/science/logic/mcy/default.nix +++ b/pkgs/applications/science/logic/mcy/default.nix @@ -7,31 +7,38 @@ let in stdenv.mkDerivation { pname = "mcy"; - version = "2020.03.21"; + version = "2020.08.03"; src = fetchFromGitHub { owner = "YosysHQ"; repo = "mcy"; - rev = "bac92b8aad9bf24714fda70d3750bb50d6d96177"; - sha256 = "0mmg6zd5cbn8g0am9c3naamg0lq67yyy117fzn2ydigcyia7vmnp"; + rev = "62048e69df13f8e03670424626755ae8ef4c36ff"; + sha256 = "15xxgzx1zxzx5kshqyrxnfx33cz6cjzxcdcn6z98jhs9bwyvf96f"; }; buildInputs = [ python ]; patchPhase = '' + chmod +x scripts/create_mutated.sh + patchShebangs . + substituteInPlace mcy.py \ --replace yosys '${yosys}/bin/yosys' \ --replace 'os.execvp("mcy-dash"' "os.execvp(\"$out/bin/mcy-dash\"" substituteInPlace mcy-dash.py \ - --replace 'app.run(debug=True)' 'app.run(host="0.0.0.0",debug=True)' + --replace 'app.run(debug=True)' 'app.run(host="0.0.0.0",debug=True)' \ + --replace 'subprocess.Popen(["mcy"' "subprocess.Popen([\"$out/bin/mcy\"" + substituteInPlace scripts/create_mutated.sh \ + --replace yosys '${yosys}/bin/yosys' ''; # the build needs a bit of work... buildPhase = "true"; installPhase = '' - mkdir -p $out/bin $out/share/mcy/dash + mkdir -p $out/bin $out/share/mcy/{dash,scripts} install mcy.py $out/bin/mcy && chmod +x $out/bin/mcy install mcy-dash.py $out/bin/mcy-dash && chmod +x $out/bin/mcy-dash - cp -r dash/. $out/share/mcy/dash/. + cp -r dash/. $out/share/mcy/dash/. + cp -r scripts/. $out/share/mcy/scripts/. ''; meta = { diff --git a/pkgs/applications/science/logic/proverif/default.nix b/pkgs/applications/science/logic/proverif/default.nix index 931ad2fc4f3..6a9367b30aa 100644 --- a/pkgs/applications/science/logic/proverif/default.nix +++ b/pkgs/applications/science/logic/proverif/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "proverif"; - version = "2.00"; + version = "2.01"; src = fetchurl { url = "http://prosecco.gforge.inria.fr/personal/bblanche/proverif/proverif${version}.tar.gz"; - sha256 = "0vjphj85ch9q39vc7sd6n4vxy5bplp017vlshk989yhfwb00r37y"; + sha256 = "01wp5431c77z0aaa99h8bnm5yhr6jslpqc8iyg0a7gxfqnb19gxi"; }; buildInputs = with ocamlPackages; [ ocaml findlib lablgtk ]; diff --git a/pkgs/applications/science/logic/sad/default.nix b/pkgs/applications/science/logic/sad/default.nix index f9b82b5d733..77613a13571 100644 --- a/pkgs/applications/science/logic/sad/default.nix +++ b/pkgs/applications/science/logic/sad/default.nix @@ -8,7 +8,7 @@ stdenv.mkDerivation { }; buildInputs = [ haskell.compiler.ghc844 spass ]; patches = [ - ./patch + ./patch.patch # Since the LTS 12.0 update, <> is an operator in Prelude, colliding with # the <> operator with a different meaning defined by this package ./monoid.patch @@ -35,5 +35,6 @@ stdenv.mkDerivation { maintainers = [ stdenv.lib.maintainers.schmitthenner ]; homepage = "http://nevidal.org/sad.en.html"; platforms = stdenv.lib.platforms.linux; + broken = true; # ghc-8.4.4 is gone from Nixpkgs }; } diff --git a/pkgs/applications/science/logic/sad/patch b/pkgs/applications/science/logic/sad/patch.patch index a5b1d617708..a5b1d617708 100644 --- a/pkgs/applications/science/logic/sad/patch +++ b/pkgs/applications/science/logic/sad/patch.patch diff --git a/pkgs/applications/science/logic/symbiyosys/default.nix b/pkgs/applications/science/logic/symbiyosys/default.nix index b180cf307f0..9cf8b0845d4 100644 --- a/pkgs/applications/science/logic/symbiyosys/default.nix +++ b/pkgs/applications/science/logic/symbiyosys/default.nix @@ -1,20 +1,20 @@ { stdenv, fetchFromGitHub , bash, python3, yosys -, yices, boolector, aiger +, yices, boolector, z3, aiger }: stdenv.mkDerivation { pname = "symbiyosys"; - version = "2020.03.24"; + version = "2020.08.22"; src = fetchFromGitHub { owner = "YosysHQ"; repo = "SymbiYosys"; - rev = "8a62780b9df4d2584e41cdd42cab92fddcd75b31"; - sha256 = "0ss5mrzwff2dny8kfciqbrz67m6k52yvc1shd7gk3qb99x7g7fp8"; + rev = "33b0bb7d836fe2a73dc7b10587222f2a718beef4"; + sha256 = "03rbrbwsji1sqcp2yhgbc0fca04zsryv2g4izjhdzv64nqjzjyhn"; }; - buildInputs = [ python3 ]; + buildInputs = [ ]; patchPhase = '' patchShebangs . @@ -26,14 +26,15 @@ stdenv.mkDerivation { # Fix various executable references substituteInPlace sbysrc/sby_core.py \ --replace '"/usr/bin/env", "bash"' '"${bash}/bin/bash"' \ - --replace ': "btormc"' ': "${boolector}/bin/btormc"' \ - --replace ': "yosys"' ': "${yosys}/bin/yosys"' \ - --replace ': "yosys-smtbmc"' ': "${yosys}/bin/yosys-smtbmc"' \ - --replace ': "yosys-abc"' ': "${yosys}/bin/yosys-abc"' \ - --replace ': "aigbmc"' ': "${aiger}/bin/aigbmc"' \ + --replace ', "btormc"' ', "${boolector}/bin/btormc"' \ + --replace ', "aigbmc"' ', "${aiger}/bin/aigbmc"' + + substituteInPlace sbysrc/sby_core.py \ + --replace '##yosys-program-prefix##' '"${yosys}/bin/"' ''; buildPhase = "true"; + installPhase = '' mkdir -p $out/bin $out/share/yosys/python3 @@ -43,6 +44,10 @@ stdenv.mkDerivation { chmod +x $out/bin/sby ''; + doCheck = false; # not all provers are yet packaged... + checkInputs = [ python3 yosys boolector yices z3 aiger ]; + checkPhase = "make test"; + meta = { description = "Tooling for Yosys-based verification flows"; homepage = "https://symbiyosys.readthedocs.io/"; diff --git a/pkgs/applications/science/logic/tlaplus/toolbox.nix b/pkgs/applications/science/logic/tlaplus/toolbox.nix index f326d62f8f0..5edc3e4129d 100644 --- a/pkgs/applications/science/logic/tlaplus/toolbox.nix +++ b/pkgs/applications/science/logic/tlaplus/toolbox.nix @@ -13,7 +13,7 @@ let comment = "IDE for TLA+"; desktopName = name; genericName = comment; - categories = "Application;Development"; + categories = "Development"; extraEntries = '' StartupWMClass=TLA+ Toolbox ''; diff --git a/pkgs/applications/science/logic/vampire/default.nix b/pkgs/applications/science/logic/vampire/default.nix index e5941a35fd5..dca03823e9e 100644 --- a/pkgs/applications/science/logic/vampire/default.nix +++ b/pkgs/applications/science/logic/vampire/default.nix @@ -2,13 +2,13 @@ stdenv.mkDerivation rec { pname = "vampire"; - version = "4.4"; + version = "4.5.1"; src = fetchFromGitHub { owner = "vprover"; repo = "vampire"; rev = version; - sha256 = "0v2fdfnk7l5xr5c4y54r25g1nbp4vi85zv29nbklh3r7aws3w9q1"; + sha256 = "0q9gqyq96amdnhxgwjyv0r2sxakikp3jvmizgj2h0spfz643p8db"; }; buildInputs = [ z3 zlib ]; diff --git a/pkgs/applications/science/logic/why3/configure.patch b/pkgs/applications/science/logic/why3/configure.patch deleted file mode 100644 index 3eebf3cf165..00000000000 --- a/pkgs/applications/science/logic/why3/configure.patch +++ /dev/null @@ -1,11 +0,0 @@ -diff --git a/configure b/configure ---- a/configure -+++ b/configure -@@ -4029,7 +4029,6 @@ fi - - if test "$USEOCAMLFIND" = yes; then - OCAMLFINDLIB=$(ocamlfind printconf stdlib) -- OCAMLFIND=$(which ocamlfind) - if test "$OCAMLFINDLIB" != "$OCAMLLIB"; then - USEOCAMLFIND=no; - echo "but your ocamlfind is not compatible with your ocamlc:" diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix index 51cb2a456c1..b9bd2172bb1 100644 --- a/pkgs/applications/science/logic/why3/default.nix +++ b/pkgs/applications/science/logic/why3/default.nix @@ -3,11 +3,11 @@ stdenv.mkDerivation { pname = "why3"; - version = "1.2.1"; + version = "1.3.1"; src = fetchurl { - url = "https://gforge.inria.fr/frs/download.php/file/38185/why3-1.2.1.tar.gz"; - sha256 = "014gkwisjp05x3342zxkryb729p02ngx1hcjjsrplpa53jzgz647"; + url = "https://gforge.inria.fr/frs/download.php/file/38291/why3-1.3.1.tar.gz"; + sha256 = "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv"; }; buildInputs = with ocamlPackages; [ @@ -29,14 +29,9 @@ stdenv.mkDerivation { enableParallelBuilding = true; - # Remove unnecessary call to which - patches = [ ./configure.patch - # Compatibility with js_of_ocaml 3.5 - (fetchpatch { - url = "https://gitlab.inria.fr/why3/why3/commit/269ab313382fe3e64ef224813937314748bf7cf0.diff"; - sha256 = "0i92wdnbh8pihvl93ac0ma1m5g95jgqqqj4kw6qqvbbjjqdgvzwa"; - }) - ]; + postPatch = '' + substituteInPlace Makefile.in --replace js_of_ocaml.ppx js_of_ocaml-ppx + ''; configureFlags = [ "--enable-verbose-make" ]; diff --git a/pkgs/applications/science/logic/workcraft/default.nix b/pkgs/applications/science/logic/workcraft/default.nix index 685d6ee4861..4038db17f93 100644 --- a/pkgs/applications/science/logic/workcraft/default.nix +++ b/pkgs/applications/science/logic/workcraft/default.nix @@ -2,11 +2,11 @@ stdenv.mkDerivation rec { pname = "workcraft"; - version = "3.2.6"; + version = "3.3.0"; src = fetchurl { url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz"; - sha256 = "1sfbxmk71gp7paw4l5azqr0lsgsyp4308gx2jz8w4k3nasfshz25"; + sha256 = "072i7kan2c9f4s9jxwqr4ccsi9979c12xhwr385sbq06rwyrna85"; }; buildInputs = [ makeWrapper ]; diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix index 170a56b95b9..350a4f99af8 100644 --- a/pkgs/applications/science/logic/z3/default.nix +++ b/pkgs/applications/science/logic/z3/default.nix @@ -1,32 +1,41 @@ -{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames }: +{ stdenv, fetchFromGitHub, python, fixDarwinDylibNames +, javaBindings ? false +, pythonBindings ? true +, jdk ? null +}: + +assert javaBindings -> jdk != null; + +with stdenv.lib; stdenv.mkDerivation rec { pname = "z3"; - version = "4.8.7"; + version = "4.8.8"; src = fetchFromGitHub { owner = "Z3Prover"; repo = pname; rev = "z3-${version}"; - sha256 = "0hprcdwhhyjigmhhk6514m71bnmvqci9r8gglrqilgx424r6ff7q"; + sha256 = "1rn538ghqwxq0v8i6578j8mflk6fyv0cp4hjfqynzvinjbps56da"; }; - buildInputs = [ python fixDarwinDylibNames ]; + buildInputs = [ python fixDarwinDylibNames ] ++ optional javaBindings jdk; propagatedBuildInputs = [ python.pkgs.setuptools ]; enableParallelBuilding = true; - configurePhase = '' - ${python.interpreter} scripts/mk_make.py --prefix=$out --python --pypkgdir=$out/${python.sitePackages} - cd build - ''; + configurePhase = concatStringsSep " " ( + [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ] + ++ optional javaBindings "--java" + ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}" + ) + "\n" + "cd build"; postInstall = '' - mkdir -p $dev $lib $python/lib - - mv $out/lib/python* $python/lib/ - mv $out/lib $lib/lib - mv $out/include $dev/include - + 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} ''; @@ -37,6 +46,6 @@ stdenv.mkDerivation rec { homepage = "https://github.com/Z3Prover/z3"; license = stdenv.lib.licenses.mit; platforms = stdenv.lib.platforms.x86_64; - maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ]; }; } |