Merge remote-tracking branch 'NixOS/master' into staging

4 files changed, 63 insertions, 3 deletions

diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 5fab9788a94..0a4e1dddcae 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -25,7 +25,7 @@ let
    "8.8.0" = "13a4fka22hdxsjk11mgjb9ffzplfxyxp1sg5v1c8nk1grxlscgw8";
    "8.8.1" = "1hlf58gwazywbmfa48219amid38vqdl94yz21i11b4map6jfwhbk";
    "8.8.2" = "1lip3xja924dm6qblisk1bk0x8ai24s5xxqxphbdxj6djglj68fd";
-   "8.9+beta1" = "1yxv2klqal3mh6symi3gc6gv3xm684zlld2c0b6ijhjmp865cin8";
+   "8.9.0" = "1dkgdjc4n1m15m1p724hhi5cyxpqbjw6rxc5na6fl3v4qjjfnizh";
   }."${version}";
   coq-version = builtins.substring 0 3 version;
   ideFlags = if buildIde then "-lablgtkdir ${ocamlPackages.lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
diff --git a/pkgs/applications/science/logic/leo3/binary.nix b/pkgs/applications/science/logic/leo3/binary.nix
new file mode 100644
index 00000000000..a3834dc70b6
--- /dev/null
+++ b/pkgs/applications/science/logic/leo3/binary.nix
@@ -0,0 +1,29 @@
+{stdenv, fetchurl, openjdk}:
+stdenv.mkDerivation rec {
+  pname = "leo3";
+  version = "1.2";
+
+  jar = fetchurl {
+    url = "https://github.com/leoprover/Leo-III/releases/download/v${version}/leo3.jar";
+    sha256 = "1lgwxbr1rnk72rnvc8raq5i1q71ckhn998pwd9xk6zf27wlzijk7";
+  };
+
+  phases=["installPhase" "fixupPhase"];
+
+  installPhase = ''
+    mkdir -p "$out"/{bin,lib/java/leo3}
+    cp "${jar}" "$out/lib/java/leo3/leo3.jar"
+    echo "#!${stdenv.shell}" > "$out/bin/leo3"
+    echo "'${openjdk}/bin/java' -jar '$out/lib/java/leo3/leo3.jar' \"\$@\""  > "$out/bin/leo3"
+    chmod a+x "$out/bin/leo3"
+  '';
+
+  meta = {
+    inherit version;
+    description = "An automated theorem prover for classical higher-order logic with choice";
+    license = stdenv.lib.licenses.bsd3;
+    maintainers = [stdenv.lib.maintainers.raskin];
+    platforms = stdenv.lib.platforms.linux;
+    homepage = "https://page.mi.fu-berlin.de/lex/leo3/";
+  };
+}
diff --git a/pkgs/applications/science/logic/z3/tptp.nix b/pkgs/applications/science/logic/z3/tptp.nix
new file mode 100644
index 00000000000..34449542abb
--- /dev/null
+++ b/pkgs/applications/science/logic/z3/tptp.nix
@@ -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];
+  };
+}
diff --git a/pkgs/applications/science/math/mathematica/l10ns.nix b/pkgs/applications/science/math/mathematica/l10ns.nix
index 2158021c754..065360a112d 100644
--- a/pkgs/applications/science/math/mathematica/l10ns.nix
+++ b/pkgs/applications/science/math/mathematica/l10ns.nix
@@ -5,10 +5,10 @@ with lib;
   l10ns = flip map
   [
     {
-      version = "11.2.0";
+      version = "11.3.0";
       lang = "en";
       language = "English";
-      sha256 = "4a1293cc1c404303aa1cab1bd273c7be151d37ac5ed928fbbb18e9c5ab2d8df9";
+      sha256 = "0fcfe208c1eac8448e7be3af0bdb84370b17bd9c5d066c013928c8ee95aed10e";
     }
     {
       version = "11.2.0";