nixpkgs: merge nixos-unstable

10 files changed, 48 insertions, 36 deletions

diff --git a/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix
index f3049a659d11..2a8c058a80bb 100644
--- a/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix
+++ b/nixpkgs/pkgs/applications/science/logic/clprover/clprover.nix
@@ -5,7 +5,7 @@ stdenv.mkDerivation {
   version = "1.0.3";
 
   src = fetchzip {
-    url = "http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/CLProver++-v1.0.3-18-04-2015.zip";
+    url = "https://cgi.csc.liv.ac.uk/~ullrich/CLProver++/CLProver++-v1.0.3-18-04-2015.zip";
     sha256 = "10kmlg4m572qwfzi6hkyb0ypb643xw8sfb55xx7866lyh37w1q3s";
     stripRoot = false;
   };
@@ -19,7 +19,7 @@ stdenv.mkDerivation {
 
   meta = with lib; {
     description = "Resolution-based theorem prover for Coalition Logic implemented in C++";
-    homepage = "http://cgi.csc.liv.ac.uk/~ullrich/CLProver++/";
+    homepage = "https://cgi.csc.liv.ac.uk/~ullrich/CLProver++/";
     license = licenses.gpl3; # Note that while the website states that it is GPLv2 but the file in the zip as well as the comments in the source state it is GPLv3
     maintainers = with maintainers; [ mgttlinger ];
     platforms = [ "x86_64-linux" ];
diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
index a2ff8382947b..62600ea90c20 100644
--- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
@@ -13,7 +13,8 @@
 , csdp ? null
 , version, coq-version ? null,
 }@args:
-let lib = import ../../../../build-support/coq/extra-lib.nix {inherit (stdenv) lib;}; in
+let lib' = lib; in
+let lib = import ../../../../build-support/coq/extra-lib.nix {lib = lib';}; in
 with builtins; with lib;
 let
   release = {
@@ -40,11 +41,11 @@ let
    "8.12.0".sha256     = "18dc7k0piv6v064zgdadpw6mkkxk7j663hb3svgj5236fihjr0cz";
    "8.12.1".sha256     = "1rkcyjjrzcqw9xk93hsq0vvji4f8r5iq0f739mghk60bghkpnb7q";
    "8.12.2".sha256     = "18gscfm039pqhq4msq01nraig5dm9ab98bjca94zldf8jvdv0x2n";
-   "8.13+beta1".sha256 = "1v4a6dpj41flspa4ihcr7m5ahqz10kbn62fmrldmv7gzq6jsyfyq";
+   "8.13.0".sha256     = "0sjbqmz6qcvnz0hv87xha80qbhvmmyd675wyc5z4rgr34j2l1ymd";
   };
   releaseRev = v: "V${v}";
   fetched = import ../../../../build-support/coq/meta-fetch/default.nix
-    { inherit stdenv fetchzip; }
+    { inherit lib stdenv fetchzip; }
     { inherit release releaseRev; location = { owner = "coq"; repo = "coq";}; }
     args.version;
   version = fetched.version;
diff --git a/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix
index 6c22c949483f..a0f81a543f18 100644
--- a/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/isabelle/default.nix
@@ -1,4 +1,4 @@
-{ lib, stdenv, fetchurl, perl, nettools, java, polyml, z3, rlwrap }:
+{ lib, stdenv, fetchurl, perl, perlPackages, makeWrapper, nettools, java, polyml, z3, rlwrap }:
 # nettools needed for hostname
 
 stdenv.mkDerivation rec {
@@ -17,7 +17,7 @@ stdenv.mkDerivation rec {
       sha256 = "1bibabhlsvf6qsjjkgxcpq3cvl1z7r8yfcgqbhbvsiv69n3gyfk3";
     };
 
-  buildInputs = [ perl polyml z3 ]
+  buildInputs = [ perl polyml z3 makeWrapper ]
              ++ lib.optionals (!stdenv.isDarwin) [ nettools java ];
 
   sourceRoot = dirname;
@@ -64,6 +64,8 @@ stdenv.mkDerivation rec {
     mv $TMP/$dirname $out
     cd $out/$dirname
     bin/isabelle install $out/bin
+
+    wrapProgram $out/$dirname/src/HOL/Tools/ATP/scripts/remote_atp --set PERL5LIB ${perlPackages.makeFullPerlPath [ perlPackages.LWP ]}
   '';
 
   meta = with lib; {
diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix
index 1f3f7afa9d1b..7749f4fd72dd 100644
--- a/nixpkgs/pkgs/applications/science/logic/lean/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/lean/default.nix
@@ -2,13 +2,13 @@
 
 stdenv.mkDerivation rec {
   pname = "lean";
-  version = "3.25.0";
+  version = "3.26.0";
 
   src = fetchFromGitHub {
     owner  = "leanprover-community";
     repo   = "lean";
     rev    = "v${version}";
-    sha256 = "sha256-/TlVoqgTGhRfC8d70kXc+VsEkURUksKNGRjYcww+F8g=";
+    sha256 = "sha256-xCULu6ljfyrA/Idr/BJ+3rLVmQqJZPoo+a7s++u50zU=";
   };
 
   nativeBuildInputs = [ cmake ];
diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix
index 5118795978d1..38039f61fda6 100644
--- a/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/default.nix
@@ -1,6 +1,6 @@
 { mkDerivation, callPackage, buildPackages
 , async, base, bytestring, containers, fetchFromGitLab, mtl
-, parallel-io, parsec, lib, stdenv, stm, transformers
+, parallel-io, parsec, lib, stm, transformers
 }:
 let
   z3 = callPackage ./z3.nix { gomp = null; z3 = buildPackages.z3; };
diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix
index 96e216417df1..f0c8dd249048 100644
--- a/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix
+++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/sbv-7.13.nix
@@ -1,7 +1,7 @@
 { mkDerivation, array, async, base, bytestring, containers
 , crackNum, deepseq, directory, doctest, filepath, generic-deriving
 , ghc, Glob, hlint, mtl, pretty, process, QuickCheck, random
-, lib, stdenv, syb, tasty, tasty-golden, tasty-hunit, tasty-quickcheck
+, lib, syb, tasty, tasty-golden, tasty-hunit, tasty-quickcheck
 , template-haskell, time, z3
 }:
 mkDerivation {
diff --git a/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix b/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix
index 3574954c376c..a20ccea16dc7 100644
--- a/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix
+++ b/nixpkgs/pkgs/applications/science/logic/petrinizer/z3.nix
@@ -1,5 +1,5 @@
 { mkDerivation, fetchpatch
-, base, containers, gomp, hspec, QuickCheck, lib, stdenv
+, base, containers, gomp, hspec, QuickCheck, lib
 , transformers, z3
 }:
 mkDerivation {
diff --git a/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix
index 1dd6dc1cfc89..3eabc9422e38 100644
--- a/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/saw-tools/default.nix
@@ -53,7 +53,7 @@ stdenv.mkDerivation {
   meta = {
     description = "Tools for software verification and analysis";
     homepage    = "https://saw.galois.com";
-    license     = lib.licenses.unfreeRedistributable;
+    license     = lib.licenses.bsd3;
     platforms   = lib.platforms.linux;
     maintainers = [ lib.maintainers.thoughtpolice ];
   };
diff --git a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
index 1f2ad4634de2..118bb8ecd206 100644
--- a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
@@ -31,6 +31,9 @@ stdenv.mkDerivation {
 
     substituteInPlace sbysrc/sby_core.py \
       --replace '##yosys-program-prefix##' '"${yosys}/bin/"'
+
+    substituteInPlace sbysrc/sby.py \
+      --replace '/usr/bin/env python3' '${python3}/bin/python'
   '';
 
   buildPhase = "true";
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
index cd58740186fe..cfef5960bd9c 100644
--- a/nixpkgs/pkgs/applications/science/logic/z3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
@@ -1,9 +1,15 @@
-{ lib, stdenv, fetchFromGitHub, python, fixDarwinDylibNames
+{ lib
+, stdenv
+, fetchFromGitHub
+, python
+, fixDarwinDylibNames
 , javaBindings ? false
 , ocamlBindings ? false
 , pythonBindings ? true
 , jdk ? null
-, ocaml ? null, findlib ? null, zarith ? null
+, ocaml ? null
+, findlib ? null
+, zarith ? null
 }:
 
 assert javaBindings -> jdk != null;
@@ -13,19 +19,19 @@ with lib;
 
 stdenv.mkDerivation rec {
   pname = "z3";
-  version = "4.8.9";
+  version = "4.8.10";
 
   src = fetchFromGitHub {
-    owner  = "Z3Prover";
-    repo   = pname;
-    rev    = "z3-${version}";
-    sha256 = "1hnbzq10d23drd7ksm3c1n2611c3kd0q0yxgz8y78zaafwczvwxx";
+    owner = "Z3Prover";
+    repo = pname;
+    rev = "z3-${version}";
+    sha256 = "1w1ym2l0gipvjx322npw7lhclv8rslq58gnj0d9i96masi3gbycf";
   };
 
   nativeBuildInputs = optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames;
   buildInputs = [ python ]
-  ++ optional javaBindings jdk
-  ++ optionals ocamlBindings [ ocaml findlib zarith ]
+    ++ optional javaBindings jdk
+    ++ optionals ocamlBindings [ ocaml findlib zarith ]
   ;
   propagatedBuildInputs = [ python.pkgs.setuptools ];
   enableParallelBuilding = true;
@@ -35,16 +41,17 @@ stdenv.mkDerivation rec {
     mkdir -p $OCAMLFIND_DESTDIR/stublibs
   '';
 
-  configurePhase = concatStringsSep " " (
-    [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ]
-    ++ optional javaBindings   "--java"
-    ++ optional ocamlBindings  "--ml"
-    ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}"
-  ) + "\n" + "cd build";
+  configurePhase = concatStringsSep " "
+    (
+      [ "${python.interpreter} scripts/mk_make.py --prefix=$out" ]
+        ++ optional javaBindings "--java"
+        ++ optional ocamlBindings "--ml"
+        ++ optional pythonBindings "--python --pypkgdir=$out/${python.sitePackages}"
+    ) + "\n" + "cd build";
 
   postInstall = ''
     mkdir -p $dev $lib
-    mv $out/lib     $lib/lib
+    mv $out/lib $lib/lib
     mv $out/include $dev/include
   '' + optionalString pythonBindings ''
     mkdir -p $python/lib
@@ -53,14 +60,13 @@ stdenv.mkDerivation rec {
   '';
 
   outputs = [ "out" "lib" "dev" "python" ]
-  ++ optional ocamlBindings "ocaml"
-  ;
+    ++ optional ocamlBindings "ocaml";
 
-  meta = {
+  meta = with lib; {
     description = "A high-performance theorem prover and SMT solver";
-    homepage    = "https://github.com/Z3Prover/z3";
-    license     = lib.licenses.mit;
-    platforms   = lib.platforms.unix;
-    maintainers = with lib.maintainers; [ thoughtpolice ttuegel ];
+    homepage = "https://github.com/Z3Prover/z3";
+    license = licenses.mit;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ thoughtpolice ttuegel ];
   };
 }