Commit 118a61fa authored by Austin Seipp's avatar Austin Seipp
Browse files

tamarin-prover: 1.6.1 -> 1.8.0 



Signed-off-by: default avatarAustin Seipp <aseipp@pobox.com>
parent a557591d

pkgs/applications/science/logic/tamarin-prover/default.nix

+31 −22
Original line number Diff line number Diff line
@@ -4,12 +4,12 @@ 
}:



let

  version = "1.6.1";

  version = "1.8.0";

  src = fetchFromGitHub {

    owner  = "tamarin-prover";

    repo   = "tamarin-prover";

    rev    = version;

    sha256 = "sha256:0cz1v7k4d0im749ag632nc34n91b51b0pq4z05rzw1p59a5lza92";

    sha256 = "sha256-ujnaUdbjqajmkphOS4Fs4QBCRGX4JZkQ2p1X2jripww=";

  };



  # tamarin has its own dependencies, but they're kept inside the repo,
@@ -51,6 +51,7 @@ let 
    doHaddock = false; # broken

    libraryHaskellDepends = (with haskellPackages; [

      aeson aeson-pretty parallel uniplate

      regex-pcre-builtin regex-posix split

    ]) ++ [ tamarin-prover-utils tamarin-prover-term ];

  });
@@ -62,31 +63,37 @@ let 
    ]) ++ [ tamarin-prover-theory ];

  });



  tamarin-prover-accountability = mkDerivation (common "tamarin-prover-accountability" (src + "/lib/accountability") // {

    postPatch = "cp --remove-destination ${src}/LICENSE .";

    doHaddock = false; # broken

    libraryHaskellDepends = (with haskellPackages; [

      raw-strings-qq

    ]) ++ [

      tamarin-prover-utils

      tamarin-prover-term

      tamarin-prover-theory

    ];

  });



  tamarin-prover-export = mkDerivation (common "tamarin-prover-export" (src + "/lib/export") // {

    postPatch = "cp --remove-destination ${src}/LICENSE .";

    doHaddock = false; # broken

    libraryHaskellDepends = (with haskellPackages; [

      HStringTemplate

    ]) ++ [

      tamarin-prover-utils

      tamarin-prover-term

      tamarin-prover-theory

      tamarin-prover-sapic

    ];

  });



in

mkDerivation (common "tamarin-prover" src // {

  isLibrary = false;

  isExecutable = true;



  patches = [

    # Backport unreleased patch allowing maude 3.2.1

    (fetchpatch {

      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";

    })

  ];

  patches = [ ];



  # strip out unneeded deps manually

  doHaddock = false;
@@ -118,6 +125,8 @@ mkDerivation (common "tamarin-prover" src // { 
    resourcet shakespeare threads wai warp yesod-core yesod-static

  ]) ++ [ tamarin-prover-utils

          tamarin-prover-sapic

          tamarin-prover-accountability

          tamarin-prover-export

          tamarin-prover-term

          tamarin-prover-theory

        ];