Merge commit 'a323570a264da96a0b0bcc1c9aa017794acdc752'

11 files changed, 58 insertions, 68 deletions

diff --git a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
index 963015b11d50..837f25e320f7 100644
--- a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -2,13 +2,13 @@
 
 let
   pname = "alt-ergo";
-  version = "2.4.0";
+  version = "2.4.1";
 
   src = fetchFromGitHub {
     owner = "OCamlPro";
     repo = pname;
     rev = version;
-    sha256 = "1jm1yrvsg8iyfp9bb728zdx2i7yb6z7minjrfs27k5ncjqkjm65g";
+    sha256 = "0hglj1p0753w2isds01h90knraxa42d2jghr35dpwf9g8a1sm9d3";
   };
 
   useDune2 = true;
diff --git a/nixpkgs/pkgs/applications/science/logic/cadical/default.nix b/nixpkgs/pkgs/applications/science/logic/cadical/default.nix
index f0cb1efb3050..c6b1f6652451 100644
--- a/nixpkgs/pkgs/applications/science/logic/cadical/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/cadical/default.nix
@@ -30,6 +30,7 @@ stdenv.mkDerivation rec {
     install -Dm0755 build/cadical "$out/bin/cadical"
     install -Dm0755 build/mobical "$out/bin/mobical"
     install -Dm0644 src/ccadical.h "$dev/include/ccadical.h"
+    install -Dm0644 src/cadical.hpp "$dev/include/cadical.hpp"
     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}/"
diff --git a/nixpkgs/pkgs/applications/science/logic/coq/default.nix b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
index e595bf47c67c..16db7384df17 100644
--- a/nixpkgs/pkgs/applications/science/logic/coq/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/coq/default.nix
@@ -44,6 +44,7 @@ let
    "8.13.0".sha256     = "0sjbqmz6qcvnz0hv87xha80qbhvmmyd675wyc5z4rgr34j2l1ymd";
    "8.13.1".sha256     = "0xx2ns84mlip9bg2mkahy3pmc5zfcgrjxsviq9yijbzy1r95wf0n";
    "8.13.2".sha256     = "1884vbmwmqwn9ngibax6dhnqh4cc02l0s2ajc6jb1xgr0i60whjk";
+   "8.14.0".sha256     = "04y2z0qyvag66zanfyc3f9agvmzbn4lsr0p1l7ck6yjhqx7vbm17";
   };
   releaseRev = v: "V${v}";
   fetched = import ../../../../build-support/coq/meta-fetch/default.nix
@@ -163,7 +164,7 @@ self = stdenv.mkDerivation {
 
   prefixKey = "-prefix ";
 
-  buildFlags = [ "revision" "coq" "coqide" "bin/votour" ];
+  buildFlags = [ "revision" "coq" "coqide" ] ++ optional (!versionAtLeast "8.14") "bin/votour";
   enableParallelBuilding = true;
 
   createFindlibDestdir = true;
@@ -177,9 +178,11 @@ self = stdenv.mkDerivation {
     categories = "Development;Science;Math;IDE;GTK";
   });
 
-  postInstall = ''
+  postInstall = let suffix = if versionAtLeast "8.14" then "-core" else ""; in ''
     cp bin/votour $out/bin/
-    ln -s $out/lib/coq $OCAMLFIND_DESTDIR/coq
+    ln -s $out/lib/coq${suffix} $OCAMLFIND_DESTDIR/coq${suffix}
+  '' + optionalString (versionAtLeast "8.14") ''
+    ln -s $out/lib/coqide-server $OCAMLFIND_DESTDIR/coqide-server
   '' + optionalString buildIde ''
     mkdir -p "$out/share/pixmaps"
     ln -s "$out/share/coq/coq.png" "$out/share/pixmaps/"
diff --git a/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix b/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix
deleted file mode 100644
index 393b84640805..000000000000
--- a/nixpkgs/pkgs/applications/science/logic/coq2html/default.nix
+++ /dev/null
@@ -1,36 +0,0 @@
-{ lib, stdenv, fetchFromGitHub, ocaml }:
-
-stdenv.mkDerivation  rec {
-  pname = "coq2html";
-  version = "1.2";
-
-  src = fetchFromGitHub {
-    owner = "xavierleroy";
-    repo = "coq2html";
-    rev = "v${version}";
-    sha256 = "sha256-ty/6A3wivjDCrmlZAcZyaIwQQ+vPBJm9MhtW6nZcV3s=";
-  };
-
-  nativeBuildInputs = [ ocaml ];
-
-  installPhase = ''
-    mkdir -p $out/bin
-    cp coq2html $out/bin
-  '';
-
-  meta = with lib; {
-    description = "HTML documentation generator for Coq source files";
-    longDescription = ''
-      coq2html is an HTML documentation generator for Coq source files. It is
-      an alternative to the standard coqdoc documentation generator
-      distributed along with Coq. The major feature of coq2html is its ability
-      to fold proof scripts: in the generated HTML, proof scripts are
-      initially hidden, but can be revealed one by one by clicking on the
-      "Proof" keyword.
-    '';
-    homepage = "https://github.com/xavierleroy/coq2html";
-    license = licenses.gpl2Plus;
-    maintainers = with maintainers; [ jwiegley siraben ];
-    platforms = platforms.unix;
-  };
-}
diff --git a/nixpkgs/pkgs/applications/science/logic/elan/default.nix b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
index 1fb4693d64a2..987068d9bbb6 100644
--- a/nixpkgs/pkgs/applications/science/logic/elan/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/elan/default.nix
@@ -1,4 +1,5 @@
 { stdenv, lib, runCommand, patchelf, makeWrapper, pkg-config, curl
+, fetchpatch
 , openssl, gmp, zlib, fetchFromGitHub, rustPlatform, libiconv }:
 
 let
@@ -7,16 +8,16 @@ in
 
 rustPlatform.buildRustPackage rec {
   pname = "elan";
-  version = "1.0.7";
+  version = "1.1.0";
 
   src = fetchFromGitHub {
     owner = "leanprover";
     repo = "elan";
     rev = "v${version}";
-    sha256 = "sha256-SFY9RbUHoaOXCaK+uIqhnKbzSkbtWiS6os/JvsggagI=";
+    sha256 = "0xmml81krr0i18b14dymfdq43szpzws7qj8k404qab51lkqxyxsb";
   };
 
-  cargoSha256 = "sha256-6TFionZw76V4htYQrz8eLX7ioW7Fbgd63rtz53s0TLU=";
+  cargoSha256 = "sha256-xjJ39hoSDn0VUH0YcL+mQBXbzFcIvZ38dPjBxV/yVNc=";
 
   nativeBuildInputs = [ pkg-config makeWrapper ];
 
@@ -40,12 +41,17 @@ rustPlatform.buildRustPackage rec {
        --subst-var dynamicLinker \
        --subst-var libPath
     '')
+    # fix build, will be included in 1.1.1
+    (fetchpatch {
+      url = "https://github.com/leanprover/elan/commit/8d1dec09d67b2ac1768b111d24f1a1cabdd563fa.patch";
+      sha256 = "sha256-yMdnXqycu4VF9EKavZ85EuspvAqvzDSIm5894SB+3+A=";
+    })
   ];
 
   postInstall = ''
     pushd $out/bin
     mv elan-init elan
-    for link in lean leanpkg leanchecker leanc leanmake; do
+    for link in lean leanpkg leanchecker leanc leanmake lake; do
       ln -s elan $link
     done
     popd
diff --git a/nixpkgs/pkgs/applications/science/logic/lean/default.nix b/nixpkgs/pkgs/applications/science/logic/lean/default.nix
index 5c6ad241cb76..0c21ce109b8f 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.32.1";
+  version = "3.33.0";
 
   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    = "35b3a9c4e2d35cccb5ed220ea2f2909a4ed2ca90";
-    sha256 = "0s69smknsvycvydbk2f3vcqj1z3jrbv3k048z2r46391dai5iwhf";
+    rev    = "a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82";
+    sha256 = "03xz3c3dzjhvjzpa8811cgzzqzw8fpajmspykavmb259i391w0y7";
   };
 
   nativeBuildInputs = [ cmake ];
diff --git a/nixpkgs/pkgs/applications/science/logic/leo2/default.nix b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix
index fc2c1e5cba4c..cbc85c5544cc 100644
--- a/nixpkgs/pkgs/applications/science/logic/leo2/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/leo2/default.nix
@@ -1,20 +1,31 @@
-{ lib, stdenv, fetchurl, makeWrapper, eprover, ocaml, perl, zlib }:
+{ lib, stdenv, fetchurl, fetchpatch, makeWrapper, eprover, ocaml, camlp4, perl, zlib }:
 
 stdenv.mkDerivation rec {
   pname = "leo2";
-  version = "1.6.2";
+  version = "1.7.0";
 
   src = fetchurl {
     url = "https://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v${version}.tgz";
-    sha256 = "1wjpmizb181iygnd18lx7p77fwaci2clgzs5ix5j51cc8f3pazmv";
+    sha256 = "sha256:1b2q7vsz6s9ighypsigqjm1mzjiq3xgnz5id5ssb4rh9zm190r82";
   };
 
   nativeBuildInputs = [ makeWrapper ];
-  buildInputs = [ eprover ocaml perl zlib ];
-
-  sourceRoot = "leo2/src";
-
-  preConfigure = "patchShebangs configure";
+  buildInputs = [ eprover ocaml camlp4 perl zlib ];
+
+  patches = [ (fetchpatch {
+      url = "https://github.com/niklasso/minisat/commit/7eb6015313561a2586032574788fcb133eeaa19f.patch";
+      stripLen = 1;
+      extraPrefix = "lib/";
+      sha256 = "sha256:01ln7hi6nvvkqkhn9hciqizizz5qspvqffgksvgmzn9x7kdd9pnh";
+    })
+  ];
+
+  preConfigure = ''
+    cd src
+    patchShebangs configure
+    substituteInPlace Makefile.pre \
+      --replace '+camlp4' "${camlp4}/lib/ocaml/${ocaml.version}/site-lib/camlp4"
+  '';
 
   buildFlags = [ "opt" ];
 
diff --git a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
index 118bb8ecd206..87bd1e2e6370 100644
--- a/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/symbiyosys/default.nix
@@ -5,13 +5,13 @@
 
 stdenv.mkDerivation {
   pname = "symbiyosys";
-  version = "2020.08.22";
+  version = "2021.09.13";
 
   src = fetchFromGitHub {
     owner  = "YosysHQ";
     repo   = "SymbiYosys";
-    rev    = "33b0bb7d836fe2a73dc7b10587222f2a718beef4";
-    sha256 = "03rbrbwsji1sqcp2yhgbc0fca04zsryv2g4izjhdzv64nqjzjyhn";
+    rev    = "15278f13467bea24a7300e23ebc5555b9261facf";
+    sha256 = "sha256-gp9F4MaGgD6XfD7AjuB/LmMVcxFurqWHEiXPeyzlQzk=";
   };
 
   buildInputs = [ ];
diff --git a/nixpkgs/pkgs/applications/science/logic/yices/default.nix b/nixpkgs/pkgs/applications/science/logic/yices/default.nix
index c26504bf7bdc..c5fc3a738373 100644
--- a/nixpkgs/pkgs/applications/science/logic/yices/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/yices/default.nix
@@ -1,18 +1,19 @@
-{ lib, stdenv, fetchFromGitHub, gmp-static, gperf, autoreconfHook, libpoly }:
+{ lib, stdenv, fetchFromGitHub, cudd, gmp-static, gperf, autoreconfHook, libpoly }:
 
 stdenv.mkDerivation rec {
   pname = "yices";
-  version = "2.6.1";
+  # We never want X.Y.${odd} versions as they are moving development tags.
+  version = "2.6.2";
 
   src = fetchFromGitHub {
     owner  = "SRI-CSL";
     repo   = "yices2";
     rev    = "Yices-${version}";
-    sha256 = "04vf468spsh00jh7gj94cjnq8kjyfwy9l6r4z7l2pm0zgwkqgyhm";
+    sha256 = "1jx3854zxvfhxrdshbipxfgyq1yxb9ll9agjc2n0cj4vxkjyh9mn";
   };
 
   nativeBuildInputs = [ autoreconfHook ];
-  buildInputs       = [ gmp-static gperf libpoly ];
+  buildInputs = [ cudd gmp-static gperf libpoly ];
   configureFlags =
     [ "--with-static-gmp=${gmp-static.out}/lib/libgmp.a"
       "--with-static-gmp-include-dir=${gmp-static.dev}/include"
@@ -25,12 +26,16 @@ stdenv.mkDerivation rec {
   # Usual shenanigans
   patchPhase = "patchShebangs tests/regress/check.sh";
 
-  # Includes a fix for the embedded soname being libyices.so.2.5, but
-  # only installing the libyices.so.2.5.x file.
+  # Includes a fix for the embedded soname being libyices.so.X.Y, but
+  # only installing the libyices.so.X.Y.Z file.
   installPhase = let
     ver_XdotY = lib.versions.majorMinor version;
   in ''
       make install LDCONFIG=true
+      # guard against packaging of unstable versions: they
+      # have a soname of hext (not current) release.
+      echo "Checking expected library version to be ${version}"
+      [ -f $out/lib/libyices.so.${version} ]
       ln -sfr $out/lib/libyices.so.{${version},${ver_XdotY}}
   '';
 
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix b/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix
index 9b7dabeb7200..2fbaa0a28caf 100644
--- a/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix
+++ b/nixpkgs/pkgs/applications/science/logic/z3/4.4.0.nix
@@ -19,7 +19,7 @@ stdenv.mkDerivation rec {
   # z3's install phase is stupid because it tries to calculate the
   # python package store location itself, meaning it'll attempt to
   # write files into the nix store, and fail.
-  soext = if stdenv.system == "x86_64-darwin" then ".dylib" else ".so";
+  soext = stdenv.hostPlatform.extensions.sharedLibrary;
   installPhase = ''
     mkdir -p $out/bin $out/lib/${python.libPrefix}/site-packages $out/include
     cp ../src/api/z3*.h       $out/include
diff --git a/nixpkgs/pkgs/applications/science/logic/z3/default.nix b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
index e482a071bb43..4153ba5f66fc 100644
--- a/nixpkgs/pkgs/applications/science/logic/z3/default.nix
+++ b/nixpkgs/pkgs/applications/science/logic/z3/default.nix
@@ -19,13 +19,13 @@ with lib;
 
 stdenv.mkDerivation rec {
   pname = "z3";
-  version = "4.8.10";
+  version = "4.8.12";
 
   src = fetchFromGitHub {
     owner = "Z3Prover";
     repo = pname;
     rev = "z3-${version}";
-    sha256 = "1w1ym2l0gipvjx322npw7lhclv8rslq58gnj0d9i96masi3gbycf";
+    sha256 = "1wbcdc7h3mag8infspvxxja2hiz4igjwxzvss2kqar1rjj4ivfx0";
   };
 
   nativeBuildInputs = optional stdenv.hostPlatform.isDarwin fixDarwinDylibNames;