diff options
author | Frederik Rietdijk <fridh@fridh.nl> | 2020-10-13 19:34:34 +0200 |
---|---|---|
committer | Frederik Rietdijk <fridh@fridh.nl> | 2020-10-13 19:34:34 +0200 |
commit | 9e1943edc03c14854295d47001c2b46d7d2472de (patch) | |
tree | 3a7b08aa961782c4a8e77837e6532502c891bc5d /pkgs/applications/science/logic | |
parent | aabcf2d8f52c68ad37d72bf80d90608831450af5 (diff) | |
parent | c5a41da563485db7e34475321e22d45941de23d0 (diff) |
Merge master into staging-next
Diffstat (limited to 'pkgs/applications/science/logic')
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 ]; + }; +} |