tamarin-prover: 1.4.1 → 1.6.0 (#100148)
This commit is contained in:
Vincent Laporte
GitHub
parent
b1a2b39740
commit
33b7529b01
@ -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;
|
||||
})
|
||||
|
||||
@ -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
|
||||
Loading…
Reference in New Issue
Block a user