Merge commit 'b3c692172e5b5241b028a98e1977f9fb12eeaf42'

15 files changed, 215 insertions, 56 deletions

diff --git a/nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix b/nixpkgs/pkgs/applications/science/logic/bitwuzla/default.nix
new file mode 100644
index 000000000000..a8820b55b746
--- /dev/null
+++ b/nixpkgs/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/nixpkgs/pkgs/applications/science/logic/cadical/default.nix b/nixpkgs/pkgs/applications/science/logic/cadical/default.nix
index ca5e6b5c4195..f0cb1efb3050 100644
--- a/nixpkgs/pkgs/applications/science/logic/cadical/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cadical/default.nix
@@ -2,23 +2,39 @@
 
 stdenv.mkDerivation rec {
   pname = "cadical";
-  version = "1.3.0";
+  version = "1.4.1";
 
   src = fetchFromGitHub {
     owner = "arminbiere";
     repo = "cadical";
     rev = "rel-${version}";
-    sha256 = "05lvnvapjawgkky38xknb9lgaliiwan4kggmb9yggl4ifpjrh8qf";
+    sha256 = "0y44z3np4gssgdh4aj5qila7pshrbphycdxn2083i8ayyyjbxshp";
   };
 
+  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/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
index a49262e7cb65..1fb4693d64a2 100644
--- a/nixpkgs/pkgs/applications/science/logic/elan/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
@@ -7,16 +7,16 @@ in
 
 rustPlatform.buildRustPackage rec {
   pname = "elan";
-  version = "1.0.6";
+  version = "1.0.7";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "elan";
     rev = "v${version}";
-    sha256 = "sha256-Ns8vSS/PDlfopigW4Nz3fdR9PCMG8gDoL36+/s0Qkeo=";
+    sha256 = "sha256-SFY9RbUHoaOXCaK+uIqhnKbzSkbtWiS6os/JvsggagI=";
   };
 
-  cargoSha256 = "sha256-NDtldiVo4SyE88f6ntKn1WJDFdvwN5Ps4DxQH15iNZE=";
+  cargoSha256 = "sha256-6TFionZw76V4htYQrz8eLX7ioW7Fbgd63rtz53s0TLU=";
 
   nativeBuildInputs = [ pkg-config makeWrapper ];
 
diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix
index ea2cd356e315..5c6ad241cb76 100644
--- a/nixpkgs/pkgs/applications/science/logic/lean/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix
@@ -2,7 +2,7 @@
 
 stdenv.mkDerivation rec {
   pname = "lean";
-  version = "3.31.0";
+  version = "3.32.1";
 
   src = fetchFromGitHub {
     owner  = "leanprover-community";
@@ -11,8 +11,8 @@ stdenv.mkDerivation rec {
     # from. this is then used to check whether an olean file should be
     # rebuilt. don't use a tag as rev because this will get replaced into
     # src/githash.h.in in preConfigure.
-    rev    = "333783350cd3fe38f25fed1da7d6a433d8f85b77";
-    sha256 = "sha256-N8Ju7pSGssvt84/0e1o6G/p7fWM1c0Mzw+ftL1/++J4=";
+    rev    = "35b3a9c4e2d35cccb5ed220ea2f2909a4ed2ca90";
+    sha256 = "0s69smknsvycvydbk2f3vcqj1z3jrbv3k048z2r46391dai5iwhf";
   };
 
   nativeBuildInputs = [ cmake ];
diff --git a/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix
new file mode 100644
index 000000000000..10266abffea1
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/logisim-evolution/default.nix
@@ -0,0 +1,46 @@
+{ lib, stdenv, fetchurl, jre, makeWrapper, copyDesktopItems, makeDesktopItem, unzip }:
+
+stdenv.mkDerivation rec {
+  pname = "logisim-evolution";
+  version = "3.5.0";
+
+  src = fetchurl {
+    url = "https://github.com/logisim-evolution/logisim-evolution/releases/download/v${version}/logisim-evolution-${version}-all.jar";
+    sha256 = "1r6im4gmjbnckx8jig6bxi5lxv06lwdnpxkyfalsfmw4nybd5arw";
+  };
+
+  dontUnpack = true;
+
+  nativeBuildInputs = [ makeWrapper copyDesktopItems unzip ];
+
+  desktopItems = [
+    (makeDesktopItem {
+      name = pname;
+      desktopName = "Logisim-evolution";
+      exec = "logisim-evolution";
+      icon = "logisim-evolution";
+      comment = meta.description;
+      categories = "Education;";
+    })
+  ];
+
+  installPhase = ''
+    runHook preInstall
+
+    mkdir -p $out/bin
+    makeWrapper ${jre}/bin/java $out/bin/logisim-evolution --add-flags "-jar $src"
+
+    unzip $src resources/logisim/img/logisim-icon.svg
+    install -D resources/logisim/img/logisim-icon.svg $out/share/pixmaps/logisim-evolution.svg
+
+    runHook postInstall
+  '';
+
+  meta = with lib; {
+    homepage = "https://github.com/logisim-evolution/logisim-evolution";
+    description = "Digital logic designer and simulator";
+    maintainers = with maintainers; [ angustrau ];
+    license = licenses.gpl2Plus;
+    platforms = platforms.unix;
+  };
+}
diff --git a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix
index 9b3f42dd4ba8..f94f08e43ab2 100644
--- a/nixpkgs/pkgs/applications/science/logic/logisim/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/logisim/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchurl, jre, makeWrapper }:
+{ lib, stdenv, fetchurl, jre, makeWrapper, copyDesktopItems, makeDesktopItem, unzip }:
 
 stdenv.mkDerivation rec {
   pname = "logisim";
@@ -11,17 +11,39 @@ stdenv.mkDerivation rec {
 
   dontUnpack = true;
 
-  nativeBuildInputs = [ makeWrapper ];
+  nativeBuildInputs = [ makeWrapper copyDesktopItems unzip ];
+
+  desktopItems = [
+    (makeDesktopItem {
+      name = pname;
+      desktopName = "Logisim";
+      exec = "logisim";
+      icon = "logisim";
+      comment = meta.description;
+      categories = "Education;";
+    })
+  ];
 
   installPhase = ''
+    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 = with lib; {
-    homepage = "http://ozark.hendrix.edu/~burch/logisim";
+    homepage = "http://www.cburch.com/logisim/";
     description = "Educational tool for designing and simulating digital logic circuits";
-    maintainers = with maintainers; [ ];
+    maintainers = with maintainers; [ angustrau ];
     license = licenses.gpl2Plus;
     platforms = platforms.unix;
   };
diff --git a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix
index 1681d4545904..fd22b7b1add8 100644
--- a/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/opensmt/default.nix
@@ -6,13 +6,13 @@
 
 stdenv.mkDerivation rec {
   pname = "opensmt";
-  version = "2.0.1";
+  version = "2.1.0";
 
   src = fetchFromGitHub {
     owner = "usi-verification-and-security";
     repo = "opensmt";
     rev = "v${version}";
-    sha256 = "uoIcXWsxxRsIuFsou3RcN9e48lc7cWMgRPVJLFVslDE=";
+    sha256 = "sha256-m8TpMBY1r0h8GJTHM4FLBuZtX+WK/Q7RTXUnNmUWV+o=";
   };
 
   nativeBuildInputs = [ cmake bison flex ];
diff --git a/nixpkgs/pkgs/applications/science/logic/poly/default.nix b/nixpkgs/pkgs/applications/science/logic/poly/default.nix
index 75ad91bc54de..c80b9bf1f0c4 100644
--- a/nixpkgs/pkgs/applications/science/logic/poly/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/poly/default.nix
@@ -2,14 +2,14 @@
 
 stdenv.mkDerivation rec {
   pname = "libpoly";
-  version = "0.1.9";
+  version = "0.1.10";
 
   src = fetchFromGitHub {
     owner = "SRI-CSL";
     repo = "libpoly";
     # they've pushed to the release branch, use explicit tag
     rev = "refs/tags/v${version}";
-    sha256 = "sha256-E2lHo8Bt4ujoGQ623fjkQbqRnDYJYilXdRt4lnF4wJk=";
+    sha256 = "sha256-22Y4L5NFnCzKwZt0A/ChMuGPU4Dk1Qyke6mdvfN063w=";
   };
 
   # https://github.com/SRI-CSL/libpoly/pull/52
diff --git a/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix
index 3eabc9422e38..df99d067f08c 100644
--- a/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix
@@ -48,8 +48,6 @@ stdenv.mkDerivation {
     done
   '';
 
-  phases = "unpackPhase installPhase fixupPhase";
-
   meta = {
     description = "Tools for software verification and analysis";
     homepage    = "https://saw.galois.com";
diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
index 89bdd979fea0..90a4aeb4f8ab 100644
--- a/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
+++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/tlaps.nix
@@ -1,6 +1,12 @@
 { fetchurl
-, lib, stdenv
-, ocaml, isabelle, cvc3, perl, wget, which
+, lib
+, stdenv
+, ocaml
+, isabelle
+, cvc3
+, perl
+, wget
+, which
 }:
 
 stdenv.mkDerivation rec {
@@ -13,8 +19,6 @@ stdenv.mkDerivation rec {
 
   buildInputs = [ ocaml isabelle cvc3 perl wget which ];
 
-  phases = [ "unpackPhase" "installPhase" ];
-
   installPhase = ''
     mkdir -pv "$out"
     export HOME="$out"
@@ -45,9 +49,9 @@ stdenv.mkDerivation rec {
       and scalable to large system specifications. It provides a
       consistent abstraction over the various “backend” verifiers.
     '';
-    homepage    = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html";
-    license     = lib.licenses.bsd2;
-    platforms   = lib.platforms.unix;
+    homepage = "https://tla.msr-inria.inria.fr/tlaps/content/Home.html";
+    license = lib.licenses.bsd2;
+    platforms = lib.platforms.unix;
     maintainers = [ ];
   };
 
diff --git a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix
index ef2d97ef6bfc..21c60d03ac1e 100644
--- a/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix
+++ b/nixpkgs/pkgs/applications/science/logic/tlaplus/toolbox.nix
@@ -1,5 +1,13 @@
-{ lib, fetchzip, makeWrapper, makeDesktopItem, stdenv
-, gtk3, libXtst, glib, zlib, wrapGAppsHook
+{ lib
+, fetchzip
+, makeWrapper
+, makeDesktopItem
+, stdenv
+, gtk3
+, libXtst
+, glib
+, zlib
+, wrapGAppsHook
 }:
 
 let
@@ -17,7 +25,8 @@ let
   };
 
 
-in stdenv.mkDerivation rec {
+in
+stdenv.mkDerivation rec {
   pname = "tla-toolbox";
   version = "1.7.1";
   src = fetchzip {
@@ -31,8 +40,6 @@ in stdenv.mkDerivation rec {
 
   dontWrapGApps = true;
 
-  phases = [ "installPhase" ];
-
   installPhase = ''
     runHook preInstall
 
diff --git a/nixpkgs/pkgs/applications/science/logic/verifast/default.nix b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix
index e426f7b80989..c610256ccaef 100644
--- a/nixpkgs/pkgs/applications/science/logic/verifast/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/verifast/default.nix
@@ -20,11 +20,11 @@ let
 in
 stdenv.mkDerivation rec {
   pname = "verifast";
-  version = "19.12";
+  version = "21.04";
 
   src = fetchurl {
     url    = "https://github.com/verifast/verifast/releases/download/${version}/${pname}-${version}-linux.tar.gz";
-    sha256 = "169kshjq4cf4i9v92azv0xaflrnik5686w7fwcgdhd6qkbzflzl6";
+    sha256 = "sha256-PlRsf4wFXoM+E+60SbeKzs/RZK0HNVirX47AnI6NeYM=";
   };
 
   dontConfigure = true;
@@ -42,7 +42,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "Verification for C and Java programs via separation logic";
-    homepage    = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/";
+    homepage    = "https://people.cs.kuleuven.be/~bart.jacobs/verifast/";
     license     = lib.licenses.mit;
     platforms   = [ "x86_64-linux" ];
     maintainers = [ lib.maintainers.thoughtpolice ];
diff --git a/nixpkgs/pkgs/applications/science/logic/why3/default.nix b/nixpkgs/pkgs/applications/science/logic/why3/default.nix
index 924ff3fd9fd2..b9f14332f9d8 100644
--- a/nixpkgs/pkgs/applications/science/logic/why3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/why3/default.nix
@@ -1,12 +1,12 @@
 { callPackage, fetchurl, fetchpatch, lib, stdenv
 , ocamlPackages, coqPackages, rubber, hevea, emacs }:
 
-stdenv.mkDerivation {
+stdenv.mkDerivation rec {
   pname = "why3";
   version = "1.4.0";
 
   src = fetchurl {
-    url = "https://gforge.inria.fr/frs/download.php/file/38425/why3-1.4.0.tar.gz";
+    url = "https://gforge.inria.fr/frs/download.php/file/38425/why3-${version}.tar.gz";
     sha256 = "0lw0cpx347zz9vvwqibmbxgs80fsd16scgk3isscvwxnajpc3rv8";
   };
 
diff --git a/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix b/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix
index d4fdbfd6937c..fc08f5d7c85e 100644
--- a/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix
+++ b/nixpkgs/pkgs/applications/science/logic/why3/with-provers.nix
@@ -1,31 +1,30 @@
 { stdenv, makeWrapper, runCommand, symlinkJoin, why3 }:
 provers:
 let configAwkScript = runCommand "why3-conf.awk" { inherit provers; }
-    ''
-      for p in $provers; do
-        for b in $p/bin/*; do
-          BASENAME=$(basename $b)
-          echo "/^command =/{ gsub(\"$BASENAME\", \"$b\") }" >> $out
-        done
+  ''
+    for p in $provers; do
+      for b in $p/bin/*; do
+        BASENAME=$(basename $b)
+        echo "/^command =/{ gsub(\"$BASENAME\", \"$b\") }" >> $out
       done
-      echo '{ print }' >> $out
-    '';
-in stdenv.mkDerivation {
+    done
+    echo '{ print }' >> $out
+  '';
+in
+stdenv.mkDerivation {
   name = "${why3.name}-with-provers";
 
-  phases = [ "buildPhase" "installPhase" ];
-
   nativeBuildInputs = [ makeWrapper ];
   buildInputs = [ why3 ] ++ provers;
 
   buildPhase = ''
-      mkdir -p $out/share/why3/
-      why3 config --detect-provers -C $out/share/why3/why3.conf
-      awk -i inplace -f ${configAwkScript} $out/share/why3/why3.conf
+    mkdir -p $out/share/why3/
+    why3 config --detect-provers -C $out/share/why3/why3.conf
+    awk -i inplace -f ${configAwkScript} $out/share/why3/why3.conf
   '';
 
   installPhase = ''
-      mkdir -p $out/bin
-      makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-config $out/share/why3/why3.conf"
+    mkdir -p $out/bin
+    makeWrapper ${why3}/bin/why3 $out/bin/why3 --add-flags "--extra-config $out/share/why3/why3.conf"
   '';
 }
diff --git a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix
index 63a946365604..2829cb59340b 100644
--- a/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/workcraft/default.nix
@@ -2,11 +2,11 @@
 
 stdenv.mkDerivation rec {
   pname = "workcraft";
-  version = "3.3.2";
+  version = "3.3.5";
 
   src = fetchurl {
     url = "https://github.com/workcraft/workcraft/releases/download/v${version}/workcraft-v${version}-linux.tar.gz";
-    sha256 = "0v71x3fph2j3xrnysvkm7zsgnbxisfbdfgxzvzxxfdg59a6l3xid";
+    sha256 = "sha256-KErKYK3mmjp5uNdGQnjzUUIEwXT5fqbAPUunH72Mtig=";
   };
 
   nativeBuildInputs = [ makeWrapper ];