yices: 2.6.5 -> 2.7.0 (#436408)

pkgs/by-name/ma/maude/package.nix

@@ -1,48 +1,52 @@
 {
   lib,
   stdenv,
-  fetchurl,
-  unzip,
-  makeWrapper,
-  flex,
+  fetchFromGitHub,
+  autoreconfHook,
   bison,
-  ncurses,
+  flex,
+  makeWrapper,
   buddy,
-  tecla,
-  libsigsegv,
-  gmpxx,
   cln,
+  cvc4,
+  gmpxx,
+  libsigsegv,
+  tecla,
   yices,
   # passthru.tests
   tamarin-prover,
 }:
 
-let
-  version = "3.4";
-in
-
-stdenv.mkDerivation {
+stdenv.mkDerivation (finalAttrs: {
   pname = "maude";
-  inherit version;
+  version = "3.5";
 
-  src = fetchurl {
-    url = "https://github.com/maude-lang/Maude/archive/refs/tags/Maude${version}.tar.gz";
-    sha256 = "IXWEWAmh388NpNSt9wnOpLkzhZ09N+AStO2wn5dRT8o=";
+  src = fetchFromGitHub {
+    owner = "maude-lang";
+    repo = "Maude";
+    tag = "Maude${finalAttrs.version}";
+    hash = "sha256-1no5K3+0N4MCg2Nr+9FgwWH6G9Inwh2MIYuA/auZhys=";
   };
 
+  # Always enabled in CVC4 1.8: https://github.com/CVC4/CVC4/pull/4519
+  postPatch = ''
+    sed -i '/rewrite-divk/d' src/Mixfix/cvc4_Bindings.cc
+  '';
+
   nativeBuildInputs = [
-    flex
+    autoreconfHook
     bison
-    unzip
+    flex
     makeWrapper
   ];
+
   buildInputs = [
-    ncurses
     buddy
-    tecla
+    cln
+    cvc4
     gmpxx
     libsigsegv
-    cln
+    tecla
     yices
   ];
 
@@ -54,23 +58,24 @@ stdenv.mkDerivation {
     "fortify"
   ];
 
-  # Fix for glibc-2.34, see
-  # https://gitweb.gentoo.org/repo/gentoo.git/commit/dev-lang/maude/maude-3.1-r1.ebuild?id=f021cc6cfa1e35eb9c59955830f1fd89bfcb26b4
-  configureFlags = [ "--without-libsigsegv" ];
+  __darwinAllowLocalNetworking = true;
 
-  # Certain tests (in particular, Misc/fileTest) expect us to build in a subdirectory
-  # We'll use the directory Opt/ as suggested in INSTALL
-  preConfigure = ''
-    mkdir Opt; cd Opt
-    configureFlagsArray=(
-      --datadir="$out/share/maude"
-      TECLA_LIBS="-ltecla -lncursesw"
-      LIBS="-lcln"
-      CFLAGS="-O3" CXXFLAGS="-O3"
-    )
-  '';
   configureScript = "../configure";
 
+  configureFlags = [
+    "--with-cvc4=yes"
+    "--with-yices2=yes"
+    "--prefix=${placeholder "out"}"
+    "--datadir=${placeholder "out"}/share/maude"
+  ];
+
+  makeFlags = [ "CVC4_LIB=-lcvc4 -lcln" ];
+
+  preConfigure = ''
+    mkdir -p build
+    cd build
+  '';
+
   doCheck = true;
 
   postInstall = ''
@@ -89,7 +94,6 @@ stdenv.mkDerivation {
     description = "High-level specification language";
     mainProgram = "maude";
     license = lib.licenses.gpl2Plus;
-
     longDescription = ''
       Maude is a high-performance reflective language and system
       supporting both equational and rewriting logic specification and
@@ -99,8 +103,7 @@ stdenv.mkDerivation {
       equational specification and programming, Maude also supports
       rewriting logic computation.
     '';
-
     platforms = lib.platforms.unix;
     maintainers = [ lib.maintainers.peti ];
   };
-}
+})

pkgs/by-name/yi/yices/package.nix

@@ -7,23 +7,31 @@
   gperf,
   autoreconfHook,
   libpoly,
+  ncurses5,
 }:
 
 let
   gmp-static = gmp.override { withStatic = true; };
 in
-stdenv.mkDerivation rec {
+stdenv.mkDerivation (finalAttrs: {
   pname = "yices";
-  version = "2.6.5";
+  version = "2.7.0";
 
   src = fetchFromGitHub {
     owner = "SRI-CSL";
     repo = "yices2";
-    rev = "Yices-${version}";
-    hash = "sha256-/sKyHkFW5I5kojNIRPEKojzTvfRZiyVIN5VlBIbAV7k=";
+    tag = "yices-${finalAttrs.version}";
+    hash = "sha256-siyepgxqKWRyO4+SB95lmhJ98iDubk0R0ErEJdSsM8o=";
   };
 
-  postPatch = "patchShebangs tests/regress/check.sh";
+  postPatch = ''
+    patchShebangs tests/regress/check.sh
+  ''
+  # operation not permitted
+  + lib.optionalString stdenv.hostPlatform.isDarwin ''
+    substituteInPlace utils/make_source_version \
+      --replace-fail '"/usr/bin/mktemp -t out"' "mktemp"
+  '';
 
   nativeBuildInputs = [ autoreconfHook ];
   buildInputs = [
@@ -41,11 +49,13 @@ stdenv.mkDerivation rec {
   enableParallelBuilding = true;
   doCheck = true;
 
-  meta = with lib; {
+  nativeCheckInputs = [ ncurses5 ];
+
+  meta = {
     description = "High-performance theorem prover and SMT solver";
     homepage = "https://yices.csl.sri.com";
-    license = licenses.gpl3;
-    platforms = with platforms; linux ++ darwin;
-    maintainers = with maintainers; [ thoughtpolice ];
+    license = lib.licenses.gpl3Plus;
+    platforms = lib.platforms.linux ++ lib.platforms.darwin;
+    maintainers = with lib.maintainers; [ thoughtpolice ];
   };
-}
+})