From dd6a74bdbeaecc9bd8faf9a2fc2b78aa70c5af6b Mon Sep 17 00:00:00 2001
From: sternenseemann <sternenseemann@systemli.org>
Date: Wed, 10 May 2023 15:07:36 +0200
Subject: [PATCH] tamarin-prover: allow maude 3.1.1

See https://github.com/tamarin-prover/tamarin-prover/pull/544.

Added tamarin-prover to passthru.tests of maude to prevent future
regressions of this kind.
---
 .../science/logic/tamarin-prover/default.nix  | 19 ++++++++++++++++---
 .../interpreters/maude/default.nix            |  7 +++++++
 2 files changed, 23 insertions(+), 3 deletions(-)

diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix
index 8e883374066d..d5d6512c734a 100644
--- a/pkgs/applications/science/logic/tamarin-prover/default.nix
+++ b/pkgs/applications/science/logic/tamarin-prover/default.nix
@@ -68,10 +68,23 @@ mkDerivation (common "tamarin-prover" src // {
   isExecutable = true;
 
   patches = [
-    # Backport of https://github.com/tamarin-prover/tamarin-prover/pull/536 to 1.6.1
+    # Backport unreleased patch allowing maude 3.2.1
     (fetchpatch {
-      url = "https://github.com/tamarin-prover/tamarin-prover/commit/95fbace0c5cbea57b5f320f6bb4d0387a4beab8d.patch";
-      sha256 = "sha256-Wjf7C208kcskEN1op//HQZnhoZopKQS42JvE8kV5NhI=";
+      name = "tamarin-prover-allow-maude-3.2.1.patch";
+      url = "https://github.com/tamarin-prover/tamarin-prover/commit/bfcf56909479e154a203f0eeefa767f4d91b600d.patch";
+      sha256 = "1zjqzyxwnfp7z3h3li8jrxn9732dx6lyq9q3w2dsphmxbzrs64dg";
+    })
+    # Backport unreleased patch allowing maude 3.2.2
+    (fetchpatch {
+      name = "tamarin-prover-allow-maude-3.2.2.patch";
+      url = "https://github.com/tamarin-prover/tamarin-prover/commit/df1aa9fc4fcc72b6cf0bed0f71844efe3d8ad238.patch";
+      sha256 = "1bkwvyyz5d660jjh08z8wq9c3l40s0rxd2nsbn20xnl2nynyvqpy";
+    })
+    # Backport proposed patch allowing maude 3.3 and 3.3.1
+    (fetchpatch {
+      name = "tamarin-prover-allow-maude-3.3.patch";
+      url = "https://github.com/tamarin-prover/tamarin-prover/pull/544/commits/d0313b1a1bac7c92130773f7ccdd890f8aec286d.patch";
+      sha256 = "1jhlz8vp9a3aahyhj24yjcv4l1389y9kg878yfnq0rkkgvk0m681";
     })
   ];
 
diff --git a/pkgs/development/interpreters/maude/default.nix b/pkgs/development/interpreters/maude/default.nix
index af012d811ed1..7c08b795d6a5 100644
--- a/pkgs/development/interpreters/maude/default.nix
+++ b/pkgs/development/interpreters/maude/default.nix
@@ -1,5 +1,7 @@
 { lib, stdenv, fetchurl, unzip, makeWrapper, flex, bison, ncurses, buddy, tecla
 , libsigsegv, gmpxx, cln, yices
+# passthru.tests
+, tamarin-prover
 }:
 
 let
@@ -46,6 +48,11 @@ stdenv.mkDerivation {
     for n in "$out/bin/"*; do wrapProgram "$n" --suffix MAUDE_LIB ':' "$out/share/maude"; done
   '';
 
+  passthru.tests = {
+    # tamarin-prover only supports specific versions of maude explicitly
+    inherit tamarin-prover;
+  };
+
   enableParallelBuilding = true;
 
   meta = {