diff options
author | Austin Seipp <aseipp@pobox.com> | 2017-12-30 16:12:40 -0600 |
---|---|---|
committer | Austin Seipp <aseipp@pobox.com> | 2017-12-30 18:23:15 -0600 |
commit | abcfa6f608f7265ebe2036d414ae1a1450b8aa71 (patch) | |
tree | 1cb653dc6fd499c57feb7fe1323a94a2251fbe45 /pkgs/applications | |
parent | b81de99c03784cc4e8f93932b948693e5bf204df (diff) | |
download | nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.tar nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.tar.gz nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.tar.bz2 nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.tar.lz nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.tar.xz nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.tar.zst nixlib-abcfa6f608f7265ebe2036d414ae1a1450b8aa71.zip |
nixpkgs: add tamarin-prover 1.3.0 (dev) tool
Signed-off-by: Austin Seipp <aseipp@pobox.com>
Diffstat (limited to 'pkgs/applications')
-rw-r--r-- | pkgs/applications/science/logic/tamarin-prover/default.nix | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix new file mode 100644 index 000000000000..f03751bacf2b --- /dev/null +++ b/pkgs/applications/science/logic/tamarin-prover/default.nix @@ -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 + ]; +}) |