diff options
Diffstat (limited to 'pkgs/applications/science/logic')
9 files changed, 406 insertions, 3 deletions
diff --git a/pkgs/applications/science/logic/cvc3/default.nix b/pkgs/applications/science/logic/cvc3/default.nix new file mode 100644 index 000000000000..9bb8f8cde4ca --- /dev/null +++ b/pkgs/applications/science/logic/cvc3/default.nix @@ -0,0 +1,54 @@ +x@{builderDefsPackage + , flex, bison, gmp, perl + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + ["gmp"]; + + buildInputs = (map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames))) + ++ [(a.lib.overrideDerivation x.gmp (y: {dontDisableStatic=true;}))]; + sourceInfo = rec { + baseName="cvc3"; + version="2.2"; + name="${baseName}-${version}"; + url="http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${name}.tar.gz"; + hash="1dw12d5vrixfr6l9j6j7026vrr22zb433xyl6n5yxx4hgfywi0ji"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + /* doConfigure should be removed if not needed */ + phaseNames = ["fixPaths" "doConfigure" "doMakeInstall"]; + fixPaths = a.fullDepEntry ('' + sed -e "s@ /bin/bash@bash@g" -i Makefile.std + find . -exec sed -e "s@/usr/bin/perl@${perl}/bin/perl@g" -i '{}' ';' + '') ["minInit" "doUnpack"]; + + meta = { + description = "A prover for satisfiability modulo theory (SMT)"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "free-noncopyleft"; + homepage = "http://www.cs.nyu.edu/acsys/cvc3/index.html"; + }; + passthru = { + updateInfo = { + downloadPage = "http://www.cs.nyu.edu/acsys/cvc3/download.html"; + }; + }; +}) x + diff --git a/pkgs/applications/science/logic/iprover/default.nix b/pkgs/applications/science/logic/iprover/default.nix new file mode 100644 index 000000000000..7bfd8dff12e3 --- /dev/null +++ b/pkgs/applications/science/logic/iprover/default.nix @@ -0,0 +1,58 @@ +x@{builderDefsPackage + , ocaml, eprover + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="iprover"; + version="0.8.1"; + name="${baseName}_v${version}"; + url="${baseName}.googlecode.com/files/${name}.tar.gz"; + hash="15qn523w4l296np5rnkwi50a5x2xqz0kaza7bsh9bkazph7jma7w"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + /* doConfigure should be removed if not needed */ + phaseNames = ["doConfigure" "doMake" "doDeploy"]; + configureCommand = "sh configure"; + doDeploy = a.fullDepEntry ('' + ensureDir "$out/bin" + cp iproveropt "$out/bin" + + ensureDir "$out/share/${name}" + cp *.p "$out/share/${name}" + echo -e "#! /bin/sh\\n$out/bin/iproveropt --clausifier \"${eprover}/bin/eprover\" --clausifier_options \" --tstp-format --silent --cnf \" \"\$@\"" > "$out"/bin/iprover + chmod a+x "$out"/bin/iprover + '') ["defEnsureDir" "minInit" "doMake"]; + + meta = { + description = "An automated first-order logic theorem prover"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "GPLv3"; + }; + passthru = { + updateInfo = { + downloadPage = "http://code.google.com/p/iprover/downloads/list"; + }; + }; +}) x + diff --git a/pkgs/applications/science/logic/isabelle/default.nix b/pkgs/applications/science/logic/isabelle/default.nix index 2471aa8b594c..b9e756e0423b 100644 --- a/pkgs/applications/science/logic/isabelle/default.nix +++ b/pkgs/applications/science/logic/isabelle/default.nix @@ -3,7 +3,7 @@ let pname = "Isabelle"; - version = "2009-1"; + version = "2009-2"; name = "${pname}${version}"; theories = ["HOL" "FOL" "ZF"]; in @@ -13,7 +13,7 @@ stdenv.mkDerivation { src = fetchurl { url = "http://www.cl.cam.ac.uk/research/hvg/${pname}/dist/${name}.tar.gz"; - sha256 = "43ad7794e8b4214b3ace49fc136a69ed6cc65ead02831ae6071f846ecbe56f68"; + sha256 = "f92a275b78bd8844de47a5902e339b58f3b768c07a7fb19d8e606b68499d5ac4"; }; buildInputs = [ perl polyml nettools ]; diff --git a/pkgs/applications/science/logic/isabelle/settings.patch b/pkgs/applications/science/logic/isabelle/settings.patch index 15a70944087b..dc9c611d4886 100644 --- a/pkgs/applications/science/logic/isabelle/settings.patch +++ b/pkgs/applications/science/logic/isabelle/settings.patch @@ -6,7 +6,7 @@ diff -Naur Isabelle2009-1/etc/settings Isabelle2009-1-patched/etc/settings # Poly/ML 5.x (automated settings) -POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")" - ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform") + ML_PLATFORM="$ISABELLE_PLATFORM" -ML_HOME=$(choosefrom \ - "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \ - "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \ diff --git a/pkgs/applications/science/logic/leo2/default.nix b/pkgs/applications/science/logic/leo2/default.nix new file mode 100644 index 000000000000..eb3a13593480 --- /dev/null +++ b/pkgs/applications/science/logic/leo2/default.nix @@ -0,0 +1,62 @@ +x@{builderDefsPackage + , ocaml, eprover + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + ["eprover"]; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="leo2"; + version="1.2.6"; + name="${baseName}_v${version}"; + url="http://www.ags.uni-sb.de/~leo/${name}.tgz"; + hash="0gjgcm6nb9kzdl0y72sgvf2w2q92s1ix70lh6wjz9lj2qdf7gi1z"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + phaseNames = ["makeInstallationDir" "doUnpack" "doMake" "doFinalize"]; + + makeInstallationDir = a.fullDepEntry ('' + ensureDir "$out/share/leo2/build-dir" + cd "$out/share/leo2/build-dir" + '') ["minInit" "defEnsureDir"]; + + goSrcDir = "cd src/"; + + doFinalize = a.fullDepEntry ('' + ensureDir "$out/bin" + echo -e "#! /bin/sh\\n$PWD/../bin/leo --atprc $out/etc/leoatprc \"\$@\"\\n" > "$out/bin/leo" + chmod a+x "$out/bin/leo" + ensureDir "$out/etc" + echo -e "e = ${eprover}/bin/eprover\\nepclextract = ${eprover}/bin/epclextract" > "$out/etc/leoatprc" + '') ["minInit" "doMake" "defEnsureDir"]; + + meta = { + description = "A high-performance typed higher order prover"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "BSD"; + }; + passthru = { + updateInfo = { + downloadPage = "http://www.ags.uni-sb.de/~leo/download.html"; + }; + }; +}) x + diff --git a/pkgs/applications/science/logic/minisat/default.nix b/pkgs/applications/science/logic/minisat/default.nix new file mode 100644 index 000000000000..34a6bd7ceff3 --- /dev/null +++ b/pkgs/applications/science/logic/minisat/default.nix @@ -0,0 +1,57 @@ +x@{builderDefsPackage + , zlib + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="minisat"; + version="2.2.0"; + name="${baseName}-${version}"; + url="http://minisat.se/downloads/${name}.tar.gz"; + hash="023qdnsb6i18yrrawlhckm47q8x0sl7chpvvw3gssfyw3j2pv5cj"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + phaseNames = ["setVars" "doMake" "doDeploy"]; + goSrcDir = "cd simp"; + doDeploy = a.fullDepEntry ('' + ensureDir "$out"/bin + cp minisat_static "$out/bin"/minisat + '') ["minInit" "defEnsureDir"]; + makeFlags = ["rs"]; + setVars = a.fullDepEntry ('' + export MROOT=$PWD/../ + '') ["doUnpack"]; + + meta = { + description = "A compact and readable SAT-solver"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "MIT"; + homepage = "http://minisat.se/"; + }; + passthru = { + updateInfo = { + downloadPage = "http://minisat.se/MiniSat.html"; + }; + }; +}) x + diff --git a/pkgs/applications/science/logic/opensmt/default.nix b/pkgs/applications/science/logic/opensmt/default.nix new file mode 100644 index 000000000000..165c8a2f1484 --- /dev/null +++ b/pkgs/applications/science/logic/opensmt/default.nix @@ -0,0 +1,51 @@ +x@{builderDefsPackage + , automake, libtool, autoconf, intltool, perl + , gmpxx, flex, bison + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="opensmt"; + version="20101017"; + name="${baseName}-${version}"; + filename="${baseName}_src_${version}"; + url="${baseName}.googlecode.com/files/${filename}.tgz"; + hash="0xrky7ixjaby5x026v7hn72xh7d401w9jhccxjn0khhn1x87p2w1"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + /* doConfigure should be removed if not needed */ + phaseNames = ["doAutotools" "doConfigure" "doMakeInstall"]; + + meta = { + description = "A satisfiability modulo theory (SMT) solver"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "GPLv3"; + homepage = "http://code.google.com/p/opensmt/"; + }; + passthru = { + updateInfo = { + downloadPage = "http://code.google.com/p/opensmt/downloads/list"; + }; + }; +}) x + diff --git a/pkgs/applications/science/logic/satallax/default.nix b/pkgs/applications/science/logic/satallax/default.nix new file mode 100644 index 000000000000..4bf6e53737e9 --- /dev/null +++ b/pkgs/applications/science/logic/satallax/default.nix @@ -0,0 +1,72 @@ +x@{builderDefsPackage + , sbcl, zlib + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="satallax"; + version="1.4"; + name="${baseName}-${version}"; + url="http://www.ps.uni-saarland.de/~cebrown/satallax/downloads/${name}.tar.gz"; + hash="0l8dq4nyfw2bdsyqmgb4v6fjw3739p8nqv4bh2gh2924ibzrq5fc"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + phaseNames = ["doDeployMinisat" "doDeploy"]; + + doDeployMinisat = a.fullDepEntry ('' + ( + cd minisat/simp + make + ) + + ensureDir "$out/bin" + cp minisat/simp/minisat "$out/bin" + + echo "(setq *minisat-binary* \"$out/bin/minisat\")" > config.lisp + + '') ["defEnsureDir" "minInit" "addInputs" "doUnpack"]; + doDeploy = a.fullDepEntry ('' + ensureDir "$out/share/satallax/build-dir" + cp -r * "$out/share/satallax/build-dir" + cd "$out/share/satallax/build-dir" + + sbcl --load make.lisp + ! ( ./test | grep ERROR ) + + ensureDir "$out/bin" + cp bin/satallax "$out/bin" + '') ["defEnsureDir" "minInit" "addInputs" "doUnpack"]; + + meta = { + description = "A higher-order logic prover"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + unix; + license = "free-noncopyleft"; + homepage = "http://www.ps.uni-saarland.de/~cebrown/satallax/"; + }; + passthru = { + updateInfo = { + downloadPage = "http://www.ps.uni-saarland.de/~cebrown/satallax/"; + }; + }; +}) x + diff --git a/pkgs/applications/science/logic/spass/default.nix b/pkgs/applications/science/logic/spass/default.nix new file mode 100644 index 000000000000..2c6144baf0e8 --- /dev/null +++ b/pkgs/applications/science/logic/spass/default.nix @@ -0,0 +1,49 @@ +x@{builderDefsPackage + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="spass"; + baseVersion="3"; + minorVersion="7"; + version="${baseVersion}.${minorVersion}"; + name="${baseName}-${version}"; + url="http://www.spass-prover.org/download/sources/${baseName}${baseVersion}${minorVersion}.tgz"; + hash="1k5a98kr3vzga54zs7slwwaaf6v6agk1yfcayd8bl55q15g7xihk"; + }; +in +rec { + src = a.fetchurl { + url = sourceInfo.url; + sha256 = sourceInfo.hash; + }; + + inherit (sourceInfo) name version; + inherit buildInputs; + + /* doConfigure should be removed if not needed */ + phaseNames = ["doConfigure" "doMakeInstall"]; + + meta = { + description = "An automated theorem preover for FOL"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "BSD"; + }; + passthru = { + updateInfo = { + downloadPage = "http://www.spass-prover.org/download/index.html"; + }; + }; +}) x + |