diff options
author | Vladimír Čunát <vcunat@gmail.com> | 2017-12-31 09:51:58 +0100 |
---|---|---|
committer | Vladimír Čunát <vcunat@gmail.com> | 2017-12-31 09:53:49 +0100 |
commit | 1fcd92ce923d33ab3d8c0b6c6d42473b135f114b (patch) | |
tree | c0f696c1c2d3ff82067d891ee25bb4f44af54880 /pkgs/applications/science/logic | |
parent | 4d2b7638173afb4c0f0c12a43654bcff5c9500ab (diff) | |
parent | ab3a12ed7ee0de4d247a8017151a1bf01829f6f7 (diff) | |
download | nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.tar nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.tar.gz nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.tar.bz2 nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.tar.lz nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.tar.xz nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.tar.zst nixlib-1fcd92ce923d33ab3d8c0b6c6d42473b135f114b.zip |
Merge branch 'master' into staging
A few thousand rebuilds from master, again. Hydra: ?compare=1422362
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r-- | pkgs/applications/science/logic/sapic/default.nix | 28 | ||||
-rw-r--r-- | pkgs/applications/science/logic/sapic/native.patch | 38 | ||||
-rw-r--r-- | pkgs/applications/science/logic/tamarin-prover/default.nix | 87 |
3 files changed, 153 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/sapic/default.nix b/pkgs/applications/science/logic/sapic/default.nix new file mode 100644 index 000000000000..27efe865a9d9 --- /dev/null +++ b/pkgs/applications/science/logic/sapic/default.nix @@ -0,0 +1,28 @@ +{ stdenv, fetchurl, unzip, ocaml }: + +stdenv.mkDerivation rec { + name = "sapic-${version}"; + version = "0.9"; + + src = fetchurl { + url = "http://sapic.gforge.inria.fr/${name}.zip"; + sha256 = "1ckl090lpyfh90mkjhnpcys5grs3nrl9wlbn9nfkxxnaivn2yx9y"; + }; + + nativeBuildInputs = [ unzip ]; + buildInputs = [ ocaml ]; + patches = [ ./native.patch ]; # create a native binary, not a bytecode one + + buildPhase = "make depend && make"; + installPhase = '' + mkdir -p $out/bin + cp ./sapic $out/bin + ''; + + meta = { + description = "Stateful applied Pi Calculus for protocol verification"; + homepage = http://sapic.gforge.inria.fr/; + platforms = stdenv.lib.platforms.unix; + maintainers = [ stdenv.lib.maintainers.thoughtpolice ]; + }; +} diff --git a/pkgs/applications/science/logic/sapic/native.patch b/pkgs/applications/science/logic/sapic/native.patch new file mode 100644 index 000000000000..6e0b98113df2 --- /dev/null +++ b/pkgs/applications/science/logic/sapic/native.patch @@ -0,0 +1,38 @@ +diff --git a/Makefile b/Makefile +index a1de94d..f9e2eb8 100644 +--- a/Makefile ++++ b/Makefile +@@ -1,8 +1,8 @@ + TARGET = sapic +-OBJS=lexer.cmo apip.cmo firsttranslation.cmo main.cmo #secondtranslation.cmo thirdtranslation.cmo main.cmo ++OBJS=lexer.cmx apip.cmx firsttranslation.cmx main.cmx + + sapic: $(OBJS) +- ocamlc -o $@ $(OBJS) ++ ocamlopt.opt -o $@ $(OBJS) + + depend: + ocamldep *.ml *.mli > .depend +@@ -13,17 +13,17 @@ clean: + rm -rf *.cmi *.cmo $(TARGET) + rm -rf apip.ml apip.mli lexer.ml lexer.mli + +-.SUFFIXES: .ml .mli .mll .mly .cmo .cmi ++.SUFFIXES: .ml .mli .mll .mly .cmo .cmi .cmx + +-.ml.cmo: +- ocamlc -c $< ++.ml.cmx: ++ ocamlopt.opt -c $< + .mli.cmi: +- ocamlc -c $< ++ ocamlopt.opt -c $< + .mll.ml: + ocamllex $< + .mly.ml: + ocamlyacc $< + .ml.mli: +- ocamlc -i $< > $@ ++ ocamlopt.opt -i $< > $@ + + -include .depend 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..bed7eb65e328 --- /dev/null +++ b/pkgs/applications/science/logic/tamarin-prover/default.nix @@ -0,0 +1,87 @@ +{ haskell, haskellPackages, mkDerivation, fetchFromGitHub, lib +# the following are non-haskell dependencies +, makeWrapper, which, maude, graphviz, sapic +}: + +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, sapic, etc + executableToolDepends = [ makeWrapper which maude graphviz sapic ]; + postInstall = '' + wrapProgram $out/bin/tamarin-prover \ + --prefix PATH : ${lib.makeBinPath [ which maude graphviz sapic ]} + ''; + + checkPhase = "./dist/build/tamarin-prover/tamarin-prover test"; + + 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 + ]; +}) |