From 40b17486d6b48430ba3509fc98e0fb7584dfad1b Mon Sep 17 00:00:00 2001 From: kyehn Date: Sun, 24 Aug 2025 16:32:58 +0800 Subject: [PATCH 1/3] yices: 2.6.5 -> 2.7.0 --- pkgs/by-name/yi/yices/package.nix | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/pkgs/by-name/yi/yices/package.nix b/pkgs/by-name/yi/yices/package.nix index d47da8915619..729d88f294d3 100644 --- a/pkgs/by-name/yi/yices/package.nix +++ b/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,6 +49,8 @@ stdenv.mkDerivation rec { enableParallelBuilding = true; doCheck = true; + nativeCheckInputs = [ ncurses5 ]; + meta = with lib; { description = "High-performance theorem prover and SMT solver"; homepage = "https://yices.csl.sri.com"; @@ -48,4 +58,4 @@ stdenv.mkDerivation rec { platforms = with platforms; linux ++ darwin; maintainers = with maintainers; [ thoughtpolice ]; }; -} +}) From 7a241300bc5522916ffcbca18e25c2dd029d946c Mon Sep 17 00:00:00 2001 From: kyehn Date: Sun, 24 Aug 2025 16:33:05 +0800 Subject: [PATCH 2/3] yices: remove with lib --- pkgs/by-name/yi/yices/package.nix | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pkgs/by-name/yi/yices/package.nix b/pkgs/by-name/yi/yices/package.nix index 729d88f294d3..0104fea519ed 100644 --- a/pkgs/by-name/yi/yices/package.nix +++ b/pkgs/by-name/yi/yices/package.nix @@ -51,11 +51,11 @@ stdenv.mkDerivation (finalAttrs: { nativeCheckInputs = [ ncurses5 ]; - meta = with lib; { + 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 ]; }; }) From b678ce47d79ce010304ad8de932954370af48a7b Mon Sep 17 00:00:00 2001 From: kyehn Date: Mon, 25 Aug 2025 13:44:35 +0800 Subject: [PATCH 3/3] maude: 3.4 -> 3.5 --- pkgs/by-name/ma/maude/package.nix | 81 ++++++++++++++++--------------- 1 file changed, 42 insertions(+), 39 deletions(-) diff --git a/pkgs/by-name/ma/maude/package.nix b/pkgs/by-name/ma/maude/package.nix index deea3053d2cf..9b7f61d52c81 100644 --- a/pkgs/by-name/ma/maude/package.nix +++ b/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 ]; }; -} +})