pyrox.dev
nixpkgs: add tamarin-prover 1.3.0 (dev) tool
Signed-off-by: Austin Seipp <aseipp@pobox.com>
+84
pkgs/applications/science/logic/tamarin-prover/default.nix
+84
pkgs/applications/science/logic/tamarin-prover/default.nix
···
1
+
{ haskell, haskellPackages, mkDerivation, fetchFromGitHub, lib
2
+
, makeWrapper, maude
3
+
}:
4
+
5
+
let
6
+
version = "1.3.0";
7
+
src = fetchFromGitHub {
8
+
owner = "tamarin-prover";
9
+
repo = "tamarin-prover";
10
+
rev = "8e823691ad3325bce8921617b013735523d74557";
11
+
sha256 = "0rr2syl9xhv17bwky5p39mhn0bypr24h8pld1xidxv87vy7vk7nr";
12
+
};
13
+
14
+
# tamarin has its own dependencies, but they're kept inside the repo,
15
+
# no submodules. this factors out the common metadata among all derivations
16
+
common = pname: src: {
17
+
inherit pname version src;
18
+
19
+
license = lib.licenses.gpl3;
20
+
homepage = https://tamarin-prover.github.io;
21
+
description = "Security protocol verification in the symbolic model";
22
+
maintainers = [ lib.maintainers.thoughtpolice ];
23
+
};
24
+
25
+
# tamarin use symlinks to the LICENSE and Setup.hs files, so for these sublibraries
26
+
# we set the patchPhase to fix that. otherwise, cabal cries a lot.
27
+
replaceSymlinks = ''
28
+
cp --remove-destination ${src}/LICENSE .;
29
+
cp --remove-destination ${src}/Setup.hs .;
30
+
'';
31
+
32
+
tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
33
+
patchPhase = replaceSymlinks;
34
+
libraryHaskellDepends = with haskellPackages; [
35
+
base base64-bytestring binary blaze-builder bytestring containers
36
+
deepseq dlist fclabels mtl pretty safe SHA syb time transformers
37
+
];
38
+
});
39
+
40
+
tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // {
41
+
patchPhase = replaceSymlinks;
42
+
libraryHaskellDepends = (with haskellPackages; [
43
+
attoparsec base binary bytestring containers deepseq dlist HUnit
44
+
mtl process safe
45
+
]) ++ [ tamarin-prover-utils ];
46
+
});
47
+
48
+
tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // {
49
+
patchPhase = replaceSymlinks;
50
+
doHaddock = false; # broken
51
+
libraryHaskellDepends = (with haskellPackages; [
52
+
aeson aeson-pretty base binary bytestring containers deepseq dlist
53
+
fclabels mtl parallel parsec process safe text transformers uniplate
54
+
]) ++ [ tamarin-prover-utils tamarin-prover-term ];
55
+
});
56
+
57
+
in
58
+
mkDerivation (common "tamarin-prover" src // {
59
+
isLibrary = false;
60
+
isExecutable = true;
61
+
62
+
# strip out unneeded deps manually
63
+
doHaddock = false;
64
+
enableSharedExecutables = false;
65
+
postFixup = "rm -rf $out/lib $out/nix-support $out/share/doc";
66
+
67
+
# wrap the prover to be sure it can find maude
68
+
postInstall = ''
69
+
wrapProgram $out/bin/tamarin-prover \
70
+
--prefix PATH : ${lib.makeBinPath [ maude ]}
71
+
'';
72
+
73
+
executableToolDepends = [ makeWrapper ];
74
+
executableHaskellDepends = (with haskellPackages; [
75
+
base binary binary-orphans blaze-builder blaze-html bytestring
76
+
cmdargs conduit containers deepseq directory fclabels file-embed
77
+
filepath gitrev http-types HUnit lifted-base mtl parsec process
78
+
resourcet safe shakespeare tamarin-prover-term
79
+
template-haskell text threads time wai warp yesod-core yesod-static
80
+
]) ++ [ tamarin-prover-utils
81
+
tamarin-prover-term
82
+
tamarin-prover-theory
83
+
];
84
+
})
+3
pkgs/top-level/all-packages.nix
+3
pkgs/top-level/all-packages.nix
···
5967
5967
psc-package = haskell.lib.justStaticExecutables
5968
5968
(haskellPackages.callPackage ../development/compilers/purescript/psc-package { });
5969
5969
5970
+
tamarin-prover = # haskell.lib.justStaticExecutables
5971
+
(haskellPackages.callPackage ../applications/science/logic/tamarin-prover { inherit maude; });
5972
+
5970
5973
inherit (ocamlPackages.haxe) haxe_3_2 haxe_3_4;
5971
5974
haxe = haxe_3_4;
5972
5975
haxePackages = recurseIntoAttrs (callPackage ./haxe-packages.nix { });