Merge master into staging-next

3 files changed, 62 insertions, 112 deletions

diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix
index 857aba5a2607..d217e2b9b505 100644
--- a/pkgs/applications/science/logic/tamarin-prover/default.nix
+++ b/pkgs/applications/science/logic/tamarin-prover/default.nix
@@ -1,15 +1,15 @@
 { haskellPackages, mkDerivation, fetchFromGitHub, lib
 # the following are non-haskell dependencies
-, makeWrapper, which, maude, graphviz, ocaml
+, makeWrapper, which, maude, graphviz
 }:
 
 let
-  version = "1.4.1";
+  version = "1.6.0";
   src = fetchFromGitHub {
     owner  = "tamarin-prover";
     repo   = "tamarin-prover";
-    rev    = "d2e1c57311ce4ed0ef46d0372c4995b8fdc25323";
-    sha256 = "1bf2qvb646jg3qxd6jgp9ja3wlr888wchxi9mfr3kg7hfn63vxbq";
+    rev    = version;
+    sha256 = "1pl3kz7gyw9g6s4x5j90z4snd10vq6296g3ajlr8d4n53p3c9i3w";
   };
 
   # tamarin has its own dependencies, but they're kept inside the repo,
@@ -33,16 +33,15 @@ let
   tamarin-prover-utils = mkDerivation (common "tamarin-prover-utils" (src + "/lib/utils") // {
     postPatch = replaceSymlinks;
     libraryHaskellDepends = with haskellPackages; [
-      base base64-bytestring binary blaze-builder bytestring containers
-      deepseq dlist fclabels mtl pretty safe SHA syb time transformers
+      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 base binary bytestring containers deepseq dlist HUnit
-      mtl process safe
+      attoparsec HUnit
     ]) ++ [ tamarin-prover-utils ];
   });
 
@@ -50,11 +49,18 @@ let
     postPatch = 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
+      aeson aeson-pretty parallel uniplate
     ]) ++ [ 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 ];
+  });
+
 in
 mkDerivation (common "tamarin-prover" src // {
   isLibrary = false;
@@ -65,45 +71,25 @@ mkDerivation (common "tamarin-prover" src // {
   enableSharedExecutables = false;
   postFixup = "rm -rf $out/lib $out/nix-support $out/share/doc";
 
-  # Fix problem with MonadBaseControl not being found
-  patchPhase = ''
-    sed -ie 's,\(import *\)Control\.Monad$,&\
-    \1Control.Monad.Trans.Control,' src/Web/Handler.hs
-
-    sed -ie 's~\( *, \)mtl~&\
-    \1monad-control~' tamarin-prover.cabal
-
-    patch -p1 < ${./sapic-native.patch}
-  '';
-
-  postBuild = ''
-    cd plugins/sapic && make sapic && cd ../..
-  '';
-
   # wrap the prover to be sure it can find maude, sapic, etc
   executableToolDepends = [ makeWrapper which maude graphviz ];
   postInstall = ''
     wrapProgram $out/bin/tamarin-prover \
       --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/{spthy,sapic}.vim
+    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
-    install -m0755 ./plugins/sapic/sapic $out/bin/sapic
   '';
 
   checkPhase = "./dist/build/tamarin-prover/tamarin-prover test";
 
-  executableSystemDepends = [ ocaml ];
   executableHaskellDepends = (with haskellPackages; [
-    base binary binary-orphans blaze-builder blaze-html bytestring
-    cmdargs conduit containers monad-control deepseq directory fclabels file-embed
-    filepath gitrev http-types HUnit lifted-base mtl monad-unlift parsec process
-    resourcet safe shakespeare tamarin-prover-term
-    template-haskell text threads time wai warp yesod-core yesod-static
+    binary-instances binary-orphans blaze-html conduit file-embed
+    gitrev http-types lifted-base monad-control monad-unlift
+    resourcet shakespeare threads wai warp yesod-core yesod-static
   ]) ++ [ tamarin-prover-utils
+          tamarin-prover-sapic
           tamarin-prover-term
           tamarin-prover-theory
         ];
-
-  broken = true;
 })
diff --git a/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch b/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch
deleted file mode 100644
index 6ab7e4e7594f..000000000000
--- a/pkgs/applications/science/logic/tamarin-prover/sapic-native.patch
+++ /dev/null
@@ -1,77 +0,0 @@
-diff --git a/plugins/sapic/Makefile b/plugins/sapic/Makefile
-index 8f1b1866..678accbe 100644
---- a/plugins/sapic/Makefile
-+++ b/plugins/sapic/Makefile
-@@ -1,18 +1,18 @@
- TARGET = sapic
--OBJS= color.cmo exceptions.cmo btree.cmo position.cmo positionplusinit.cmo var.cmo term.cmo fact.cmo atomformulaaction.cmo action.cmo atom.cmo formula.cmo tamarin.cmo sapicterm.cmo sapicvar.cmo sapicaction.cmo lexer.cmo  sapic.cmo annotatedsapicaction.cmo annotatedsapictree.cmo progressfunction.cmo restrictions.cmo annotatedrule.cmo translationhelper.cmo basetranslation.cmo firsttranslation.cmo main.cmo 
-+OBJS= color.cmx exceptions.cmx btree.cmx position.cmx positionplusinit.cmx var.cmx term.cmx fact.cmx atomformulaaction.cmx action.cmx atom.cmx formula.cmx tamarin.cmx sapicterm.cmx sapicvar.cmx sapicaction.cmx lexer.cmx  sapic.cmx annotatedsapicaction.cmx annotatedsapictree.cmx progressfunction.cmx restrictions.cmx annotatedrule.cmx translationhelper.cmx basetranslation.cmx firsttranslation.cmx main.cmx
- FLAGS=-g
- 
--OCAMLC    := $(shell command -v ocamlc    2> /dev/null)
-+OCAMLOPT  := $(shell command -v ocamlopt  2> /dev/null)
- OCAMLLEX  := $(shell command -v ocamllex  2> /dev/null)
- OCAMLYACC := $(shell command -v ocamlyacc 2> /dev/null)
- OCAMLDEP  := $(shell command -v ocamldep  2> /dev/null)
--OCAMLC_GTEQ_402 := $(shell expr `ocamlc -version | sed -e 's/\.\([0-9][0-9]\)/\1/g' -e 's/\.\([0-9]\)/0\1/g' -e 's/^[0-9]\{3,4\}$$/&00/'` \>= 40200)
-+OCAMLC_GTEQ_402 := $(shell expr `ocamlopt -version | sed -e 's/\.\([0-9][0-9]\)/\1/g' -e 's/\.\([0-9]\)/0\1/g' -e 's/^[0-9]\{3,4\}$$/&00/'` \>= 40200)
- 
- default: sapic
- 
- sapic:
--ifdef OCAMLC
--	@echo "Found ocamlc."
-+ifdef OCAMLOPT
-+	@echo "Found ocamlopt."
- ifdef OCAMLLEX
- 	@echo "Found ocamllex."
- ifdef OCAMLYACC
-@@ -22,9 +22,9 @@ ifdef OCAMLDEP
- ifeq "$(OCAMLC_GTEQ_402)" "1"
- 	@echo "Building SAPIC."
- 	$(MAKE) $(OBJS)
--	ocamlc $(FLAGS) -o $@ str.cma $(OBJS)
--	@echo "Installing SAPIC into ~/.local/bin/"
--	cp sapic ~/.local/bin
-+	ocamlopt $(FLAGS) -o $@ str.cmxa $(OBJS)
-+#	@echo "Installing SAPIC into ~/.local/bin/"
-+#	cp sapic ~/.local/bin
- else
- 	@echo "Found OCAML version < 4.02. SAPIC will not be installed."
- endif
-@@ -38,7 +38,7 @@ else
- 	@echo "ocamllex not found. SAPIC will not be installed."
- endif
- else
--	@echo "ocamlc not found. SAPIC will not be installed."
-+	@echo "ocamlopt not found. SAPIC will not be installed."
- endif
- 
- depend:
-@@ -48,20 +48,20 @@ lexer.ml: sapic.cmi
- 
- .PHONY: clean
- clean:
--	rm -rf *.cmi *.cmo $(TARGET)
-+	rm -rf *.cmi **.cmx $(TARGET)
- 	rm -rf sapic.ml sapic.mli lexer.ml lexer.mli
- 
--.SUFFIXES: .ml .mli .mll .mly .cmo .cmi
-+.SUFFIXES: .ml .mli .mll .mly .cmx .cmi
- 
--.ml.cmo:
--	ocamlc $(FLAGS) -c $<
-+.ml.cmx:
-+	ocamlopt $(FLAGS) -c $<
- .mli.cmi:
--	ocamlc $(FLAGS) -c $<
-+	ocamlopt $(FLAGS) -c $<
- .mll.ml:
- 	ocamllex $<
- .mly.ml:
- 	ocamlyacc $<
- .ml.mli:
--	ocamlc -i $< > $@
-+	ocamlopt -i $< > $@
- 
- -include .depend
diff --git a/pkgs/applications/science/logic/z3/4.4.0.nix b/pkgs/applications/science/logic/z3/4.4.0.nix
new file mode 100644
index 000000000000..1e3bcea42ef7
--- /dev/null
+++ b/pkgs/applications/science/logic/z3/4.4.0.nix
@@ -0,0 +1,41 @@
+{ stdenv, fetchFromGitHub, python }:
+
+stdenv.mkDerivation rec {
+  name = "z3-${version}";
+  version = "4.4.0";
+
+  src = fetchFromGitHub {
+    owner  = "Z3Prover";
+    repo   = "z3";
+    rev    = "7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152";
+    sha256 = "1xllvq9fcj4cz34biq2a9dn2sj33bdgrzyzkj26hqw70wkzv1kzx";
+  };
+
+  buildInputs = [ python ];
+  enableParallelBuilding = true;
+
+  configurePhase = "python scripts/mk_make.py --prefix=$out && cd build";
+
+  # z3's install phase is stupid because it tries to calculate the
+  # python package store location itself, meaning it'll attempt to
+  # write files into the nix store, and fail.
+  soext = if stdenv.system == "x86_64-darwin" then ".dylib" else ".so";
+  installPhase = ''
+    mkdir -p $out/bin $out/lib/${python.libPrefix}/site-packages $out/include
+    cp ../src/api/z3*.h       $out/include
+    cp ../src/api/c++/z3*.h   $out/include
+    cp z3                     $out/bin
+    cp libz3${soext}          $out/lib
+    cp libz3${soext}          $out/lib/${python.libPrefix}/site-packages
+    cp z3*.pyc                $out/lib/${python.libPrefix}/site-packages
+    cp ../src/api/python/*.py $out/lib/${python.libPrefix}/site-packages
+  '';
+
+  meta = {
+    description = "A high-performance theorem prover and SMT solver";
+    homepage    = "http://github.com/Z3Prover/z3";
+    license     = stdenv.lib.licenses.mit;
+    platforms   = stdenv.lib.platforms.x86_64;
+    maintainers = with stdenv.lib.maintainers; [ thoughtpolice ttuegel ];
+  };
+}