1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
{ haskellPackages, mkDerivation, fetchFromGitHub, fetchpatch, lib, stdenv
# the following are non-haskell dependencies
, makeWrapper, which, maude, graphviz, glibcLocales
}:
let
version = "1.8.0";
src = fetchFromGitHub {
owner = "tamarin-prover";
repo = "tamarin-prover";
rev = version;
sha256 = "sha256-ujnaUdbjqajmkphOS4Fs4QBCRGX4JZkQ2p1X2jripww=";
};
# tamarin has its own dependencies, but they're kept inside the repo,
# no submodules. this factors out the common metadata among all derivations
common = pname: src: {
inherit pname version src;
license = lib.licenses.gpl3;
homepage = "https://tamarin-prover.github.io";
description = "Security protocol verification in the symbolic model";
maintainers = [ lib.maintainers.thoughtpolice ];
hydraPlatforms = lib.platforms.linux; # maude is broken on darwin
};
# tamarin use symlinks to the LICENSE and Setup.hs files, so for these sublibraries
# we set the patchPhase to fix that. otherwise, cabal cries a lot.
replaceSymlinks = ''
cp --remove-destination ${src}/LICENSE .;
cp --remove-destination ${src}/Setup.hs .;
'';
tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
postPatch = replaceSymlinks;
libraryHaskellDepends = with haskellPackages; [
base64-bytestring blaze-builder
dlist exceptions fclabels safe SHA syb
];
});
tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // {
postPatch = replaceSymlinks;
libraryHaskellDepends = (with haskellPackages; [
attoparsec HUnit
]) ++ [ tamarin-prover-utils ];
});
tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // {
postPatch = replaceSymlinks;
doHaddock = false; # broken
libraryHaskellDepends = (with haskellPackages; [
aeson aeson-pretty parallel uniplate
regex-pcre-builtin regex-posix split
]) ++ [ tamarin-prover-utils tamarin-prover-term ];
});
tamarin-prover-sapic = mkDerivation (common "tamarin-prover-sapic" (src + "/lib/sapic") // {
postPatch = "cp --remove-destination ${src}/LICENSE .";
doHaddock = false; # broken
libraryHaskellDepends = (with haskellPackages; [
raw-strings-qq
]) ++ [ 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 = [ ];
# strip out unneeded deps manually
doHaddock = false;
enableSharedExecutables = false;
postFixup = "rm -rf $out/lib $out/nix-support $out/share/doc";
# wrap the prover to be sure it can find maude, sapic, etc
executableToolDepends = [ makeWrapper which maude graphviz ];
postInstall = ''
wrapProgram $out/bin/tamarin-prover \
'' + lib.optionalString stdenv.isLinux ''
--set LOCALE_ARCHIVE "${glibcLocales}/lib/locale/locale-archive" \
'' + ''
--prefix PATH : ${lib.makeBinPath [ which maude graphviz ]}
# so that the package can be used as a vim plugin to install syntax coloration
install -Dt $out/share/vim-plugins/tamarin-prover/syntax/ etc/syntax/spthy.vim
install etc/filetype.vim -D $out/share/vim-plugins/tamarin-prover/ftdetect/tamarin.vim
mkdir -p $out/share/nvim
ln -s $out/share/vim-plugins/tamarin-prover $out/share/nvim/site
# Emacs SPTHY major mode
install -Dt $out/share/emacs/site-lisp etc/spthy-mode.el
'';
checkPhase = "./dist/build/tamarin-prover/tamarin-prover test";
executableHaskellDepends = (with haskellPackages; [
binary-instances binary-orphans blaze-html conduit file-embed
gitrev http-types lifted-base monad-control
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
];
})
|