tamarin-prover: 1.4.1 → 1.6.0 (#100148)

2 files changed, 21 insertions, 112 deletions

diff --git a/pkgs/applications/science/logic/tamarin-prover/default.nix b/pkgs/applications/science/logic/tamarin-prover/default.nix
index 857aba5a260..d217e2b9b50 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 6ab7e4e7594..00000000000
--- 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