Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
nixpkgs: add tamarin-prover 1.3.0 (dev) tool
Signed-off-by: Austin Seipp <aseipp@pobox.com>
- Loading branch information
1 parent
b81de99
commit abcfa6f
Showing
2 changed files
with
87 additions
and
0 deletions.
There are no files selected for viewing
84 changes: 84 additions & 0 deletions
84
pkgs/applications/science/logic/tamarin-prover/default.nix
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,84 @@ | ||
{ haskell, haskellPackages, mkDerivation, fetchFromGitHub, lib | ||
, makeWrapper, maude | ||
}: | ||
|
||
let | ||
version = "1.3.0"; | ||
src = fetchFromGitHub { | ||
owner = "tamarin-prover"; | ||
repo = "tamarin-prover"; | ||
rev = "8e823691ad3325bce8921617b013735523d74557"; | ||
sha256 = "0rr2syl9xhv17bwky5p39mhn0bypr24h8pld1xidxv87vy7vk7nr"; | ||
}; | ||
|
||
# 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 ]; | ||
}; | ||
|
||
# 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") // { | ||
patchPhase = replaceSymlinks; | ||
libraryHaskellDepends = with haskellPackages; [ | ||
base base64-bytestring binary blaze-builder bytestring containers | ||
deepseq dlist fclabels mtl pretty safe SHA syb time transformers | ||
]; | ||
}); | ||
|
||
tamarin-prover-term = mkDerivation (common "tamarin-prover-term" (src + "/lib/term") // { | ||
patchPhase = replaceSymlinks; | ||
libraryHaskellDepends = (with haskellPackages; [ | ||
attoparsec base binary bytestring containers deepseq dlist HUnit | ||
mtl process safe | ||
]) ++ [ tamarin-prover-utils ]; | ||
}); | ||
|
||
tamarin-prover-theory = mkDerivation (common "tamarin-prover-theory" (src + "/lib/theory") // { | ||
patchPhase = replaceSymlinks; | ||
doHaddock = false; # broken | ||
libraryHaskellDepends = (with haskellPackages; [ | ||
aeson aeson-pretty base binary bytestring containers deepseq dlist | ||
fclabels mtl parallel parsec process safe text transformers uniplate | ||
]) ++ [ tamarin-prover-utils tamarin-prover-term ]; | ||
}); | ||
|
||
in | ||
mkDerivation (common "tamarin-prover" src // { | ||
isLibrary = false; | ||
isExecutable = true; | ||
|
||
# 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 | ||
postInstall = '' | ||
wrapProgram $out/bin/tamarin-prover \ | ||
--prefix PATH : ${lib.makeBinPath [ maude ]} | ||
''; | ||
|
||
executableToolDepends = [ makeWrapper ]; | ||
executableHaskellDepends = (with haskellPackages; [ | ||
base binary binary-orphans blaze-builder blaze-html bytestring | ||
cmdargs conduit containers deepseq directory fclabels file-embed | ||
filepath gitrev http-types HUnit lifted-base mtl parsec process | ||
resourcet safe shakespeare tamarin-prover-term | ||
template-haskell text threads time wai warp yesod-core yesod-static | ||
]) ++ [ tamarin-prover-utils | ||
tamarin-prover-term | ||
tamarin-prover-theory | ||
]; | ||
}) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters