diff options
Diffstat (limited to 'pkgs/applications/science')
12 files changed, 518 insertions, 4 deletions
diff --git a/pkgs/applications/science/electronics/verilog/default.nix b/pkgs/applications/science/electronics/verilog/default.nix index 8f48879f76a3..a4c803e2952c 100644 --- a/pkgs/applications/science/electronics/verilog/default.nix +++ b/pkgs/applications/science/electronics/verilog/default.nix @@ -4,7 +4,7 @@ stdenv.mkDerivation rec { name = "verilog-0.9.3"; src = fetchurl { - url = "mirror://sourceforce/${name}.tar.gz"; + url = "mirror://sourceforge/iverilog/${name}.tar.gz"; sha256 = "dd68c8ab874a93805d1e93fa76ee1e91fc0c7b20822ded3e57b6536cd8c0d1ba"; }; 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 + diff --git a/pkgs/applications/science/math/pari/default.nix b/pkgs/applications/science/math/pari/default.nix new file mode 100644 index 000000000000..62763ac2198a --- /dev/null +++ b/pkgs/applications/science/math/pari/default.nix @@ -0,0 +1,50 @@ +x@{builderDefsPackage + , perl, zlib, gmp, readline + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="pari"; + version="2.3.5"; + name="${baseName}-${version}"; + url="http://pari.math.u-bordeaux.fr/pub/pari/unix/${name}.tar.gz"; + hash="124xr2jdz2c15v45i1zvgylng44lhf23729a1mk7ci1vywdaxpa7"; + }; +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"]; + configureCommand="./Configure"; + + meta = { + description = "Computer algebra system for high-performance number theory computations"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "GPLv2+"; + homepage = "http://pari.math.u-bordeaux.fr/"; + }; + passthru = { + updateInfo = { + downloadPage = "http://pari.math.u-bordeaux.fr/download.html"; + }; + }; +}) x + diff --git a/pkgs/applications/science/math/singular/default.nix b/pkgs/applications/science/math/singular/default.nix new file mode 100644 index 000000000000..dfc97eca8ebe --- /dev/null +++ b/pkgs/applications/science/math/singular/default.nix @@ -0,0 +1,61 @@ +x@{builderDefsPackage + , gmp, bison, perl, autoconf, ncurses, readline + , coreutils + , ...}: +builderDefsPackage +(a : +let + helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ + []; + + buildInputs = map (n: builtins.getAttr n x) + (builtins.attrNames (builtins.removeAttrs x helperArgNames)); + sourceInfo = rec { + baseName="Singular"; + version="3-1-2"; + revision="-1"; + name="${baseName}-${version}${revision}"; + url="http://www.mathematik.uni-kl.de/ftp/pub/Math/Singular/SOURCES/${version}/${name}.tar.gz"; + hash="04f9i1xar0r7qrrbfki1h9rrmx5y2xg4w7rrvlbx05v2dy6s8djv"; + }; +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 = ["doFixPaths" "doConfigure" "doMakeInstall" "fixInstall"]; + doFixPaths = a.fullDepEntry ('' + find . -exec sed -e 's@/bin/rm@${a.coreutils}&@g' -i '{}' ';' + find . -exec sed -e 's@/bin/uname@${a.coreutils}&@g' -i '{}' ';' + '') ["minInit" "doUnpack"]; + fixInstall = a.fullDepEntry ('' + rm -rf "$out/LIB" + cp -r Singular/LIB "$out" + ensureDir "$out/bin" + ln -s "$out"/*/Singular "$out/bin" + '') ["minInit" "defEnsureDir"]; + + meta = { + description = "A CAS for polynomial computations"; + maintainers = with a.lib.maintainers; + [ + raskin + ]; + platforms = with a.lib.platforms; + linux; + license = "GPLv3"; # Or GPLv2 at your option - but not GPLv4 + homepage = "http://www.singular.uni-kl.de/index.php"; + }; + passthru = { + updateInfo = { + downloadPage = "http://www.mathematik.uni-kl.de/ftp/pub/Math/Singular/SOURCES/"; + }; + }; +}) x + |