From 33b7529b01709e54f34c61b9416ae2543d3e8020 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 13 Oct 2020 10:16:11 +0200 Subject: [PATCH] =?UTF-8?q?tamarin-prover:=201.4.1=20=E2=86=92=201.6.0=20(?= =?UTF-8?q?#100148)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../science/logic/tamarin-prover/default.nix | 56 +++++--------- .../logic/tamarin-prover/sapic-native.patch | 77 ------------------- 2 files changed, 21 insertions(+), 112 deletions(-) delete mode 100644 pkgs/applications/science/logic/tamarin-prover/sapic-native.patch 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