diff options
Diffstat (limited to 'pkgs/applications/science/logic')
10 files changed, 148 insertions, 36 deletions
diff --git a/pkgs/applications/science/logic/bitwuzla/default.nix b/pkgs/applications/science/logic/bitwuzla/default.nix new file mode 100644 index 00000000000..a8820b55b74 --- /dev/null +++ b/pkgs/applications/science/logic/bitwuzla/default.nix @@ -0,0 +1,67 @@ +{ stdenv +, fetchFromGitHub +, lib +, python3 +, cmake +, lingeling +, btor2tools +, gtest +, gmp +, cadical +, minisat +, picosat +, cryptominisat +, zlib +, pkg-config + # "*** internal error in 'lglib.c': watcher stack overflow" on aarch64-linux +, withLingeling ? !stdenv.hostPlatform.isAarch64 +}: + +stdenv.mkDerivation rec { + pname = "bitwuzla"; + version = "unstable-2021-07-01"; + + src = fetchFromGitHub { + owner = "bitwuzla"; + repo = "bitwuzla"; + rev = "58d720598e359b1fdfec4a469c76f1d1f24db51a"; + sha256 = "06ymqsdppyixb918161rmbgqvbnarj4nm4az88lkn3ri4gyimw04"; + }; + + nativeBuildInputs = [ cmake pkg-config ]; + buildInputs = [ + cadical + cryptominisat + picosat + minisat + btor2tools + gmp + zlib + ] ++ lib.optional withLingeling lingeling; + + cmakeFlags = [ + "-DBUILD_SHARED_LIBS=ON" + "-DPicoSAT_INCLUDE_DIR=${lib.getDev picosat}/include/picosat" + "-DBtor2Tools_INCLUDE_DIR=${lib.getDev btor2tools}/include/btor2parser" + "-DBtor2Tools_LIBRARIES=${lib.getLib btor2tools}/lib/libbtor2parser${stdenv.hostPlatform.extensions.sharedLibrary}" + ] ++ lib.optional doCheck "-DTESTING=YES"; + + checkInputs = [ python3 gtest ]; + # two tests fail on darwin and 3 on aarch64-linux + doCheck = stdenv.hostPlatform.isLinux && (!stdenv.hostPlatform.isAarch64); + preCheck = let + var = if stdenv.isDarwin then "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"; + in + '' + export ${var}=$(readlink -f lib) + patchShebangs .. + ''; + + meta = with lib; { + description = "A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions"; + homepage = "https://bitwuzla.github.io"; + license = licenses.mit; + platforms = platforms.unix; + maintainers = with maintainers; [ symphorien ]; + }; +} diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix index 6916379bdea..7d90dca46f5 100644 --- a/pkgs/applications/science/logic/boolector/default.nix +++ b/pkgs/applications/science/logic/boolector/default.nix @@ -1,26 +1,18 @@ -{ stdenv, fetchFromGitHub, fetchpatch, lib, python3 +{ stdenv, fetchFromGitHub, lib, python3 , cmake, lingeling, btor2tools, gtest, gmp }: stdenv.mkDerivation rec { pname = "boolector"; - version = "3.2.1"; + version = "3.2.2"; src = fetchFromGitHub { owner = "boolector"; repo = "boolector"; - rev = "refs/tags/${version}"; - sha256 = "0jkmaw678njqgkflzj9g374yk1mci8yqvsxkrqzlifn6bwhwb7ci"; + rev = version; + sha256 = "1smcy6yp8wvnw2brgnv5bf40v87k4v4fbdbrhi7987vja632k50z"; }; - # excludes development artifacts from install, will be included in next release - patches = [ - (fetchpatch { - url = "https://github.com/Boolector/boolector/commit/4d240436e34e65096671099766344dd9126145b1.patch"; - sha256 = "1girsbvlhkkl1hldl2gsjynwc3m92jskn798qhx0ydg6whrfgcgw"; - }) - ]; - postPatch = '' sed s@REPLACEME@file://${gtest.src}@ ${./cmake-gtest.patch} | patch -p1 ''; diff --git a/pkgs/applications/science/logic/cadical/default.nix b/pkgs/applications/science/logic/cadical/default.nix index ca5e6b5c419..6758eeb6605 100644 --- a/pkgs/applications/science/logic/cadical/default.nix +++ b/pkgs/applications/science/logic/cadical/default.nix @@ -11,14 +11,30 @@ stdenv.mkDerivation rec { sha256 = "05lvnvapjawgkky38xknb9lgaliiwan4kggmb9yggl4ifpjrh8qf"; }; + outputs = [ "out" "dev" "lib" ]; doCheck = true; - dontAddPrefix = true; + + # the configure script is not generated by autotools and does not accept the + # arguments that the default configurePhase passes like --prefix and --libdir + configurePhase = '' + runHook preConfigure + + ./configure + + runHook postConfigure + ''; installPhase = '' + runHook preInstall + install -Dm0755 build/cadical "$out/bin/cadical" install -Dm0755 build/mobical "$out/bin/mobical" - mkdir -p "$out/share/doc/${pname}-${version}/" - install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}-${version}/" + install -Dm0644 src/ccadical.h "$dev/include/ccadical.h" + install -Dm0644 build/libcadical.a "$lib/lib/libcadical.a" + mkdir -p "$out/share/doc/${pname}/" + install -Dm0755 {LICEN?E,README*,VERSION} "$out/share/doc/${pname}/" + + runHook postInstall ''; meta = with lib; { diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index b5c66289c9d..cd19b9a9442 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/pkgs/applications/science/logic/coq/default.nix @@ -162,6 +162,7 @@ self = stdenv.mkDerivation { prefixKey = "-prefix "; buildFlags = [ "revision" "coq" "coqide" "bin/votour" ]; + enableParallelBuilding = true; createFindlibDestdir = true; diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 600ae83ff91..f9337f69025 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -1,20 +1,20 @@ -{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, rlwrap }: +{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, rlwrap, makeDesktopItem }: # nettools needed for hostname stdenv.mkDerivation rec { pname = "isabelle"; - version = "2020"; + version = "2021"; dirname = "Isabelle${version}"; src = if stdenv.isDarwin then fetchurl { url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_macos.tar.gz"; - sha256 = "1sfr5filsaqj93g5y4p9n8g5652dhr4whj25x4lifdxr2pp560xx"; + sha256 = "1c2qm2ksmpyxyccyyn4lyj2wqj5m74nz2i0c5abrd1hj45zcnh1m"; } else fetchurl { url = "https://isabelle.in.tum.de/website-${dirname}/dist/${dirname}_linux.tar.gz"; - sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3"; + sha256 = "1isgc9w4q95638dcag9gxz1kmf97pkin3jz1dm2lhd64b2k12y2x"; }; nativeBuildInputs = [ makeWrapper ]; @@ -48,6 +48,8 @@ stdenv.mkDerivation rec { ISABELLE_JDK_HOME=${java} EOF + sed -i -e 's/naproche_server : bool = true/naproche_server : bool = false/' contrib/naproche-*/etc/options + echo ISABELLE_LINE_EDITOR=${rlwrap}/bin/rlwrap >>etc/settings for comp in contrib/jdk* contrib/polyml-* contrib/z3-*; do @@ -66,9 +68,26 @@ stdenv.mkDerivation rec { cd $out/$dirname bin/isabelle install $out/bin + # icon + mkdir -p "$out/share/icons/hicolor/isabelle/apps" + cp "$out/Isabelle${version}/lib/icons/isabelle.xpm" "$out/share/icons/hicolor/isabelle/apps/" + + # desktop item + mkdir -p "$out/share" + cp -r "${desktopItem}/share/applications" "$out/share/applications" + wrapProgram $out/$dirname/src/HOL/Tools/ATP/scripts/remote_atp --set PERL5LIB ${perlPackages.makeFullPerlPath [ perlPackages.LWP ]} ''; + desktopItem = makeDesktopItem { + name = "isabelle"; + exec = "isabelle jedit"; + icon = "isabelle"; + desktopName = "Isabelle"; + comment = meta.description; + categories = "Education;Science;Math;"; + }; + meta = with lib; { description = "A generic proof assistant"; diff --git a/pkgs/applications/science/logic/logisim/default.nix b/pkgs/applications/science/logic/logisim/default.nix index 1ca22cf769c..f94f08e43ab 100644 --- a/pkgs/applications/science/logic/logisim/default.nix +++ b/pkgs/applications/science/logic/logisim/default.nix @@ -1,29 +1,50 @@ -{ lib, stdenv, fetchurl, jre, makeWrapper }: +{ lib, stdenv, fetchurl, jre, makeWrapper, copyDesktopItems, makeDesktopItem, unzip }: -let version = "2.7.1"; in - -stdenv.mkDerivation { +stdenv.mkDerivation rec { pname = "logisim"; - inherit version; + version = "2.7.1"; src = fetchurl { - url = "mirror://sourceforge/project/circuit/2.7.x/${version}/logisim-generic-${version}.jar"; + url = "mirror://sourceforge/project/circuit/${lib.versions.majorMinor version}.x/${version}/logisim-generic-${version}.jar"; sha256 = "1hkvc9zc7qmvjbl9579p84hw3n8wl3275246xlzj136i5b0phain"; }; - phases = [ "installPhase" ]; + dontUnpack = true; + + nativeBuildInputs = [ makeWrapper copyDesktopItems unzip ]; - nativeBuildInputs = [makeWrapper]; + desktopItems = [ + (makeDesktopItem { + name = pname; + desktopName = "Logisim"; + exec = "logisim"; + icon = "logisim"; + comment = meta.description; + categories = "Education;"; + }) + ]; installPhase = '' - mkdir -pv $out/bin + runHook preInstall + + mkdir -p $out/bin makeWrapper ${jre}/bin/java $out/bin/logisim --add-flags "-jar $src" + + # Create icons + unzip $src "resources/logisim/img/*" + for size in 16 20 24 48 64 128 + do + install -D "./resources/logisim/img/logisim-icon-$size.png" "$out/share/icons/hicolor/''${size}x''${size}/apps/logisim.png" + done + + runHook postInstall ''; - meta = { - homepage = "http://ozark.hendrix.edu/~burch/logisim"; + meta = with lib; { + homepage = "http://www.cburch.com/logisim/"; description = "Educational tool for designing and simulating digital logic circuits"; - license = lib.licenses.gpl2Plus; - platforms = lib.platforms.unix; + maintainers = with maintainers; [ angustrau ]; + license = licenses.gpl2Plus; + platforms = platforms.unix; }; } diff --git a/pkgs/applications/science/logic/potassco/clingcon.nix b/pkgs/applications/science/logic/potassco/clingcon.nix index 4d64a813e62..0f3218b7673 100644 --- a/pkgs/applications/science/logic/potassco/clingcon.nix +++ b/pkgs/applications/science/logic/potassco/clingcon.nix @@ -32,7 +32,6 @@ stdenv.mkDerivation rec { ]; meta = { - inherit version; description = "Extension of clingo to handle constraints over integers"; license = lib.licenses.gpl3; # for now GPL3, next version MIT! platforms = lib.platforms.unix; diff --git a/pkgs/applications/science/logic/potassco/clingo.nix b/pkgs/applications/science/logic/potassco/clingo.nix index 091b098fa3f..2e907a2d3a3 100644 --- a/pkgs/applications/science/logic/potassco/clingo.nix +++ b/pkgs/applications/science/logic/potassco/clingo.nix @@ -14,7 +14,6 @@ stdenv.mkDerivation rec { cmakeFlags = [ "-DCLINGO_BUILD_WITH_PYTHON=OFF" ]; meta = { - inherit version; description = "ASP system to ground and solve logic programs"; license = lib.licenses.mit; maintainers = [lib.maintainers.raskin]; diff --git a/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix index 8c88f47327e..9bfad1fa010 100644 --- a/pkgs/applications/science/logic/satallax/default.nix +++ b/pkgs/applications/science/logic/satallax/default.nix @@ -60,7 +60,6 @@ stdenv.mkDerivation rec { ''; meta = { - inherit version; description = "Automated theorem prover for higher-order logic"; license = lib.licenses.mit ; maintainers = [lib.maintainers.raskin]; diff --git a/pkgs/applications/science/logic/z3/tptp.nix b/pkgs/applications/science/logic/z3/tptp.nix index bb912742b7c..23136ddf7a7 100644 --- a/pkgs/applications/science/logic/z3/tptp.nix +++ b/pkgs/applications/science/logic/z3/tptp.nix @@ -23,7 +23,6 @@ stdenv.mkDerivation rec { ''; meta = { - inherit version; inherit (z3.meta) license homepage platforms; description = "TPTP wrapper for Z3 prover"; maintainers = [lib.maintainers.raskin]; |