summary refs log tree commit diff
path: root/pkgs/applications/science
diff options
context:
space:
mode:
Diffstat (limited to 'pkgs/applications/science')
-rw-r--r--pkgs/applications/science/astronomy/celestia/default.nix2
-rw-r--r--pkgs/applications/science/astronomy/gravit/default.nix2
-rw-r--r--pkgs/applications/science/astronomy/stellarium/default.nix11
-rw-r--r--pkgs/applications/science/astronomy/xplanet/default.nix6
-rw-r--r--pkgs/applications/science/astronomy/xplanet/giflib.patch130
-rw-r--r--pkgs/applications/science/biology/arb/default.nix1
-rw-r--r--pkgs/applications/science/biology/plink/default.nix3
-rw-r--r--pkgs/applications/science/chemistry/avogadro/default.nix8
-rw-r--r--pkgs/applications/science/electronics/archimedes/default.nix6
-rw-r--r--pkgs/applications/science/electronics/caneda/default.nix2
-rw-r--r--pkgs/applications/science/electronics/gtkwave/default.nix6
-rw-r--r--pkgs/applications/science/electronics/kicad/default.nix24
-rw-r--r--pkgs/applications/science/electronics/ngspice/default.nix6
-rw-r--r--pkgs/applications/science/electronics/pulseview/default.nix24
-rw-r--r--pkgs/applications/science/electronics/qfsm/default.nix3
-rw-r--r--pkgs/applications/science/electronics/qucs/default.nix2
-rw-r--r--pkgs/applications/science/electronics/tkgate/1.x.nix18
-rw-r--r--pkgs/applications/science/electronics/tkgate/2.x.nix17
-rw-r--r--pkgs/applications/science/electronics/verilog/default.nix7
-rw-r--r--pkgs/applications/science/electronics/xoscope/default.nix2
-rw-r--r--pkgs/applications/science/geometry/tetgen/default.nix8
-rw-r--r--pkgs/applications/science/logic/abc/default.nix27
-rw-r--r--pkgs/applications/science/logic/alt-ergo/default.nix23
-rw-r--r--pkgs/applications/science/logic/boolector/default.nix47
-rw-r--r--pkgs/applications/science/logic/coq/HEAD.nix57
-rw-r--r--pkgs/applications/science/logic/coq/default.nix8
-rw-r--r--pkgs/applications/science/logic/cvc3/default.nix4
-rw-r--r--pkgs/applications/science/logic/ekrhyper/default.nix8
-rw-r--r--pkgs/applications/science/logic/hol/default.nix4
-rw-r--r--pkgs/applications/science/logic/hol_light/default.nix28
-rw-r--r--pkgs/applications/science/logic/iprover/default.nix12
-rw-r--r--pkgs/applications/science/logic/leo2/default.nix22
-rw-r--r--pkgs/applications/science/logic/leo2/default.upstream6
-rw-r--r--pkgs/applications/science/logic/logisim/default.nix2
-rw-r--r--pkgs/applications/science/logic/ltl2ba/default.nix24
-rw-r--r--pkgs/applications/science/logic/matita/130312.nix2
-rw-r--r--pkgs/applications/science/logic/matita/default.nix2
-rw-r--r--pkgs/applications/science/logic/minisat/default.nix11
-rw-r--r--pkgs/applications/science/logic/opensmt/default.nix20
-rw-r--r--pkgs/applications/science/logic/picosat/default.nix2
-rw-r--r--pkgs/applications/science/logic/prooftree/default.nix40
-rw-r--r--pkgs/applications/science/logic/ssreflect/default.nix6
-rw-r--r--pkgs/applications/science/logic/stp/default.nix23
-rw-r--r--pkgs/applications/science/logic/stp/fixbuild.diff45
-rw-r--r--pkgs/applications/science/logic/stp/fixrefs.diff192
-rw-r--r--pkgs/applications/science/logic/tptp/default.nix15
-rw-r--r--pkgs/applications/science/logic/twelf/default.nix46
-rw-r--r--pkgs/applications/science/logic/verifast/default.nix43
-rw-r--r--pkgs/applications/science/logic/why3/default.nix22
-rw-r--r--pkgs/applications/science/logic/yices/default.nix40
-rw-r--r--pkgs/applications/science/logic/z3/default.nix46
-rw-r--r--pkgs/applications/science/math/R/default.nix9
-rw-r--r--pkgs/applications/science/math/content/default.nix1
-rw-r--r--pkgs/applications/science/math/eukleides/default.nix2
-rw-r--r--pkgs/applications/science/math/fricas/default.nix23
-rw-r--r--pkgs/applications/science/math/gap/default.nix22
-rw-r--r--pkgs/applications/science/math/glsurf/default.nix2
-rw-r--r--pkgs/applications/science/math/jags/default.nix4
-rw-r--r--pkgs/applications/science/math/mathematica/default.nix6
-rw-r--r--pkgs/applications/science/math/maxima/default.nix6
-rw-r--r--pkgs/applications/science/math/pari/default.nix4
-rw-r--r--pkgs/applications/science/math/pssp/default.nix4
-rw-r--r--pkgs/applications/science/math/sage/default.nix31
-rw-r--r--pkgs/applications/science/math/singular/default.nix13
-rw-r--r--pkgs/applications/science/math/sloane/default.nix28
-rw-r--r--pkgs/applications/science/math/weka/default.nix2
-rw-r--r--pkgs/applications/science/math/wxmaxima/default.nix2
-rw-r--r--pkgs/applications/science/math/yacas/default.nix2
-rw-r--r--pkgs/applications/science/misc/boinc/default.nix8
-rw-r--r--pkgs/applications/science/misc/fityk/default.nix23
-rw-r--r--pkgs/applications/science/misc/golly/default.nix14
-rw-r--r--pkgs/applications/science/misc/megam/default.nix46
-rw-r--r--pkgs/applications/science/misc/megam/ocaml-3.12.patch12
-rw-r--r--pkgs/applications/science/misc/megam/ocaml-includes.patch21
-rw-r--r--pkgs/applications/science/misc/root/cmake.patch11
-rw-r--r--pkgs/applications/science/misc/root/default.nix27
-rw-r--r--pkgs/applications/science/misc/simgrid/default.nix37
-rw-r--r--pkgs/applications/science/misc/tulip/default.nix2
-rw-r--r--pkgs/applications/science/misc/vite/default.nix2
-rw-r--r--pkgs/applications/science/molecular-dynamics/gromacs/default.nix6
-rw-r--r--pkgs/applications/science/spyder/default.nix6
81 files changed, 1280 insertions, 211 deletions
diff --git a/pkgs/applications/science/astronomy/celestia/default.nix b/pkgs/applications/science/astronomy/celestia/default.nix
index d7814aa5b78f..d4da5c113c99 100644
--- a/pkgs/applications/science/astronomy/celestia/default.nix
+++ b/pkgs/applications/science/astronomy/celestia/default.nix
@@ -65,6 +65,8 @@ stdenv.mkDerivation {
     )
   '';
 
+  installPhase = ''make MKDIR_P="mkdir -p" install'';
+
   enableParallelBuilding = true;
 
   meta = {
diff --git a/pkgs/applications/science/astronomy/gravit/default.nix b/pkgs/applications/science/astronomy/gravit/default.nix
index a2cc07b0a61c..696890f95f1e 100644
--- a/pkgs/applications/science/astronomy/gravit/default.nix
+++ b/pkgs/applications/science/astronomy/gravit/default.nix
@@ -15,7 +15,7 @@ stdenv.mkDerivation rec {
   meta = {
     homepage = "http://gravit.slowchop.com";
     description = "A beautiful OpenGL-based gravity simulator";
-    license = "GPLv2";
+    license = stdenv.lib.licenses.gpl2;
 
     longDescription = ''
       Gravit is a gravity simulator which runs under Linux, Windows and
diff --git a/pkgs/applications/science/astronomy/stellarium/default.nix b/pkgs/applications/science/astronomy/stellarium/default.nix
index 04c82b21e859..6b84143d0138 100644
--- a/pkgs/applications/science/astronomy/stellarium/default.nix
+++ b/pkgs/applications/science/astronomy/stellarium/default.nix
@@ -1,14 +1,11 @@
-{stdenv, fetchurl, cmake, freetype, libpng, mesa, gettext, openssl, qt4, perl, libiconv}:
+{ stdenv, fetchurl, cmake, freetype, libpng, mesa, gettext, openssl, qt4, perl, libiconv }:
 
-let
-  name = "stellarium-0.12.1";
-in
-stdenv.mkDerivation {
-  inherit name;
+stdenv.mkDerivation rec {
+  name = "stellarium-0.12.4";
 
   src = fetchurl {
     url = "mirror://sourceforge/stellarium/${name}.tar.gz";
-    sha256 = "02qfp56mkg3bqggv3ndx8v6zfswg51gkczwiqy5c9y4rw28hazla";
+    sha256 = "11367hv9niyz9v47lf31vjsqkgc8da0vy2nhiyxgmk1i49p1pbhg";
   };
 
   buildInputs = [ cmake freetype libpng mesa gettext openssl qt4 perl libiconv ];
diff --git a/pkgs/applications/science/astronomy/xplanet/default.nix b/pkgs/applications/science/astronomy/xplanet/default.nix
index 816119a3b925..bdb93c992262 100644
--- a/pkgs/applications/science/astronomy/xplanet/default.nix
+++ b/pkgs/applications/science/astronomy/xplanet/default.nix
@@ -2,15 +2,17 @@
 , libjpeg, netpbm}:
 
 stdenv.mkDerivation rec {
-  name = "xplanet-1.2.2";
+  name = "xplanet-1.3.0";
 
   src = fetchurl {
     url = "mirror://sourceforge/xplanet/${name}.tar.gz";
-    sha256 = "1jnkrly9njkibxqbg5im4pq9cqjzwmki6jzd318dvlfmnicqr3vg";
+    sha256 = "0hml2v228wi2r61m1pgka7h96rl92b6apk0iigm62miyp4mp9ys4";
   };
 
   buildInputs = [ pkgconfig freetype pango libpng libtiff giflib libjpeg netpbm ];
 
+  patches = [ ./giflib.patch ];
+
   meta = {
     description = "Renders an image of the earth or other planets into the X root window";
     homepage = http://xplanet.sourceforge.net;
diff --git a/pkgs/applications/science/astronomy/xplanet/giflib.patch b/pkgs/applications/science/astronomy/xplanet/giflib.patch
new file mode 100644
index 000000000000..aaf024198fbc
--- /dev/null
+++ b/pkgs/applications/science/astronomy/xplanet/giflib.patch
@@ -0,0 +1,130 @@
+diff -wbBur xplanet-1.3.0/src/libimage/gif.c /home/sergej/tmp/BUILD/staging-i686/sergej/build/xplanet/src/xplanet-1.3.0/src/libimage/gif.c
+--- xplanet-1.3.0/src/libimage/gif.c	2006-03-26 01:50:51.000000000 +0300
++++ /home/sergej/tmp/BUILD/staging-i686/sergej/build/xplanet/src/xplanet-1.3.0/src/libimage/gif.c	2013-07-30 18:21:17.412474692 +0400
+@@ -20,7 +20,7 @@
+ 
+ #include <stdio.h>
+ #include <stdlib.h>
+-
++#define FALSE 0
+ #include <gif_lib.h>
+ 
+ /*
+@@ -42,11 +42,11 @@
+     int color_index;
+     unsigned char *ptr = NULL;
+ 
+-    infile = DGifOpenFileName(filename);
++    infile = DGifOpenFileName(filename, NULL);
+ 
+     if (infile == NULL)
+     {
+-        PrintGifError();
++        printf("%s\n", GifErrorString(GIF_ERROR));
+         return(0);
+     }
+ 
+@@ -54,7 +54,7 @@
+     {
+         if (DGifGetRecordType(infile, &record_type) == GIF_ERROR) 
+         {
+-            PrintGifError();
++            printf("%s\n", GifErrorString(GIF_ERROR));
+             return(0);
+         }
+ 
+@@ -63,7 +63,7 @@
+         case IMAGE_DESC_RECORD_TYPE:
+             if (DGifGetImageDesc(infile) == GIF_ERROR)
+             {
+-                PrintGifError();
++                printf("%s\n", GifErrorString(GIF_ERROR));
+                 return(0);
+             }
+ 
+@@ -107,14 +107,14 @@
+             GifByteType *ext;
+             if (DGifGetExtension(infile, &ext_code, &ext) == GIF_ERROR) 
+             {
+-                PrintGifError();
++                printf("%s\n", GifErrorString(GIF_ERROR));
+                 return(0);
+             }
+             while (ext != NULL) 
+             {
+                 if (DGifGetExtensionNext(infile, &ext) == GIF_ERROR) 
+                 {
+-                    PrintGifError();
++                    printf("%s\n", GifErrorString(GIF_ERROR));
+                     return(0);
+                 }
+             }
+@@ -178,7 +178,7 @@
+         return(0);
+     }
+ 
+-    colormap = MakeMapObject(colormap_size, NULL);
++    colormap = GifMakeMapObject(colormap_size, NULL);
+ 
+     for (i = 0; i < width * height; i++)
+     {
+@@ -187,10 +187,10 @@
+         blue[i]  = (GifByteType) rgb[3*i+2];
+     }
+   
+-    if (QuantizeBuffer(width, height, &colormap_size, red, green, blue,   
++    if (GifQuantizeBuffer(width, height, &colormap_size, red, green, blue,   
+                        buffer, colormap->Colors) == GIF_ERROR)
+     {
+-        PrintGifError();
++        printf("%s\n", GifErrorString(GIF_ERROR));
+         return(0);
+     }
+ 
+@@ -198,24 +198,24 @@
+     free(green);
+     free(blue);
+ 
+-    outfile = EGifOpenFileName((char *) filename, FALSE);
++    outfile = EGifOpenFileName((char *) filename, FALSE, NULL);
+     if (outfile == NULL)
+     {
+-        PrintGifError();
++        printf("%s\n", GifErrorString(GIF_ERROR));
+         return(0);
+     }
+ 
+     if (EGifPutScreenDesc(outfile, width, height, colormap_size, 0, colormap)
+         == GIF_ERROR)
+     {
+-        PrintGifError();
++        printf("%s\n", GifErrorString(GIF_ERROR));
+         return(0);
+     }
+ 
+     if (EGifPutImageDesc(outfile, 0, 0, width, height, FALSE, NULL)
+         == GIF_ERROR)
+     {
+-        PrintGifError();
++        printf("%s\n", GifErrorString(GIF_ERROR));
+         return(0);
+     }
+ 
+@@ -224,7 +224,7 @@
+     {
+         if (EGifPutLine(outfile, ptr, width) == GIF_ERROR)
+         {
+-            PrintGifError();
++            printf("%s\n", GifErrorString(GIF_ERROR));
+             return(0);
+         }
+         ptr += width;
+@@ -233,7 +233,7 @@
+     EGifSpew(outfile);
+ 
+     if (EGifCloseFile(outfile) == GIF_ERROR) 
+-        PrintGifError();
++        printf("%s\n", GifErrorString(GIF_ERROR));
+ 
+     free(buffer);
+ 
diff --git a/pkgs/applications/science/biology/arb/default.nix b/pkgs/applications/science/biology/arb/default.nix
index 279091f21bd2..2f622e94057b 100644
--- a/pkgs/applications/science/biology/arb/default.nix
+++ b/pkgs/applications/science/biology/arb/default.nix
@@ -81,5 +81,6 @@ stdenv.mkDerivation {
     pkgMaintainer = "http://BioLib.open-bio.org/";
     homepage    = http://www.arb-home.de/;
     priority    = "10";   # because it includes binaries of clustal etc.
+    broken = true;
   };
 }
diff --git a/pkgs/applications/science/biology/plink/default.nix b/pkgs/applications/science/biology/plink/default.nix
index fa6dcaa82ede..009e12aa02f0 100644
--- a/pkgs/applications/science/biology/plink/default.nix
+++ b/pkgs/applications/science/biology/plink/default.nix
@@ -18,7 +18,8 @@ stdenv.mkDerivation {
   meta = {
     description = "Whole genome association toolkit";
     homepage = "http://pngu.mgh.harvard.edu/~purcell/plink/";
-    license = "GNUv2";
+    license = stdenv.lib.licenses.gpl2;
     platforms = stdenv.lib.platforms.all;
+    broken = true;
   };
 }
diff --git a/pkgs/applications/science/chemistry/avogadro/default.nix b/pkgs/applications/science/chemistry/avogadro/default.nix
index e45f5b645fd9..1e9f3ee521b1 100644
--- a/pkgs/applications/science/chemistry/avogadro/default.nix
+++ b/pkgs/applications/science/chemistry/avogadro/default.nix
@@ -1,16 +1,16 @@
-{ stdenv, fetchurl, cmake, qt4, zlib, eigen, openbabel, pkgconfig, mesa, libX11 }:
+{ stdenv, fetchurl, cmake, qt4, zlib, eigen, openbabel, pkgconfig, mesa, libX11, doxygen }:
 
 stdenv.mkDerivation rec {
-  name = "avogadro-1.0.3";
+  name = "avogadro-1.1.1";
 
   src = fetchurl {
     url = "mirror://sourceforge/avogadro/${name}.tar.bz2";
-    sha256 = "0s44r78vm7hf4cs13d2qki3gf178gjj1ihph6rs04g6s4figvdpg";
+    sha256 = "050ag9p4vg7jg8hj1wqfv7lsm6ar2isxjw2vw85s49vsl7g7nvzy";
   };
 
   buildInputs = [ qt4 eigen zlib openbabel mesa libX11 ];
 
-  nativeBuildInputs = [ cmake pkgconfig ];
+  nativeBuildInputs = [ cmake pkgconfig doxygen ];
 
   NIX_CFLAGS_COMPILE = "-include ${mesa}/include/GL/glu.h";
 
diff --git a/pkgs/applications/science/electronics/archimedes/default.nix b/pkgs/applications/science/electronics/archimedes/default.nix
index f22ef09a9839..a6a5f68755a4 100644
--- a/pkgs/applications/science/electronics/archimedes/default.nix
+++ b/pkgs/applications/science/electronics/archimedes/default.nix
@@ -1,17 +1,17 @@
 {stdenv, fetchurl}:
 
 stdenv.mkDerivation rec {
-  name = "archimedes-2.0.0";
+  name = "archimedes-2.0.1";
 
   src = fetchurl {
     url = "mirror://gnu/archimedes/${name}.tar.gz";
-    sha256 = "1ajg4xvk5slv05fsbikrina9g4bmhx8gykk249yz21pir67sdk4x";
+    sha256 = "0jfpnd3pns5wxcxbiw49v5sgpmm5b4v8s4q1a5292hxxk2hzmb3z";
   };
 
   meta = {
     description = "GNU package for semiconductor device simulations";
     homepage = http://www.gnu.org/software/archimedes;
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     platforms = with stdenv.lib.platforms; linux;
   };
 }
diff --git a/pkgs/applications/science/electronics/caneda/default.nix b/pkgs/applications/science/electronics/caneda/default.nix
index d135fb094345..404ffc5010b4 100644
--- a/pkgs/applications/science/electronics/caneda/default.nix
+++ b/pkgs/applications/science/electronics/caneda/default.nix
@@ -32,7 +32,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Open source EDA software focused on easy of use and portability";
     homepage = http://caneda.tuxfamily.org;
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = with stdenv.lib.maintainers; [viric];
     platforms = with stdenv.lib.platforms; linux;
   };
diff --git a/pkgs/applications/science/electronics/gtkwave/default.nix b/pkgs/applications/science/electronics/gtkwave/default.nix
index bb4b969f0621..c761f6196424 100644
--- a/pkgs/applications/science/electronics/gtkwave/default.nix
+++ b/pkgs/applications/science/electronics/gtkwave/default.nix
@@ -1,10 +1,10 @@
 {stdenv, fetchurl, gtk, gperf, pkgconfig, bzip2, tcl, tk, judy, xz}:
 stdenv.mkDerivation rec {
-  name = "gtkwave-3.3.39";
+  name = "gtkwave-3.3.53";
 
   src = fetchurl {
     url = "mirror://sourceforge/gtkwave/${name}.tar.gz";
-    sha256 = "1va506anlbpbha7l6h94s44xjdy6ch22iv629swn4bh5m3qi33bg";
+    sha256 = "1jmrk2p2azjca250h2bi4c8v0cp1gqd3c027dx18sxy3cgw1fsp1";
   };
 
   buildInputs = [ gtk gperf pkgconfig bzip2 tcl tk judy xz ];
@@ -14,7 +14,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Wave viewer for Unix and Win32";
     homepage = http://gtkwave.sourceforge.net;
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = with stdenv.lib.maintainers; [viric];
     platforms = with stdenv.lib.platforms; linux;
   };
diff --git a/pkgs/applications/science/electronics/kicad/default.nix b/pkgs/applications/science/electronics/kicad/default.nix
index cc53611493d0..1fc97abef927 100644
--- a/pkgs/applications/science/electronics/kicad/default.nix
+++ b/pkgs/applications/science/electronics/kicad/default.nix
@@ -1,21 +1,21 @@
-{ stdenv, fetchurl, fetchbzr, unzip, cmake, mesa, gtk, wxGTK, zlib, libX11, 
-gettext, cups } : 
+{ stdenv, fetchurl, fetchbzr, cmake, mesa, wxGTK, zlib, libX11, gettext }:
 
 stdenv.mkDerivation rec {
-  name = "kicad-20130325";
+  name = "kicad-20131025";
 
-  src = fetchurl {
-    url = "http://iut-tice.ujf-grenoble.fr/cao/kicad-sources-stable_2013-03-25_BZR4005.zip";
-    sha256 = "0hg2aiis14am7mmpimcxnxvhy7c7fr5rgzlk6rjv44d9m0f9957m";
+  src = fetchbzr {
+    url = "https://code.launchpad.net/~kicad-stable-committers/kicad/stable";
+    rev = 4024;
+    sha256 = "1sv1l2zpbn6439ccz50p05hvqg6j551aqra551wck9h3929ghly5";
   };
 
   srcLibrary = fetchbzr {
     url = "http://bazaar.launchpad.net/~kicad-lib-committers/kicad/library";
-    revision = 220;
-    sha256 = "0l2lblgnm51n2w1p4ifpwdvq04rxgq73zrfxlhqa9zdlyh4rcddb";
+    rev = 293;
+    sha256 = "1wn9a4nhqyjzzfkq6xm7ag8n5n10xy7gkq6i7yry7wxini7pzv1i";
   };
 
-  cmakeFlags = "-DKICAD_TESTING_VERSION=ON";
+  cmakeFlags = "-DKICAD_STABLE_VERSION=ON";
 
   # They say they only support installs to /usr or /usr/local,
   # so we have to handle this.
@@ -23,9 +23,9 @@ stdenv.mkDerivation rec {
     sed -i -e 's,/usr/local/kicad,'$out,g common/gestfich.cpp
   '';
 
-  enableParallelBuilding = true;
+  #enableParallelBuilding = true; # often fails on Hydra: fatal error: pcb_plot_params_lexer.h: No such file or directory
 
-  buildInputs = [ unzip cmake mesa wxGTK zlib libX11 gettext ];
+  buildInputs = [ cmake mesa wxGTK zlib libX11 gettext ];
 
   postInstall = ''
     mkdir library
@@ -37,7 +37,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Free Software EDA Suite";
     homepage = "http://www.kicad-pcb.org/";
-    license = "GPLv2";
+    license = stdenv.lib.licenses.gpl2;
     maintainers = with stdenv.lib.maintainers; [viric];
     platforms = with stdenv.lib.platforms; linux;
   };
diff --git a/pkgs/applications/science/electronics/ngspice/default.nix b/pkgs/applications/science/electronics/ngspice/default.nix
index 579492248ea3..493af97d1567 100644
--- a/pkgs/applications/science/electronics/ngspice/default.nix
+++ b/pkgs/applications/science/electronics/ngspice/default.nix
@@ -1,11 +1,11 @@
 {stdenv, fetchurl, readline, bison, libX11, libICE, libXaw, libXext}:
 
 stdenv.mkDerivation {
-  name = "ng-spice-rework-24";
+  name = "ng-spice-rework-25";
 
   src = fetchurl {
-    url = "mirror://sourceforge/ngspice/ngspice-24.tar.gz";
-    sha256 = "0rgh75hbqrsljz767whbj65wi6369yc286v0qk8jxnv2da7p9ll6";
+    url = "mirror://sourceforge/ngspice/ngspice-25.tar.gz";
+    sha256 = "03hlxwvl2j1wlb5yg4swvmph9gja37c2gqvwvzv6z16vg2wvn06h";
   };
 
   buildInputs = [ readline libX11 bison libICE libXaw libXext ];
diff --git a/pkgs/applications/science/electronics/pulseview/default.nix b/pkgs/applications/science/electronics/pulseview/default.nix
new file mode 100644
index 000000000000..07724d932541
--- /dev/null
+++ b/pkgs/applications/science/electronics/pulseview/default.nix
@@ -0,0 +1,24 @@
+{ stdenv, fetchurl, pkgconfig, cmake, glib, qt4, boost, libsigrok
+, libsigrokdecode, libserialport, libzip, udev, libusb1, libftdi
+}:
+
+stdenv.mkDerivation rec {
+  name = "pulseview-0.2.0";
+
+  src = fetchurl {
+    url = "http://sigrok.org/download/source/pulseview/${name}.tar.gz";
+    sha256 = "1pf1dgwd9j586nqmni6gqf3qxrsmawcmi9wzqfzqkjci18xd7dgy";
+  };
+
+  buildInputs = [ pkgconfig cmake glib qt4 boost libsigrok
+    libsigrokdecode libserialport libzip udev libusb1 libftdi
+  ];
+
+  meta = with stdenv.lib; {
+    description = "Qt-based LA/scope/MSO GUI for sigrok (a signal analysis software suite)";
+    homepage = http://sigrok.org/;
+    license = licenses.gpl3Plus;
+    platforms = platforms.linux;
+    maintainers = [ maintainers.bjornfor ];
+  };
+}
diff --git a/pkgs/applications/science/electronics/qfsm/default.nix b/pkgs/applications/science/electronics/qfsm/default.nix
index 0f24784e9e57..160c530e722e 100644
--- a/pkgs/applications/science/electronics/qfsm/default.nix
+++ b/pkgs/applications/science/electronics/qfsm/default.nix
@@ -18,7 +18,6 @@ stdenv.mkDerivation rec {
     description = "Graphical editor for finite state machines";
     homepage = "http://qfsm.sourceforge.net/";
     license = stdenv.lib.licenses.gpl3Plus;
-    maintainers = [ stdenv.lib.maintainers.simons ];
-    platforms = stdenv.lib.platforms.linux;
+    broken = true;
   };
 }
diff --git a/pkgs/applications/science/electronics/qucs/default.nix b/pkgs/applications/science/electronics/qucs/default.nix
index e434c97db2b0..dd3eaecc7441 100644
--- a/pkgs/applications/science/electronics/qucs/default.nix
+++ b/pkgs/applications/science/electronics/qucs/default.nix
@@ -16,7 +16,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Integrated circuit simulator";
     homepage = http://qucs.sourceforge.net;
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = with stdenv.lib.maintainers; [viric];
     platforms = with stdenv.lib.platforms; linux;
   };
diff --git a/pkgs/applications/science/electronics/tkgate/1.x.nix b/pkgs/applications/science/electronics/tkgate/1.x.nix
index 7c04c85fdb7e..30e882a7f38e 100644
--- a/pkgs/applications/science/electronics/tkgate/1.x.nix
+++ b/pkgs/applications/science/electronics/tkgate/1.x.nix
@@ -1,7 +1,9 @@
-{ stdenv, fetchurl, tcl, tk, libX11, libiconvOrLibc, which, yacc, flex, imake, xproto, gccmakedep }:
-
-assert stdenv.system == "i686-linux" || stdenv.system == "x86_64-linux";
+{ stdenv, fetchurl, tcl, tk, libX11, glibc, which, yacc, flex, imake, xproto, gccmakedep }:
 
+let
+  libiconvInc = stdenv.lib.optionalString stdenv.isLinux "${glibc}/include";
+  libiconvLib = stdenv.lib.optionalString stdenv.isLinux "${glibc}/lib";
+in
 stdenv.mkDerivation rec {
   name = "tkgate-1.8.7";
 
@@ -10,13 +12,13 @@ stdenv.mkDerivation rec {
     sha256 = "1pqywkidfpdbj18i03h97f4cimld4fb3mqfy8jjsxs12kihm18fs";
   };
 
-  buildInputs = [ tcl tk libX11 libiconvOrLibc which yacc flex imake xproto gccmakedep ];
+  buildInputs = [ tcl tk libX11 which yacc flex imake xproto gccmakedep ];
 
   patchPhase = ''
     sed -i config.h \
       -e 's|.*#define.*TKGATE_TCLTK_VERSIONS.*|#define TKGATE_TCLTK_VERSIONS "8.5"|' \
-      -e 's|.*#define.*TKGATE_INCDIRS.*|#define TKGATE_INCDIRS "${tcl}/include ${tk}/include ${libiconvOrLibc}/include ${libX11}/include"|' \
-      -e 's|.*#define.*TKGATE_LIBDIRS.*|#define TKGATE_LIBDIRS "${tcl}/lib ${tk}/lib ${libiconvOrLibc}/lib ${libX11}/lib"|' \
+      -e 's|.*#define.*TKGATE_INCDIRS.*|#define TKGATE_INCDIRS "${tcl}/include ${tk}/include ${libiconvInc} ${libX11}/include"|' \
+      -e 's|.*#define.*TKGATE_LIBDIRS.*|#define TKGATE_LIBDIRS "${tcl}/lib ${tk}/lib ${libiconvLib} ${libX11}/lib"|' \
       \
       -e '20 i #define TCL_LIBRARY "${tcl}/lib"' \
       -e '20 i #define TK_LIBRARY "${tk}/lib/${tk.libPrefix}"' \
@@ -31,8 +33,8 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Event driven digital circuit simulator with a TCL/TK-based graphical editor";
     homepage = "http://www.tkgate.org/";
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = [ stdenv.lib.maintainers.simons ];
-    platforms = stdenv.lib.platforms.linux;
+    hydraPlatforms = stdenv.lib.platforms.linux;
   };
 }
diff --git a/pkgs/applications/science/electronics/tkgate/2.x.nix b/pkgs/applications/science/electronics/tkgate/2.x.nix
index 756fe7052d83..108986ddefe4 100644
--- a/pkgs/applications/science/electronics/tkgate/2.x.nix
+++ b/pkgs/applications/science/electronics/tkgate/2.x.nix
@@ -1,7 +1,9 @@
-{ stdenv, fetchurl, tcl, tk, libX11, libiconvOrLibc }:
-
-assert stdenv.system == "i686-linux" || stdenv.system == "x86_64-linux";
+{ stdenv, fetchurl, tcl, tk, libX11, glibc }:
 
+let
+  libiconvInc = stdenv.lib.optionalString stdenv.isLinux "${glibc}/include";
+  libiconvLib = stdenv.lib.optionalString stdenv.isLinux "${glibc}/lib";
+in
 stdenv.mkDerivation rec {
   name = "tkgate-2.0-b10";
 
@@ -16,8 +18,8 @@ stdenv.mkDerivation rec {
 
   patchPhase = ''
     sed -i configure \
-      -e 's|TKGATE_INCDIRS=.*|TKGATE_INCDIRS="${tcl}/include ${tk}/include ${libiconvOrLibc}/include"|' \
-      -e 's|TKGATE_LIBDIRS=.*|TKGATE_LIBDIRS="${tcl}/lib ${tk}/lib ${libiconvOrLibc}/lib"|'
+      -e 's|TKGATE_INCDIRS=.*|TKGATE_INCDIRS="${tcl}/include ${tk}/include ${libiconvInc}"|' \
+      -e 's|TKGATE_LIBDIRS=.*|TKGATE_LIBDIRS="${tcl}/lib ${tk}/lib ${libiconvLib}"|'
     sed -i options.h \
       -e 's|.* #define TCL_LIBRARY .*|#define TCL_LIBRARY "${tcl}/${tcl.libdir}"|' \
       -e 's|.* #define TK_LIBRARY .*|#define TK_LIBRARY "${tk}/lib/${tk.libPrefix}"|'
@@ -26,8 +28,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Event driven digital circuit simulator with a TCL/TK-based graphical editor";
     homepage = "http://www.tkgate.org/";
-    license = "GPLv2+";
-    maintainers = [ stdenv.lib.maintainers.simons ];
-    platforms = stdenv.lib.platforms.linux;
+    license = stdenv.lib.licenses.gpl2Plus;
+    broken = true;
   };
 }
diff --git a/pkgs/applications/science/electronics/verilog/default.nix b/pkgs/applications/science/electronics/verilog/default.nix
index a4c803e2952c..e68d2a4ab91a 100644
--- a/pkgs/applications/science/electronics/verilog/default.nix
+++ b/pkgs/applications/science/electronics/verilog/default.nix
@@ -1,19 +1,20 @@
 {stdenv, fetchurl, gperf, flex, bison}:
 
 stdenv.mkDerivation rec {
-  name = "verilog-0.9.3";
+  name = "verilog-0.9.7";
 
   src = fetchurl {
     url = "mirror://sourceforge/iverilog/${name}.tar.gz";
-    sha256 = "dd68c8ab874a93805d1e93fa76ee1e91fc0c7b20822ded3e57b6536cd8c0d1ba";
+    sha256 = "0m3liqw7kq24vn7k8wvi630ljz0awz23r3sd4rcklk7vgghp4pks";
   };
 
   buildInputs = [ gperf flex bison ];
 
   meta = {
     description = "Icarus Verilog compiler";
+    repositories.git = https://github.com/steveicarus/iverilog.git;
     homepage = http://www.icarus.com;
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = with stdenv.lib.maintainers; [winden];
     platforms = with stdenv.lib.platforms; linux;
   };
diff --git a/pkgs/applications/science/electronics/xoscope/default.nix b/pkgs/applications/science/electronics/xoscope/default.nix
index 54aae9e7d3bf..df7d053d93bd 100644
--- a/pkgs/applications/science/electronics/xoscope/default.nix
+++ b/pkgs/applications/science/electronics/xoscope/default.nix
@@ -16,7 +16,7 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Oscilloscope through the sound card";
     homepage = http://xoscope.sourceforge.net;
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = with stdenv.lib.maintainers; [viric];
     platforms = with stdenv.lib.platforms; linux;
   };
diff --git a/pkgs/applications/science/geometry/tetgen/default.nix b/pkgs/applications/science/geometry/tetgen/default.nix
index a43ec3b0eb9f..ddfb92def958 100644
--- a/pkgs/applications/science/geometry/tetgen/default.nix
+++ b/pkgs/applications/science/geometry/tetgen/default.nix
@@ -4,8 +4,8 @@ stdenv.mkDerivation rec {
   name = "tetgen-1.4.3";
 
   src = fetchurl {
-    url = http://tetgen.berlios.de/files/tetgen1.4.3.tar.gz;
-    sha256 = "159i0vdjz7abb8bycz47ax4fqlzc82kv19sygqnrkr86qm4g43wy";
+    url = "${meta.homepage}/files/tetgen1.4.3.tar.gz";
+    sha256 = "0d70vjqdapmy1ghlsxjlvl5z9yp310zw697bapc4zxmp0sxi29wm";
   };
 
   installPhase = ''
@@ -15,7 +15,7 @@ stdenv.mkDerivation rec {
 
   meta = {
     description = "Quality Tetrahedral Mesh Generator and 3D Delaunay Triangulator";
-    homepage = "http://tetgen.berlios.de/";
-    license = "MIT";
+    homepage = "http://tetgen.org/";
+    license = stdenv.lib.licenses.mit;
   };
 }
diff --git a/pkgs/applications/science/logic/abc/default.nix b/pkgs/applications/science/logic/abc/default.nix
new file mode 100644
index 000000000000..30c36ae29dc8
--- /dev/null
+++ b/pkgs/applications/science/logic/abc/default.nix
@@ -0,0 +1,27 @@
+{ fetchhg, stdenv, readline }:
+
+stdenv.mkDerivation rec {
+  name = "abc-verifier-${version}";
+  version = "140509"; # YYMMDD
+
+  src = fetchhg {
+    url    = "https://bitbucket.org/alanmi/abc";
+    rev    = "03e221443d71e49e56cbc37f1907ee3b0ff3e7c9";
+    sha256 = "0ahrqg718y7xpv939f6x8w1kqh7wsja4pw8hca7j67j0qjdgb4lm";
+  };
+
+  buildInputs = [ readline ];
+  enableParallelBuilding = true;
+  installPhase = ''
+    mkdir -p $out/bin
+    mv abc $out/bin
+  '';
+
+  meta = {
+    description = "Sequential Logic Synthesis and Formal Verification";
+    homepage    = "www.eecs.berkeley.edu/~alanmi/abc/abc.htm";
+    license     = stdenv.lib.licenses.mit;
+    platforms   = stdenv.lib.platforms.unix;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix
new file mode 100644
index 000000000000..2a95d0cd65bb
--- /dev/null
+++ b/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -0,0 +1,23 @@
+{ fetchurl, stdenv, ocaml, ocamlPackages, gmp }:
+
+stdenv.mkDerivation rec {
+  name = "alt-ergo-${version}";
+  version = "0.95.2";
+
+  src = fetchurl {
+    url    = "http://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
+    name   = "${name}.tar.gz";
+    sha256 = "1b7f0rh3jgm67g0x2m3wv7gnnqmz9cjlrfm136z56ihlkhsd8v2s";
+  };
+
+  buildInputs = with ocamlPackages;
+    [ ocaml findlib ocamlgraph zarith lablgtk gmp ];
+
+  meta = {
+    description = "Alt-Ergo is a high-performance theorem prover and SMT solver";
+    homepage    = "http://alt-ergo.ocamlpro.com/";
+    license     = stdenv.lib.licenses.cecill-c; # LGPL-2 compatible
+    platforms   = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/boolector/default.nix b/pkgs/applications/science/logic/boolector/default.nix
new file mode 100644
index 000000000000..3879ee8ef470
--- /dev/null
+++ b/pkgs/applications/science/logic/boolector/default.nix
@@ -0,0 +1,47 @@
+{ stdenv, fetchurl, zlib, useV16 ? false }:
+
+let
+  v15 = rec {
+    name    = "boolector-${version}";
+    version = "1.5.118";
+    src = fetchurl {
+      url    = "http://fmv.jku.at/boolector/${name}-with-sat-solvers.tar.gz";
+      sha256 = "17j7q02rryvfwgvglxnhx0kv8hxwy8wbhzawn48lw05i98vxlmk9";
+    };
+  };
+
+  v16 = rec {
+    name    = "boolector-${version}";
+    version = "1.6.0";
+    src = fetchurl {
+      url    = "http://fmv.jku.at/boolector/${name}-with-sat-solvers.tar.gz";
+      sha256 = "0jka4r6bc3i24axgdp6qbq6gjadwz9kvi11s2c5sbwmdnjd7cp85";
+    };
+  };
+
+  boolectorPkg = if useV16 then v16 else v15;
+  license = with stdenv.lib.licenses; if useV16 then unfreeRedistributable else gpl3;
+in
+stdenv.mkDerivation (boolectorPkg // {
+  buildInputs = [ zlib ];
+  enableParallelBuilding = false;
+
+  buildPhase = "./build.sh";
+
+  installPhase = ''
+    mkdir -p $out/bin $out/lib $out/include
+    cp boolector/boolector      $out/bin
+    cp boolector/deltabtor      $out/bin
+    cp boolector/synthebtor     $out/bin
+    cp boolector/libboolector.a $out/lib
+    cp boolector/boolector.h    $out/include
+  '';
+
+  meta = {
+    inherit license;
+    description = "An extremely fast SMT solver for bit-vectors and arrays";
+    homepage    = "http://fmv.jku.at/boolector";
+    platforms   = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+})
diff --git a/pkgs/applications/science/logic/coq/HEAD.nix b/pkgs/applications/science/logic/coq/HEAD.nix
new file mode 100644
index 000000000000..8e6fde6bc240
--- /dev/null
+++ b/pkgs/applications/science/logic/coq/HEAD.nix
@@ -0,0 +1,57 @@
+# - coqide compilation can be disabled by setting lablgtk to null;
+
+{stdenv, fetchgit, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+
+let 
+  version = "8.5pre-8bc01590";
+  buildIde = lablgtk != null;
+  ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
+  idePath = if buildIde then ''
+    CAML_LD_LIBRARY_PATH=${lablgtk}/lib/ocaml/3.12.1/site-lib/stublibs
+  '' else "";
+in
+
+stdenv.mkDerivation {
+  name = "coq-${version}";
+
+  src = fetchgit {
+    url = git://scm.gforge.inria.fr/coq/coq.git;
+    rev = "8bc0159095cb0230a50c55a1611c8b77134a6060";
+    sha256 = "1cp4hbk9jw78y03vwz099yvixax161h60hsbyvwiwz2z5czjxzcv";
+  };
+
+  buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
+
+  postPatch = ''
+    UNAME=$(type -tp uname)
+    RM=$(type -tp rm)
+    substituteInPlace configure --replace "/bin/uname" "$UNAME"
+    substituteInPlace tools/beautify-archive --replace "/bin/rm" "$RM"
+  '';
+
+  preConfigure = ''
+    buildFlagsArray=(${idePath})
+    configureFlagsArray=(
+      -opt
+      ${ideFlags}
+    )
+  '';
+
+  prefixKey = "-prefix ";
+
+  buildFlags = "revision coq coqide";
+
+  meta = {
+    description = "Coq proof assistant";
+    longDescription = ''
+      Coq is a formal proof management system.  It provides a formal language
+      to write mathematical definitions, executable algorithms and theorems
+      together with an environment for semi-interactive development of
+      machine-checked proofs.
+    '';
+    homepage = "http://coq.inria.fr";
+    license = "LGPL";
+    maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ];
+    platforms = stdenv.lib.platforms.unix;
+  };
+}
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index b4a7a203a3c4..678ec6a4b049 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -3,7 +3,7 @@
 {stdenv, fetchurl, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
 
 let 
-  version = "8.4pl2";
+  version = "8.4pl4";
   buildIde = lablgtk != null;
   ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else "";
   idePath = if buildIde then ''
@@ -16,7 +16,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "http://coq.inria.fr/distrib/V${version}/files/coq-${version}.tar.gz";
-    sha256 = "1n52pky7bb45irk2jw6f4rd3kvy8lm2yfldjwdhiic0kyqw9lwgv";
+    sha256 = "00bzf4kfbd0g279jrr8ynzvb9wqcly3wi577bkrxivhrg2msxhq6";
   };
 
   buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
@@ -54,7 +54,7 @@ stdenv.mkDerivation {
     '';
     homepage = "http://coq.inria.fr";
     license = "LGPL";
-    maintainers = [ stdenv.lib.maintainers.roconnor ];
-    platforms = stdenv.lib.platforms.linux;
+    maintainers = with stdenv.lib.maintainers; [ roconnor thoughtpolice ];
+    platforms = stdenv.lib.platforms.unix;
   };
 }
diff --git a/pkgs/applications/science/logic/cvc3/default.nix b/pkgs/applications/science/logic/cvc3/default.nix
index 9bb8f8cde4ca..07b87e3cf073 100644
--- a/pkgs/applications/science/logic/cvc3/default.nix
+++ b/pkgs/applications/science/logic/cvc3/default.nix
@@ -12,10 +12,10 @@ let
     ++ [(a.lib.overrideDerivation x.gmp (y: {dontDisableStatic=true;}))];
   sourceInfo = rec {
     baseName="cvc3";
-    version="2.2";
+    version="2.4.1";
     name="${baseName}-${version}";
     url="http://www.cs.nyu.edu/acsys/cvc3/releases/${version}/${name}.tar.gz";
-    hash="1dw12d5vrixfr6l9j6j7026vrr22zb433xyl6n5yxx4hgfywi0ji";
+    hash="1xxcwhz3y6djrycw8sm6xz83wb4hb12rd1n0skvc7fng0rh1snym";
   };
 in
 rec {
diff --git a/pkgs/applications/science/logic/ekrhyper/default.nix b/pkgs/applications/science/logic/ekrhyper/default.nix
index c90099f495a2..e1eb9a2dcc3b 100644
--- a/pkgs/applications/science/logic/ekrhyper/default.nix
+++ b/pkgs/applications/science/logic/ekrhyper/default.nix
@@ -3,11 +3,11 @@ let
   s = # Generated upstream information
   rec {
     baseName="ekrhyper";
-    version="1_4_30072013";
+    version="1_4_21022014";
     name="${baseName}-${version}";
-    hash="0ashsblm477r7dmq9f33wajkbr29rbyyc919mifdgrrdy6zlc663";
-    url="http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/ekrh_1_4_30072013.tar.gz";
-    sha256="0ashsblm477r7dmq9f33wajkbr29rbyyc919mifdgrrdy6zlc663";
+    hash="14xaaxyvfli1nd4vd9fp4j1s8k76z2bhazxzzc7br3q6hc6b8ivw";
+    url="http://userpages.uni-koblenz.de/~bpelzer/ekrhyper/ekrh_1_4_21022014.tar.gz";
+    sha256="14xaaxyvfli1nd4vd9fp4j1s8k76z2bhazxzzc7br3q6hc6b8ivw";
   };
   buildInputs = [
     ocaml perl
diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
index 2e1647b6c71d..dc8e975ce1d1 100644
--- a/pkgs/applications/science/logic/hol/default.nix
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -46,11 +46,11 @@ stdenv.mkDerivation {
     #sed -ie "/compute/,999 d" tools/build-sequence # for testing
 
     poly < tools/smart-configure.sml
-
+    
     bin/build ${kernelFlag} -symlink
 
     mkdir -p "$out/bin"
-    ln -st $out/bin  "$out/src/${holsubdir}/bin/"*
+    ln -st $out/bin  $out/src/${holsubdir}/bin/*
     # ln -s $out/src/hol4.${version}/bin $out/bin
   '';
 
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index d6c1c0c18781..3e6440ea9773 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -1,19 +1,20 @@
-{stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5}:
+{ stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5 }:
 
 let
   start_script = ''
     #!/bin/sh
     cd "$out/lib/hol_light"
-    exec ${ocaml}/bin/ocaml -I "camlp5 -where" -init make.ml
+    exec ${ocaml}/bin/ocaml -I \`${camlp5}/bin/camlp5 -where\` -init make.ml
   '';
 in
+stdenv.mkDerivation rec {
+  name     = "hol_light-${version}";
+  version  = "189";
 
-stdenv.mkDerivation {
-  name = "hol_light-20130324";
   src = fetchsvn {
     url = http://hol-light.googlecode.com/svn/trunk;
-    rev = "157";
-    sha256 = "0d0pbnkw2gb11dn30ggfl91lhdxv86kd1fyiqn170w08n0gi805f";
+    rev = version;
+    sha256 = "1v10l64rs7da2kag3wlb651i09pn83icy9n5z84j8h1iwlxzajdh";
   };
 
   buildInputs = [ ocaml findlib camlp5 ];
@@ -27,16 +28,9 @@ stdenv.mkDerivation {
 
   meta = {
     description = "Interactive theorem prover based on Higher-Order Logic";
-    longDescription = ''
-      HOL Light is a computer program to help users prove interesting
-      mathematical theorems completely formally in Higher-Order Logic.  It sets
-      a very exacting standard of correctness, but provides a number of
-      automated tools and pre-proved mathematical theorems (e.g., about
-      arithmetic, basic set theory and real analysis) to save the user work.
-      It is also fully programmable, so users can extend it with new theorems
-      and inference rules without compromising its soundness.
-    '';
-    homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
-    license = stdenv.lib.licenses.bsd2;
+    homepage    = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
+    license     = stdenv.lib.licenses.bsd2;
+    platforms   = stdenv.lib.platforms.unix;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };
 }
diff --git a/pkgs/applications/science/logic/iprover/default.nix b/pkgs/applications/science/logic/iprover/default.nix
index 2fb9678b8329..e03b33fa43cc 100644
--- a/pkgs/applications/science/logic/iprover/default.nix
+++ b/pkgs/applications/science/logic/iprover/default.nix
@@ -2,9 +2,9 @@ x@{builderDefsPackage
   , ocaml, eprover
   , ...}:
 builderDefsPackage
-(a :  
-let 
-  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+(a :
+let
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
     [];
 
   buildInputs = map (n: builtins.getAttr n x)
@@ -38,7 +38,7 @@ rec {
     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;
@@ -47,7 +47,8 @@ rec {
     ];
     platforms = with a.lib.platforms;
       linux;
-    license = "GPLv3";
+    license = with a.lib.licenses;
+      gpl3;
   };
   passthru = {
     updateInfo = {
@@ -55,4 +56,3 @@ rec {
     };
   };
 }) x
-
diff --git a/pkgs/applications/science/logic/leo2/default.nix b/pkgs/applications/science/logic/leo2/default.nix
index 913171827af1..8f673eb0f15a 100644
--- a/pkgs/applications/science/logic/leo2/default.nix
+++ b/pkgs/applications/science/logic/leo2/default.nix
@@ -1,5 +1,5 @@
 x@{builderDefsPackage
-  , ocaml, eprover
+  , ocaml, eprover, zlib
   , ...}:
 builderDefsPackage
 (a :  
@@ -11,16 +11,16 @@ let
     (builtins.attrNames (builtins.removeAttrs x helperArgNames));
   sourceInfo = rec {
     baseName="leo2";
-    version="1.2.8";
+    version = "1.6.2";
     name="${baseName}_v${version}";
-    url="http://www.ags.uni-sb.de/~leo/${name}.tgz";
-    hash="d46a94f5991623386eb9061cfb0d748e258359a8c690fded173d45303e0e9e3a";
+    url="page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v${version}.tgz";
+    hash="d46a94f5991623386eb9061cfb0d748e258359a8c690fded173d35303e0e9e3a";
   };
 in
 rec {
   src = a.fetchurl {
     url = sourceInfo.url;
-    sha256 = sourceInfo.hash;
+    sha256 = "1wjpmizb181iygnd18lx7p77fwaci2clgzs5ix5j51cc8f3pazmv";
   };
 
   name = "${sourceInfo.baseName}-${sourceInfo.version}";
@@ -43,6 +43,10 @@ rec {
     echo -e "e = ${eprover}/bin/eprover\\nepclextract = ${eprover}/bin/epclextract" > "$out/etc/leoatprc"
   '') ["minInit" "doMake" "defEnsureDir"];
 
+  makeFlags = [
+    "SHELL=${a.stdenv.shell}"
+  ];
+
   meta = {
     description = "A high-performance typed higher order prover";
     maintainers = with a.lib.maintainers;
@@ -52,11 +56,9 @@ rec {
     platforms = with a.lib.platforms;
       linux;
     license = "BSD";
-  };
-  passthru = {
-    updateInfo = {
-      downloadPage = "http://www.ags.uni-sb.de/~leo/download.html";
-    };
+    inherit (sourceInfo) version;
+    homepage = "http://page.mi.fu-berlin.de/cbenzmueller/leo/";
+    downloadPage = "http://page.mi.fu-berlin.de/cbenzmueller/leo/download.html";
   };
 }) x
 
diff --git a/pkgs/applications/science/logic/leo2/default.upstream b/pkgs/applications/science/logic/leo2/default.upstream
new file mode 100644
index 000000000000..52b8ed1cdaa2
--- /dev/null
+++ b/pkgs/applications/science/logic/leo2/default.upstream
@@ -0,0 +1,6 @@
+url http://page.mi.fu-berlin.de/cbenzmueller/leo/download.html
+version_link '[.]tgz'
+version '.*_v([0-9.]+)[.][a-z0-9]+$' '\1'
+do_overwrite () {
+  do_overwrite_just_version
+}
diff --git a/pkgs/applications/science/logic/logisim/default.nix b/pkgs/applications/science/logic/logisim/default.nix
index ab46efa9a961..c71ed73a9925 100644
--- a/pkgs/applications/science/logic/logisim/default.nix
+++ b/pkgs/applications/science/logic/logisim/default.nix
@@ -27,6 +27,6 @@ stdenv.mkDerivation {
   meta = {
     homepage = "http://ozark.hendrix.edu/~burch/logisim";
     description = "Educational tool for designing and simulating digital logic circuits";
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
   };
 }
diff --git a/pkgs/applications/science/logic/ltl2ba/default.nix b/pkgs/applications/science/logic/ltl2ba/default.nix
new file mode 100644
index 000000000000..cdadd18ac9f5
--- /dev/null
+++ b/pkgs/applications/science/logic/ltl2ba/default.nix
@@ -0,0 +1,24 @@
+{ fetchurl, stdenv }:
+
+stdenv.mkDerivation rec {
+  name = "ltl2ba-${version}";
+  version = "1.1";
+
+  src = fetchurl {
+    url    = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/${name}.tar.gz";
+    sha256 = "16z0gc7a9dkarwn0l6rvg5jdhw1q4qyn4501zlchy0zxqddz0sx6";
+  };
+
+  installPhase = ''
+    mkdir -p $out/bin
+    mv ltl2ba $out/bin
+  '';
+
+  meta = {
+    description = "fast translation from LTL formulae to Buchi automata";
+    homepage    = "http://www.lsv.ens-cachan.fr/~gastin/ltl2ba";
+    license     = stdenv.lib.licenses.gpl2Plus;
+    platforms   = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/matita/130312.nix b/pkgs/applications/science/logic/matita/130312.nix
index f77e9d34a2a8..9e98c8db3947 100644
--- a/pkgs/applications/science/logic/matita/130312.nix
+++ b/pkgs/applications/science/logic/matita/130312.nix
@@ -60,7 +60,7 @@ stdenv.mkDerivation {
   meta = {
     homepage = http://matita.cs.unibo.it/;
     description = "Matita is an experimental, interactive theorem prover";
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = [ stdenv.lib.maintainers.roconnor ];
   };
 }
diff --git a/pkgs/applications/science/logic/matita/default.nix b/pkgs/applications/science/logic/matita/default.nix
index 0713ff09e929..f601f97de62e 100644
--- a/pkgs/applications/science/logic/matita/default.nix
+++ b/pkgs/applications/science/logic/matita/default.nix
@@ -48,7 +48,7 @@ stdenv.mkDerivation {
   meta = {
     homepage = http://matita.cs.unibo.it/;
     description = "Matita is an experimental, interactive theorem prover";
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
     maintainers = [ stdenv.lib.maintainers.roconnor ];
   };
 }
diff --git a/pkgs/applications/science/logic/minisat/default.nix b/pkgs/applications/science/logic/minisat/default.nix
index 1f29b3aa1a11..e91ff67fc9cc 100644
--- a/pkgs/applications/science/logic/minisat/default.nix
+++ b/pkgs/applications/science/logic/minisat/default.nix
@@ -2,9 +2,9 @@ x@{builderDefsPackage
   , zlib
   , ...}:
 builderDefsPackage
-(a :  
-let 
-  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+(a :
+let
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
     [];
 
   buildInputs = map (n: builtins.getAttr n x)
@@ -36,7 +36,7 @@ rec {
   setVars = a.fullDepEntry (''
     export MROOT=$PWD/../
   '') ["doUnpack"];
-      
+
   meta = {
     description = "A compact and readable SAT-solver";
     maintainers = with a.lib.maintainers;
@@ -45,7 +45,7 @@ rec {
     ];
     platforms = with a.lib.platforms;
       linux;
-    license = "MIT";
+    license = a.stdenv.lib.licenses.mit;
     homepage = "http://minisat.se/";
   };
   passthru = {
@@ -54,4 +54,3 @@ rec {
     };
   };
 }) x
-
diff --git a/pkgs/applications/science/logic/opensmt/default.nix b/pkgs/applications/science/logic/opensmt/default.nix
index 430537fd57ff..62e11651175f 100644
--- a/pkgs/applications/science/logic/opensmt/default.nix
+++ b/pkgs/applications/science/logic/opensmt/default.nix
@@ -3,9 +3,9 @@ x@{builderDefsPackage
   , gmpxx, flex, bison
   , ...}:
 builderDefsPackage
-(a :  
-let 
-  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+(a :
+let
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
     [];
 
   buildInputs = map (n: builtins.getAttr n x)
@@ -30,17 +30,14 @@ rec {
 
   /* 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";
+    maintainers = [ a.lib.maintainers.raskin ];
+    platforms = a.lib.platforms.linux;
+    license = a.stdenv.lib.licenses.gpl3;
     homepage = "http://code.google.com/p/opensmt/";
+    broken = true;
   };
   passthru = {
     updateInfo = {
@@ -48,4 +45,3 @@ rec {
     };
   };
 }) x
-
diff --git a/pkgs/applications/science/logic/picosat/default.nix b/pkgs/applications/science/logic/picosat/default.nix
index 970daf739fca..6c2cce0ea4b1 100644
--- a/pkgs/applications/science/logic/picosat/default.nix
+++ b/pkgs/applications/science/logic/picosat/default.nix
@@ -35,7 +35,7 @@ stdenv.mkDerivation rec {
   meta = {
     homepage = http://fmv.jku.at/picosat/;
     description = "SAT solver with proof and core support";
-    license = "MIT";
+    license = stdenv.lib.licenses.mit;
     maintainers = [ stdenv.lib.maintainers.roconnor ];
   };
 }
diff --git a/pkgs/applications/science/logic/prooftree/default.nix b/pkgs/applications/science/logic/prooftree/default.nix
new file mode 100644
index 000000000000..caaf4a94a1ed
--- /dev/null
+++ b/pkgs/applications/science/logic/prooftree/default.nix
@@ -0,0 +1,40 @@
+{stdenv, fetchurl, pkgconfig, ocaml, findlib, camlp5, ncurses, lablgtk ? null}:
+
+stdenv.mkDerivation (rec {
+  name = "prooftree-${version}";
+  version = "0.12";
+
+  src = fetchurl {
+    url = "http://askra.de/software/prooftree/releases/prooftree-${version}.tar.gz";
+    sha256 = "08yp66j05pdkdpv9xkfqymqy82mir5xbwfh9mkzhh219xkps4b4m";
+  };
+
+  buildInputs = [ pkgconfig ocaml findlib camlp5 ncurses lablgtk ];
+
+  dontAddPrefix = true;
+  configureFlags = [ "--prefix" "$(out)" ];
+
+  meta = {
+    description = "Prooftree is a program for proof-tree visualization";
+    longDescription = ''
+      Prooftree is a program for proof-tree visualization during interactive
+      proof development in a theorem prover. It is currently being developed
+      for Coq and Proof General. Prooftree helps against getting lost between
+      different subgoals in interactive proof development. It clearly shows
+      where the current subgoal comes from and thus helps in developing the
+      right plan for solving it.
+
+      Prooftree uses different colors for the already proven subgoals, the
+      current branch in the proof and the still open subgoals. Sequent texts
+      are not displayed in the proof tree itself, but they are shown as a
+      tool-tip when the mouse rests over a sequent symbol. Long proof commands
+      are abbreviated in the tree display, but show up in full length as
+      tool-tip. Both, sequents and proof commands, can be shown in the display
+      below the tree (on single click) or in a separate window (on double or
+      shift-click).
+    '';
+    homepage = http://askra.de/software/prooftree;
+    platforms = stdenv.lib.platforms.unix;
+    maintainers = [ stdenv.lib.maintainers.jwiegley ];
+  };
+})
diff --git a/pkgs/applications/science/logic/ssreflect/default.nix b/pkgs/applications/science/logic/ssreflect/default.nix
index 6377db9c8955..a784e5fe1b6e 100644
--- a/pkgs/applications/science/logic/ssreflect/default.nix
+++ b/pkgs/applications/science/logic/ssreflect/default.nix
@@ -6,7 +6,7 @@
 
 let
   pname = "ssreflect";
-  version = "1.4";
+  version = "1.5";
   name = "${pname}-${version}";
   webpage = http://www.msr-inria.inria.fr/Projects/math-components;
 in
@@ -15,8 +15,8 @@ stdenv.mkDerivation {
   inherit name;
 
   src = fetchurl {
-    url = "http://ssr.msr-inria.inria.fr/FTP/${name}-coq8.4.tar.gz";
-    sha256 = "1ysx29xw09i86lq0d92z9cnyx133jfgq4qddy3501000fn7xwi7h";
+    url = "http://ssr.msr-inria.inria.fr/FTP/${name}.tar.gz";
+    sha256 = "0hm1ha7sxqfqhc7iwhx6zdz3nki4rj5nfd3ab24hmz8v7mlpinds";
   };
 
   buildInputs = [ ocaml camlp5 coq makeWrapper ];
diff --git a/pkgs/applications/science/logic/stp/default.nix b/pkgs/applications/science/logic/stp/default.nix
new file mode 100644
index 000000000000..cfe96bc6983a
--- /dev/null
+++ b/pkgs/applications/science/logic/stp/default.nix
@@ -0,0 +1,23 @@
+{stdenv, cmake, boost, bison, flex, fetchgit, perl, zlib}: 
+stdenv.mkDerivation rec {
+  version = "2014.01.07";
+  name = "stp-${version}";
+  src = fetchgit {
+    url    = "git://github.com/stp/stp";
+    rev    = "3aa11620a823d617fc033d26aedae91853d18635";
+    sha256 = "832520787f57f63cf47364d080f30ad10d6d6e00f166790c19b125be3d6dd45c";
+  };
+  buildInputs = [ cmake boost bison flex perl zlib ];
+  cmakeFlags = [ "-DBUILD_SHARED_LIBS=ON" ];
+  patchPhase = ''
+      sed -e 's,^export(PACKAGE.*,,' -i CMakeLists.txt
+      patch -p1 < ${./fixbuild.diff}
+      patch -p1 < ${./fixrefs.diff}
+  '';
+  meta = {
+    description = ''Simple Theorem Prover'';
+    maintainers = with stdenv.lib.maintainers; [mornfall];
+    platforms = with stdenv.lib.platforms; linux;
+    license = with stdenv.lib.licenses; mit;
+  };
+}
diff --git a/pkgs/applications/science/logic/stp/fixbuild.diff b/pkgs/applications/science/logic/stp/fixbuild.diff
new file mode 100644
index 000000000000..01782cb4f40b
--- /dev/null
+++ b/pkgs/applications/science/logic/stp/fixbuild.diff
@@ -0,0 +1,45 @@
+diff --git a/src/libstp/CMakeLists.txt b/src/libstp/CMakeLists.txt
+index 83bd03a..9c0304b 100644
+--- a/src/libstp/CMakeLists.txt
++++ b/src/libstp/CMakeLists.txt
+@@ -23,6 +23,15 @@ set(stp_lib_targets
+     printer
+ )
+ 
++include_directories(${CMAKE_SOURCE_DIR}/src/AST/)
++include_directories(${CMAKE_BINARY_DIR}/src/AST/)
++
++add_library(globalstp OBJECT
++    ../main/Globals.cpp
++    ${CMAKE_CURRENT_BINARY_DIR}/../main/GitSHA1.cpp
++)
++add_dependencies(globalstp ASTKind_header)
++
+ # Create list of objects and gather list of
+ # associated public headers.
+ set(stp_lib_objects "")
+@@ -31,6 +40,7 @@ foreach(target ${stp_lib_targets})
+     list(APPEND stp_lib_objects $<TARGET_OBJECTS:${target}>)
+ 
+     get_target_property(TARGETS_PUBLIC_HEADERS ${target} PUBLIC_HEADER)
++    set_target_properties(${target} PROPERTIES POSITION_INDEPENDENT_CODE ON)
+     if (EXISTS "${TARGETS_PUBLIC_HEADERS}")
+         list(APPEND stp_public_headers "${TARGETS_PUBLIC_HEADERS}")
+         message("Adding public header(s) ${TARGETS_PUBLIC_HEADERS} to target libstp")
+diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
+index 0735137..73039f5 100644
+--- a/src/main/CMakeLists.txt
++++ b/src/main/CMakeLists.txt
+@@ -3,12 +3,6 @@ include_directories(${CMAKE_BINARY_DIR}/src/AST/)
+ 
+ configure_file("${CMAKE_CURRENT_SOURCE_DIR}/GitSHA1.cpp.in" "${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp" @ONLY)
+ 
+-add_library(globalstp OBJECT
+-    Globals.cpp
+-    ${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp
+-)
+-add_dependencies(globalstp ASTKind_header)
+-
+ # -----------------------------------------------------------------------------
+ # Create binary
+ # -----------------------------------------------------------------------------
diff --git a/pkgs/applications/science/logic/stp/fixrefs.diff b/pkgs/applications/science/logic/stp/fixrefs.diff
new file mode 100644
index 000000000000..60ad4949f076
--- /dev/null
+++ b/pkgs/applications/science/logic/stp/fixrefs.diff
@@ -0,0 +1,192 @@
+commit 53b6043e25b2eba264faab845077fbf6736cf22f
+Author: Petr Rockai <me@mornfall.net>
+Date:   Tue Jan 7 13:30:07 2014 +0100
+
+    aig: Comment out unused functions with undefined references in them.
+
+diff --git a/src/extlib-abc/aig/aig/aigPart.c b/src/extlib-abc/aig/aig/aigPart.c
+index a4cc116..5bd5f08 100644
+--- a/src/extlib-abc/aig/aig/aigPart.c
++++ b/src/extlib-abc/aig/aig/aigPart.c
+@@ -869,6 +869,7 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )

+ {

+     extern int Cmd_CommandExecute( void * pAbc, char * sCommand );

+@@ -981,6 +982,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
+     Aig_ManMarkValidChoices( pAig );

+     return pAig;

+ }

++#endif

+ 

+ 

+ ////////////////////////////////////////////////////////////////////////

+diff --git a/src/extlib-abc/aig/aig/aigShow.c b/src/extlib-abc/aig/aig/aigShow.c
+index ae8fa8b..f04eedc 100644
+--- a/src/extlib-abc/aig/aig/aigShow.c
++++ b/src/extlib-abc/aig/aig/aigShow.c
+@@ -326,6 +326,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )

+ {

+     extern void Abc_ShowFile( char * FileNameDot );

+@@ -347,7 +348,7 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
+     // visualize the file 

+     Abc_ShowFile( FileNameDot );

+ }

+-

++#endif

+ 

+ ////////////////////////////////////////////////////////////////////////

+ ///                       END OF FILE                                ///

+diff --git a/src/extlib-abc/aig/dar/darRefact.c b/src/extlib-abc/aig/dar/darRefact.c
+index d744b4f..23fc3d5 100644
+--- a/src/extlib-abc/aig/dar/darRefact.c
++++ b/src/extlib-abc/aig/dar/darRefact.c
+@@ -340,6 +340,7 @@ printf( "\n" );
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required )

+ {

+     Vec_Ptr_t * vCut;

+@@ -428,6 +429,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
+     }

+     return p->GainBest;

+ }

++#endif

+ 

+ /**Function*************************************************************

+ 

+@@ -461,6 +463,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
+   SeeAlso     []

+  

+ ***********************************************************************/

++#if 0

+ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )

+ {

+ //    Bar_Progress_t * pProgress;

+@@ -583,6 +586,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
+     return 1;

+ 

+ }

++#endif

+ 

+ ////////////////////////////////////////////////////////////////////////

+ ///                       END OF FILE                                ///

+diff --git a/src/extlib-abc/aig/dar/darScript.c b/src/extlib-abc/aig/dar/darScript.c
+index e60df00..1b9c24f 100644
+--- a/src/extlib-abc/aig/dar/darScript.c
++++ b/src/extlib-abc/aig/dar/darScript.c
+@@ -64,6 +64,7 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )

+ //alias rwsat       "st; rw -l; b -l; rw -l; rf -l"

+ {

+@@ -108,7 +109,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
+ 

+     return pAig;

+ }

+-

++#endif

+ 

+ /**Function*************************************************************

+ 

+@@ -121,6 +122,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )

+ //alias compress2   "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"

+ {

+@@ -180,6 +182,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
+ 

+     return pAig;

+ }

++#endif

+ 

+ /**Function*************************************************************

+ 

+@@ -192,6 +195,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )

+ //alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"

+ {

+@@ -285,6 +289,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
+     }

+     return pAig;

+ }

++#endif

+ 

+ /**Function*************************************************************

+ 

+@@ -297,6 +302,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )

+ //alias resyn    "b; rw; rwz; b; rwz; b"

+ //alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"

+@@ -311,6 +317,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
+     Vec_PtrPush( vAigs, pAig );

+     return vAigs;

+ }

++#endif

+ 

+ /**Function*************************************************************

+ 

+diff --git a/src/extlib-abc/aig/kit/kitAig.c b/src/extlib-abc/aig/kit/kitAig.c
+index de301f2..7e5df0f 100644
+--- a/src/extlib-abc/aig/kit/kitAig.c
++++ b/src/extlib-abc/aig/kit/kitAig.c
+@@ -95,6 +95,7 @@ Aig_Obj_t * Kit_GraphToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, Kit_Graph_t
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * pTruth, int nVars, Vec_Int_t * vMemory )

+ {

+     Aig_Obj_t * pObj;

+@@ -113,6 +114,7 @@ Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * p
+     Kit_GraphFree( pGraph );

+     return pObj;

+ }

++#endif

+ 

+ ////////////////////////////////////////////////////////////////////////

+ ///                       END OF FILE                                ///

+diff --git a/src/extlib-abc/aig/kit/kitGraph.c b/src/extlib-abc/aig/kit/kitGraph.c
+index 39ef587..0485c66 100644
+--- a/src/extlib-abc/aig/kit/kitGraph.c
++++ b/src/extlib-abc/aig/kit/kitGraph.c
+@@ -349,6 +349,7 @@ unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph )
+   SeeAlso     []

+ 

+ ***********************************************************************/

++#if 0

+ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory )

+ {

+     Kit_Graph_t * pGraph;

+@@ -365,6 +366,7 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
+     pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );

+     return pGraph;

+ }

++#endif

+ 

+ /**Function*************************************************************

+ 

diff --git a/pkgs/applications/science/logic/tptp/default.nix b/pkgs/applications/science/logic/tptp/default.nix
index 5c8cb7203245..ef00b135c271 100644
--- a/pkgs/applications/science/logic/tptp/default.nix
+++ b/pkgs/applications/science/logic/tptp/default.nix
@@ -11,15 +11,19 @@ let
     (builtins.attrNames (builtins.removeAttrs x helperArgNames));
   sourceInfo = rec {
     baseName="TPTP";
-    version="5.4.0";
+    version="6.0.0";
     name="${baseName}-${version}";
-    url="http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v${version}.tgz";
-    hash="0rvrmh3vw4bk7mj29bx1pi76g2bsqyc13gsnpa1cbjs5pzyhm780";
+    urls=
+    [
+    "http://www.cs.miami.edu/~tptp/TPTP/Distribution/TPTP-v${version}.tgz"
+    "http://www.cs.miami.edu/~tptp/TPTP/Archive/TPTP-v${version}/TPTP-v${version}.tgz"
+    ];
+    hash="0jnjkqdz937c7mkxvh9wc3byw5h1k19jss058fbzdxxc2hkwq1af";
   };
 in
 rec {
   src = a.fetchurl {
-    url = sourceInfo.url;
+    urls = sourceInfo.urls;
     sha256 = sourceInfo.hash;
   };
 
@@ -74,8 +78,7 @@ rec {
     # A GiB of data. Installation is unpacking and editing a few files.
     # No sense in letting Hydra build it.
     # Also, it is unclear what is covered by "verbatim" - we will edit configs
-    platforms = with a.lib.platforms;
-      [];
+    hydraPlatforms = [];
     license = "verbatim-redistribution";
   };
   passthru = {
diff --git a/pkgs/applications/science/logic/twelf/default.nix b/pkgs/applications/science/logic/twelf/default.nix
new file mode 100644
index 000000000000..c6c7e4d9c1a7
--- /dev/null
+++ b/pkgs/applications/science/logic/twelf/default.nix
@@ -0,0 +1,46 @@
+{ stdenv, fetchurl, pkgconfig, smlnj, rsync }:
+
+stdenv.mkDerivation rec {
+  name = "twelf-${version}";
+  version = "1.7.1";
+
+  src = fetchurl {
+    url = "http://twelf.plparty.org/releases/twelf-src-${version}.tar.gz";
+    sha256 = "0fi1kbs9hrdrm1x4k13angpjasxlyd1gc3ys8ah54i75qbcd9c4i";
+  };
+
+  buildInputs = [ pkgconfig smlnj rsync ];
+
+  buildPhase = ''
+    export SMLNJ_HOME=${smlnj}
+    make smlnj
+  '';
+
+  installPhase = ''
+    mkdir -p $out/bin
+    rsync -av bin/* $out/bin/
+
+    mkdir -p $out/share/emacs/site-lisp/twelf/
+    rsync -av emacs/ $out/share/emacs/site-lisp/twelf/
+
+    mkdir -p $out/share/twelf/examples
+    rsync -av examples/ $out/share/twelf/examples/
+    mkdir -p $out/share/twelf/vim
+    rsync -av vim/ $out/share/twelf/vim/
+  '';
+
+  meta = {
+    description = "Twelf logic proof assistant";
+    longDescription = ''
+      Twelf is a language used to specify, implement, and prove properties of
+      deductive systems such as programming languages and logics. Large
+      research projects using Twelf include the TALT typed assembly language,
+      a foundational proof-carrying-code system, and a type safety proof for
+      Standard ML.
+    '';
+    homepage = http://twelf.org/wiki/Main_Page;
+    license = "MIT";
+    maintainers = with stdenv.lib.maintainers; [ jwiegley ];
+    platforms = stdenv.lib.platforms.unix;
+  };
+}
diff --git a/pkgs/applications/science/logic/verifast/default.nix b/pkgs/applications/science/logic/verifast/default.nix
new file mode 100644
index 000000000000..7ab08cf8799f
--- /dev/null
+++ b/pkgs/applications/science/logic/verifast/default.nix
@@ -0,0 +1,43 @@
+{ stdenv, fetchurl, gtk, gdk_pixbuf, atk, pango, glib, cairo, freetype
+, fontconfig, libxml2, gnome2 }:
+
+let
+  libPath = stdenv.lib.makeLibraryPath
+    [ stdenv.gcc.libc stdenv.gcc.gcc gtk gdk_pixbuf atk pango glib cairo
+      freetype fontconfig libxml2 gnome2.gtksourceview
+    ] + ":${stdenv.gcc.gcc}/lib64";
+
+  patchExe = x: ''
+    patchelf --interpreter "$(cat $NIX_GCC/nix-support/dynamic-linker)" \
+      --set-rpath ${libPath} ${x}
+  '';
+in
+stdenv.mkDerivation rec {
+  name    = "verifast-${version}";
+  version = "14.5";
+
+  src = fetchurl {
+    url    = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/${name}-x64.tar.gz";
+    sha256 = "03y1s6s2j9vqgiad0vbxriipsypxaylxxd3q36n9rvrc3lf9xra9";
+  };
+
+  dontStrip = true;
+  phases = "unpackPhase installPhase";
+  installPhase = ''
+    mkdir -p $out/bin
+    cp -R bin $out/libexec
+
+    ${patchExe "$out/libexec/verifast-core"}
+    ${patchExe "$out/libexec/vfide-core"}
+    ln -s $out/libexec/verifast-core $out/bin/verifast
+    ln -s $out/libexec/vfide-core    $out/bin/vfide
+  '';
+
+  meta = {
+    description = "Verification for C and Java programs via separation logic";
+    homepage    = "http://people.cs.kuleuven.be/~bart.jacobs/verifast/";
+    license     = stdenv.lib.licenses.msrla;
+    platforms   = [ "x86_64-linux" ];
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
new file mode 100644
index 000000000000..71ff1cc7fb47
--- /dev/null
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -0,0 +1,22 @@
+{ fetchurl, stdenv, ocaml, ocamlPackages, coq }:
+
+stdenv.mkDerivation rec {
+  name    = "why3-${version}";
+  version = "0.83";
+
+  src = fetchurl {
+    url    = "https://gforge.inria.fr/frs/download.php/33490/${name}.tar.gz";
+    sha256 = "1jcs5vj91ppbgh4q4hch89b63wgakjhg35pm3r4jwhp377lnggya";
+  };
+
+  buildInputs = with ocamlPackages;
+    [ coq ocaml findlib lablgtk ocamlgraph zarith ];
+
+  meta = {
+    description = "why is a software verification platform";
+    homepage    = "http://why3.lri.fr/";
+    license     = stdenv.lib.licenses.lgpl21;
+    platforms   = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/yices/default.nix b/pkgs/applications/science/logic/yices/default.nix
new file mode 100644
index 000000000000..5a1a4ef19922
--- /dev/null
+++ b/pkgs/applications/science/logic/yices/default.nix
@@ -0,0 +1,40 @@
+{ stdenv, fetchurl }:
+
+let
+  libPath = stdenv.lib.makeLibraryPath [ stdenv.gcc.libc ];
+in
+stdenv.mkDerivation rec {
+  name    = "yices-${version}";
+  version = "2.2.1";
+
+  src =
+    if stdenv.system == "i686-linux"
+    then fetchurl {
+      url = "http://yices.csl.sri.com/cgi-bin/yices2-newdownload.cgi?file=yices-2.2.1-i686-pc-linux-gnu-static-gmp.tar.gz&accept=I+accept";
+      name = "yices-${version}-i686.tar.gz";
+      sha256 = "12jzk3kqlbqa5x6rl92cpzj7dch7gm7fnbj72wifvwgdj4zyhrra";
+    }
+    else fetchurl {
+      url = "http://yices.csl.sri.com/cgi-bin/yices2-newdownload.cgi?file=yices-2.2.1-x86_64-unknown-linux-gnu-static-gmp.tar.gz&accept=I+accept";
+      name = "yices-${version}-x86_64.tar.gz";
+      sha256 = "0fpmihf6ykcg4qbsimkamgcwp4sl1xyxmz7q28ily91rd905ijaj";
+    };
+
+  buildPhase = false;
+  installPhase = ''
+    mkdir -p $out/bin $out/lib $out/include
+    cd bin     && mv * $out/bin     && cd ..
+    cd lib     && mv * $out/lib     && cd ..
+    cd include && mv * $out/include && cd ..
+
+    patchelf --set-rpath ${libPath} $out/lib/libyices.so.${version}
+  '';
+
+  meta = {
+    description = "Yices is a high-performance theorem prover and SMT solver";
+    homepage    = "http://yices.csl.sri.com";
+    license     = stdenv.lib.licenses.unfreeRedistributable;
+    platforms   = stdenv.lib.platforms.linux;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/logic/z3/default.nix b/pkgs/applications/science/logic/z3/default.nix
new file mode 100644
index 000000000000..7a87cb5e8be0
--- /dev/null
+++ b/pkgs/applications/science/logic/z3/default.nix
@@ -0,0 +1,46 @@
+{ stdenv, fetchurl, python, unzip, autoreconfHook }:
+
+stdenv.mkDerivation rec {
+  name = "z3-${version}";
+  version = "4.3.1";
+  src = fetchurl {
+    url    = "http://download-codeplex.sec.s-msft.com/Download/SourceControlFileDownload.ashx\?ProjectName\=z3\&changeSetId\=89c1785b73225a1b363c0e485f854613121b70a7";
+    name   = "${name}.zip";
+    sha256 = "3b94465c52ec174350d8707dd6a1fb0cef42f0fa23f148cc1808c14f3c2c7f76";
+  };
+
+  buildInputs = [ python unzip autoreconfHook ];
+  enableParallelBuilding = true;
+
+  # The zip file doesn't unpack a directory, just the code itself.
+  unpackPhase = "mkdir ${name} && cd ${name} && unzip $src";
+  postConfigure = ''
+    python scripts/mk_make.py
+    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/z3_api.h    $out/include
+    cp ../src/api/z3_v1.h     $out/include
+    cp ../src/api/z3_macros.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
+  '';
+
+  meta = {
+    description = "Z3 is a high-performance theorem prover and SMT solver";
+    homepage    = "http://z3.codeplex.com";
+    license     = stdenv.lib.licenses.msrla;
+    platforms   = stdenv.lib.platforms.unix;
+    maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/pkgs/applications/science/math/R/default.nix b/pkgs/applications/science/math/R/default.nix
index 6c8ec9e68c53..edba65146a66 100644
--- a/pkgs/applications/science/math/R/default.nix
+++ b/pkgs/applications/science/math/R/default.nix
@@ -2,14 +2,15 @@
 , libjpeg, libpng, libtiff, ncurses, pango, pcre, perl, readline, tcl
 , texLive, tk, xz, zlib, less, texinfo, graphviz, icu, pkgconfig, bison
 , imake, which, jdk, atlas
+, withRecommendedPackages ? true
 }:
 
 stdenv.mkDerivation rec {
-  name = "R-3.0.2";
+  name = "R-3.1.0";
 
   src = fetchurl {
     url = "http://cran.r-project.org/src/base/R-3/${name}.tar.gz";
-    sha256 = "0jq2vk6bgksbvgmdjvv7vfj6llp091d0nhl5j825aya4c2nhavlm";
+    sha256 = "1qjzbw341bvi1h4jwbvdkvq8j0z9l3m85mpgrlfw0n2cz2806s4a";
   };
 
   buildInputs = [ blas bzip2 gfortran liblapack libX11 libXmu libXt
@@ -23,6 +24,7 @@ stdenv.mkDerivation rec {
   preConfigure = ''
     configureFlagsArray=(
       --disable-lto
+      --with${stdenv.lib.optionalString (!withRecommendedPackages) "out"}-recommended-packages
       --with-blas="-L${atlas}/lib -lf77blas -latlas"
       --with-lapack="-L${liblapack}/lib -llapack"
       --with-readline
@@ -36,6 +38,7 @@ stdenv.mkDerivation rec {
       --with-system-pcre
       --with-system-xz
       --with-ICU
+      --enable-R-shlib
       AR=$(type -p ar)
       AWK=$(type -p gawk)
       CC=$(type -p gcc)
@@ -81,7 +84,7 @@ stdenv.mkDerivation rec {
       user-defined recursive functions and input and output facilities.
     '';
 
-    platforms = stdenv.lib.platforms.linux;
+    hydraPlatforms = stdenv.lib.platforms.linux;
     maintainers = [ stdenv.lib.maintainers.simons ];
   };
 }
diff --git a/pkgs/applications/science/math/content/default.nix b/pkgs/applications/science/math/content/default.nix
index 87c047c29957..177efd667a39 100644
--- a/pkgs/applications/science/math/content/default.nix
+++ b/pkgs/applications/science/math/content/default.nix
@@ -93,5 +93,6 @@ rec {
       a.lib.maintainers.raskin
     ];
     platforms = a.lib.platforms.linux;
+    broken = true;
   };
 }
diff --git a/pkgs/applications/science/math/eukleides/default.nix b/pkgs/applications/science/math/eukleides/default.nix
index 55ea4c6216c6..fdf5c1bd8315 100644
--- a/pkgs/applications/science/math/eukleides/default.nix
+++ b/pkgs/applications/science/math/eukleides/default.nix
@@ -20,7 +20,7 @@ stdenv.mkDerivation {
   meta = {
     description = "Geometry Drawing Language";
     homepage = "http://www.eukleides.org/";
-    license = "GPLv2";
+    license = stdenv.lib.licenses.gpl2;
 
     longDescription = ''
       Eukleides is a computer language devoted to elementary plane
diff --git a/pkgs/applications/science/math/fricas/default.nix b/pkgs/applications/science/math/fricas/default.nix
new file mode 100644
index 000000000000..1817c43ed7be
--- /dev/null
+++ b/pkgs/applications/science/math/fricas/default.nix
@@ -0,0 +1,23 @@
+{ stdenv, fetchurl, sbcl, libX11, libXpm, libICE, libSM, libXt, libXau, libXdmcp }:
+
+stdenv.mkDerivation rec {
+  name = "fricas-1.2.2";
+
+  src = fetchurl {
+    url    = "http://sourceforge.net/projects/fricas/files/fricas/1.2.2/${name}-full.tar.bz2";
+    sha256 = "87db64a1fd4211f3b776793acea931b4271d2e7a28396414c7d7397d833defe1";
+  };
+
+  buildInputs = [ sbcl libX11 libXpm libICE libSM libXt libXau libXdmcp ];
+
+  dontStrip = true;
+
+  meta = {
+    homepage = http://fricas.sourceforge.net/;
+    description = "Fricas CAS";
+    license = stdenv.lib.licenses.bsd3;
+
+    hydraPlatforms = stdenv.lib.platforms.linux;
+    maintainers = stdenv.lib.maintainers.sprock;
+  };
+}
diff --git a/pkgs/applications/science/math/gap/default.nix b/pkgs/applications/science/math/gap/default.nix
index f76640567f60..0700251c3a82 100644
--- a/pkgs/applications/science/math/gap/default.nix
+++ b/pkgs/applications/science/math/gap/default.nix
@@ -1,10 +1,10 @@
 x@{builderDefsPackage
-  , pari ? null 
+  , pari ? null
   , ...}:
 builderDefsPackage
-(a :  
-let 
-  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+(a :
+let
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
     [];
 
   buildInputs = map (n: builtins.getAttr n x)
@@ -38,20 +38,20 @@ rec {
   phaseNames = ["doConfigure" "doMake" "doDeploy"];
 
   doDeploy = a.fullDepEntry ''
-    ensureDir "$out/bin" "$out/share/gap/"
+    mkdir -p "$out/bin" "$out/share/gap/"
 
     cp -r . "$out/share/gap/build-dir"
 
     tar xf "${pkgSrc}" -C "$out/share/gap/build-dir/pkg"
 
-    ${if a.pari != null then 
-      ''sed -e '2iexport PATH=$PATH:${pari}/bin' -i "$out/share/gap/build-dir/bin/gap.sh" '' 
+    ${if a.pari != null then
+      ''sed -e '2iexport PATH=$PATH:${pari}/bin' -i "$out/share/gap/build-dir/bin/gap.sh" ''
     else ""}
-    sed -e "/GAP_DIR=/aGAP_DIR='$out/share/gap/build-dir/'" -i "$out/share/gap/build-dir/bin/gap.sh" 
+    sed -e "/GAP_DIR=/aGAP_DIR='$out/share/gap/build-dir/'" -i "$out/share/gap/build-dir/bin/gap.sh"
 
     ln -s "$out/share/gap/build-dir/bin/gap.sh" "$out/bin"
   '' ["doMake" "minInit" "defEnsureDir"];
-      
+
   meta = {
     description = "Computational discrete algebra system";
     maintainers = with a.lib.maintainers;
@@ -60,8 +60,8 @@ rec {
     ];
     platforms = with a.lib.platforms;
       linux;
-    license = "GPLv2";
+    license = with a.lib.licenses;
+      gpl2;
     homepage = "http://gap-system.org/";
   };
 }) x
-
diff --git a/pkgs/applications/science/math/glsurf/default.nix b/pkgs/applications/science/math/glsurf/default.nix
index a056a32c64c2..c4352c46f92e 100644
--- a/pkgs/applications/science/math/glsurf/default.nix
+++ b/pkgs/applications/science/math/glsurf/default.nix
@@ -9,7 +9,7 @@ stdenv.mkDerivation {
 
   src = fetchdarcs {
     url = "http://lama.univ-savoie.fr/~raffalli/GlSurf";
-    tag = "3.3";
+    rev = "3.3";
     sha256 = ""; md5="";
   };
 
diff --git a/pkgs/applications/science/math/jags/default.nix b/pkgs/applications/science/math/jags/default.nix
index 3043df15da74..a93386149bd4 100644
--- a/pkgs/applications/science/math/jags/default.nix
+++ b/pkgs/applications/science/math/jags/default.nix
@@ -1,10 +1,10 @@
 {stdenv, fetchurl, gfortran, liblapack, blas}:
 
 stdenv.mkDerivation rec {
-  name = "JAGS-2.2.0";
+  name = "JAGS-3.4.0";
   src = fetchurl {
     url = "mirror://sourceforge/mcmc-jags/${name}.tar.gz";
-    sha256 = "016xml4k99lmdwwjiabxin95k9p3q2zh4pcci8wwcqwlq5y205b6";
+    sha256 = "0ayqsz9kkmbss7mxlwr34ch2z1vsb65lryjzqpprab1ccyiaksib";
   };
   buildInputs = [gfortran liblapack blas];
 
diff --git a/pkgs/applications/science/math/mathematica/default.nix b/pkgs/applications/science/math/mathematica/default.nix
index cedb491cc8b9..d4d352c95bbb 100644
--- a/pkgs/applications/science/math/mathematica/default.nix
+++ b/pkgs/applications/science/math/mathematica/default.nix
@@ -18,10 +18,8 @@
 
 let
   platform =
-    if stdenv.system == "i686-linux" then
+    if stdenv.system == "i686-linux" || stdenv.system == "x86_64-linux" then
       "Linux"
-    else if stdenv.system == "x86_64-linux" then
-      "Linux-x86-64"
     else
       throw "Mathematica requires i686-linux or x86_64 linux";
 in
@@ -121,6 +119,6 @@ stdenv.mkDerivation rec {
   meta = {
     description = "Wolfram Mathematica computational software system";
     homepage = "http://www.wolfram.com/mathematica/";
-    license = "unfree";
+    license = stdenv.lib.licenses.unfree;
   };
 }
diff --git a/pkgs/applications/science/math/maxima/default.nix b/pkgs/applications/science/math/maxima/default.nix
index b8f7f2e65b66..096796a859d0 100644
--- a/pkgs/applications/science/math/maxima/default.nix
+++ b/pkgs/applications/science/math/maxima/default.nix
@@ -2,7 +2,7 @@
 
 let
   name    = "maxima";
-  version = "5.31.2";
+  version = "5.33.0";
 
   searchPath =
     stdenv.lib.makeSearchPath "bin"
@@ -13,7 +13,7 @@ stdenv.mkDerivation {
 
   src = fetchurl {
     url = "mirror://sourceforge/${name}/${name}-${version}.tar.gz";
-    sha256 = "12j5irwfckl5583h7lwh0wrp0c65q7mqzcsri2v086j50xvvv398";
+    sha256 = "13axm11xw0f3frx5b0qdidi7igkn1524fzz77s9rbpl2yy2nrbz2";
   };
 
   buildInputs = [sbcl texinfo perl makeWrapper];
@@ -40,7 +40,7 @@ stdenv.mkDerivation {
   meta = {
     description = "Maxima computer algebra system";
     homepage = "http://maxima.sourceforge.net";
-    license = "GPLv2";
+    license = stdenv.lib.licenses.gpl2;
 
     longDescription = ''
       Maxima is a fairly complete computer algebra system written in
diff --git a/pkgs/applications/science/math/pari/default.nix b/pkgs/applications/science/math/pari/default.nix
index 5fda04fed4f3..576a28b054f4 100644
--- a/pkgs/applications/science/math/pari/default.nix
+++ b/pkgs/applications/science/math/pari/default.nix
@@ -1,11 +1,11 @@
 { stdenv, fetchurl, gmp, readline }:
 
 stdenv.mkDerivation rec {
-  name = "pari-2.5.4";
+  name = "pari-2.5.5";
 
   src = fetchurl {
     url = "http://pari.math.u-bordeaux.fr/pub/pari/unix/${name}.tar.gz";
-    sha256 = "0gpsj5n8d1gyl7nq2y915sscs3d334ryrv8qgjdwqf3cr95f2dwz";
+    sha256 = "058nw1fhggy7idii4f124ami521lv3izvngs9idfz964aks8cvvn";
   };
 
   buildInputs = [gmp readline];
diff --git a/pkgs/applications/science/math/pssp/default.nix b/pkgs/applications/science/math/pssp/default.nix
index 587f41fe998b..0a9e0e4735d0 100644
--- a/pkgs/applications/science/math/pssp/default.nix
+++ b/pkgs/applications/science/math/pssp/default.nix
@@ -3,11 +3,11 @@
 }:
 
 stdenv.mkDerivation rec {
-  name = "pspp-0.8.1";
+  name = "pspp-0.8.2";
 
   src = fetchurl {
     url = "mirror://gnu/pspp/${name}.tar.gz";
-    sha256 = "0qhxsdbwxd3cn1shc13wxvx2lg32lp4z6sz24kv3jz7p5xfi8j7x";
+    sha256 = "1w7h3dglgx0jlq1wb605b8pgfsk2vr1q2q2rj7bsajh9ihbcsixr";
   };
 
   buildInputs = [ libxml2 readline zlib perl cairo gtk gsl pkgconfig
diff --git a/pkgs/applications/science/math/sage/default.nix b/pkgs/applications/science/math/sage/default.nix
new file mode 100644
index 000000000000..ced8b6f95bb6
--- /dev/null
+++ b/pkgs/applications/science/math/sage/default.nix
@@ -0,0 +1,31 @@
+{ stdenv, fetchurl, m4, perl, gfortran, texLive, ffmpeg, tk
+, imagemagick, liblapack
+}:
+
+stdenv.mkDerivation rec {
+  name = "sage-6.1.1";
+
+  src = fetchurl {
+    url = "http://mirrors.xmission.com/sage/src/sage-6.1.1.tar.gz";
+    sha256 = "0kbzs0l9q7y34jv3f8rd1c2mrjsjkdgaw6mfdwjlpg9g4gghmq5y";
+  };
+
+  buildInputs = [ m4 perl gfortran texLive ffmpeg tk imagemagick liblapack ];
+
+  enableParallelBuilding = true;
+
+  preConfigure = ''
+    export SAGE_NUM_THREADS=$NIX_BUILD_CORES
+    sed -i 's/if ! [ -d "$HOME" ]/if [ -d "$HOME" ]/' src/bin/sage-env
+  '' + stdenv.lib.optionalString stdenv.isDarwin ''
+    sed -i "s/ld_version = try_run('ld  -v')/ld_version = 'Apple'/" \
+      build/pkgs/atlas/configuration.py
+  '';
+
+  meta = {
+    homepage = http://www.scilab.org/;
+    description = "Scientific software package for numerical computations (Matlab lookalike)";
+    # see http://www.scilab.org/legal
+    license = "SciLab";
+  };
+}
diff --git a/pkgs/applications/science/math/singular/default.nix b/pkgs/applications/science/math/singular/default.nix
index 5c5dfae8200f..1afb510e9948 100644
--- a/pkgs/applications/science/math/singular/default.nix
+++ b/pkgs/applications/science/math/singular/default.nix
@@ -3,9 +3,9 @@ x@{builderDefsPackage
   , coreutils
   , ...}:
 builderDefsPackage
-(a :  
-let 
-  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++ 
+(a :
+let
+  helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
     [];
 
   buildInputs = map (n: builtins.getAttr n x)
@@ -38,9 +38,9 @@ rec {
     rm -rf "$out/LIB"
     cp -r Singular/LIB "$out"
     mkdir -p "$out/bin"
-    ln -s "$out"/*/Singular "$out/bin"
+    ln -s "$out/"*/Singular "$out/bin"
   '') ["minInit" "defEnsureDir"];
-      
+
   meta = {
     description = "A CAS for polynomial computations";
     maintainers = with a.lib.maintainers;
@@ -49,7 +49,7 @@ rec {
     ];
     platforms = with a.lib.platforms;
       linux;
-    license = "GPLv3"; # Or GPLv2 at your option - but not GPLv4
+    license = a.stdenv.lib.licenses.gpl3; # Or GPLv2 at your option - but not GPLv4
     homepage = "http://www.singular.uni-kl.de/index.php";
   };
   passthru = {
@@ -58,4 +58,3 @@ rec {
     };
   };
 }) x
-
diff --git a/pkgs/applications/science/math/sloane/default.nix b/pkgs/applications/science/math/sloane/default.nix
new file mode 100644
index 000000000000..b3bde7874cab
--- /dev/null
+++ b/pkgs/applications/science/math/sloane/default.nix
@@ -0,0 +1,28 @@
+# This file was auto-generated by cabal2nix. Please do NOT edit manually!
+
+{ cabal, ansiTerminal, cereal, downloadCurl, filepath, HTTP
+, network, optparseApplicative, terminalSize, text, zlib
+}:
+
+cabal.mkDerivation (self: {
+  pname = "sloane";
+  version = "1.9.1";
+  sha256 = "0scnvir7il8ldy3g846xmrdkk2rxnlsiyqak0jvcarf2qi251x5i";
+  isLibrary = false;
+  isExecutable = true;
+  buildDepends = [
+    ansiTerminal cereal downloadCurl filepath HTTP network
+    optparseApplicative terminalSize text zlib
+  ];
+  postInstall = ''
+    mkdir -p $out/share/man/man1
+    cp sloane.1 $out/share/man/man1/
+  '';
+  meta = {
+    homepage = "http://github.com/akc/sloane";
+    description = "A command line interface to Sloane's On-Line Encyclopedia of Integer Sequences";
+    license = self.stdenv.lib.licenses.bsd3;
+    platforms = self.ghc.meta.platforms;
+    maintainers = [ self.stdenv.lib.maintainers.akc ];
+  };
+})
diff --git a/pkgs/applications/science/math/weka/default.nix b/pkgs/applications/science/math/weka/default.nix
index 8471c46c8d75..66609fa58341 100644
--- a/pkgs/applications/science/math/weka/default.nix
+++ b/pkgs/applications/science/math/weka/default.nix
@@ -27,6 +27,6 @@ stdenv.mkDerivation {
   meta = {
     homepage = "http://www.cs.waikato.ac.nz/ml/weka/";
     description = "Collection of machine learning algorithms for data mining tasks";
-    license = "GPLv2+";
+    license = stdenv.lib.licenses.gpl2Plus;
   };
 }
diff --git a/pkgs/applications/science/math/wxmaxima/default.nix b/pkgs/applications/science/math/wxmaxima/default.nix
index 01be4ba7e6c6..75448b6965cd 100644
--- a/pkgs/applications/science/math/wxmaxima/default.nix
+++ b/pkgs/applications/science/math/wxmaxima/default.nix
@@ -27,7 +27,7 @@ stdenv.mkDerivation {
 
   meta = {
     description = "Cross platform GUI for the computer algebra system Maxima";
-    license = "GPL2";
+    license = stdenv.lib.licenses.gpl2;
     homepage = http://wxmaxima.sourceforge.net;
     platforms = stdenv.lib.platforms.linux;
     maintainers = [ stdenv.lib.maintainers.simons ];
diff --git a/pkgs/applications/science/math/yacas/default.nix b/pkgs/applications/science/math/yacas/default.nix
index acc4740eb6b4..2c9d63be1b4d 100644
--- a/pkgs/applications/science/math/yacas/default.nix
+++ b/pkgs/applications/science/math/yacas/default.nix
@@ -35,7 +35,7 @@ stdenv.mkDerivation rec {
   meta = { 
       description = "Easy to use, general purpose Computer Algebra System";
       homepage = http://yacas.sourceforge.net/;
-      license = "GPLv2+";
+      license = stdenv.lib.licenses.gpl2Plus;
       maintainers = with stdenv.lib.maintainers; [viric];
       platforms = with stdenv.lib.platforms; all;
   };
diff --git a/pkgs/applications/science/misc/boinc/default.nix b/pkgs/applications/science/misc/boinc/default.nix
index 0bc5c3cb7c7c..7020de0bca88 100644
--- a/pkgs/applications/science/misc/boinc/default.nix
+++ b/pkgs/applications/science/misc/boinc/default.nix
@@ -3,12 +3,12 @@ mesa, libXmu, libXi, freeglut, libjpeg, libtool, wxGTK, xcbutil,
 sqlite, gtk, patchelf, libXScrnSaver, libnotify, libX11, libxcb }:
 
 stdenv.mkDerivation rec {
-  name = "boinc-7.0.44";
+  name = "boinc-7.2.42";
 
   src = fetchgit {
     url = "git://boinc.berkeley.edu/boinc-v2.git";
-    rev = "7c449b1fb8a681ceb27d6895751b62a2b3adf0f2";
-    sha256 = "0hdramyl9nip3gadp7xiaz8ngyld15i93d8ai1nsd04bmrvdfqia";
+    rev = "dd0d630882547c123ca0f8fda7a62e058d60f6a9";
+    sha256 = "1zifpi3mjgaj68fba6kammp3x7z8n2x164zz6fj91xfiapnan56j";
   };
 
   buildInputs = [ libtool automake autoconf m4 pkgconfig curl mesa libXmu libXi
@@ -36,7 +36,7 @@ stdenv.mkDerivation rec {
 
     homepage = http://boinc.berkeley.edu/;
 
-    license = "LGPLv2+";
+    license = stdenv.lib.licenses.lgpl2Plus;
 
     platforms = stdenv.lib.platforms.linux;  # arbitrary choice
   };
diff --git a/pkgs/applications/science/misc/fityk/default.nix b/pkgs/applications/science/misc/fityk/default.nix
new file mode 100644
index 000000000000..db79839ba669
--- /dev/null
+++ b/pkgs/applications/science/misc/fityk/default.nix
@@ -0,0 +1,23 @@
+{ stdenv, fetchurl, wxGTK30, boost, lua, zlib, bzip2, xylib, readline, gnuplot }:
+
+let
+  name    = "fityk";
+  version = "1.2.9";
+in
+stdenv.mkDerivation {
+  name = "${name}-${version}";
+
+  src = fetchurl {
+    url = "https://github.com/wojdyr/fityk/releases/download/v${version}/${name}-${version}.tar.bz2";
+    sha256 = "1gl938nd2jyya8b3gzbagm1jab2mkc9zvr6zsg5d0vkfdqlk0pv1";
+  };
+
+  buildInputs = [wxGTK30 boost lua zlib bzip2 xylib readline gnuplot ];
+
+  meta = {
+    description = "Fityk -- curve fitting and peak fitting software";
+    license = "GPL2";
+    homepage = http://fityk.nieto.pl/;
+    platforms = stdenv.lib.platforms.linux;
+  };
+}
diff --git a/pkgs/applications/science/misc/golly/default.nix b/pkgs/applications/science/misc/golly/default.nix
index a380f05b0915..9d198cd5c7f8 100644
--- a/pkgs/applications/science/misc/golly/default.nix
+++ b/pkgs/applications/science/misc/golly/default.nix
@@ -1,11 +1,11 @@
-x@{builderDefsPackage, 
+x@{builderDefsPackage,
   wxGTK, perl, python, zlib
   , ...}:
 builderDefsPackage
-(a :  
-let 
+(a :
+let
   s = import ./src-for-default.nix;
-  helperArgNames = ["builderDefsPackage"] ++ 
+  helperArgNames = ["builderDefsPackage"] ++
     [];
   buildInputs = map (n: builtins.getAttr n x)
     (builtins.attrNames (builtins.removeAttrs x helperArgNames));
@@ -26,7 +26,7 @@ rec {
     export NIX_LDFLAGS="$NIX_LDFLAGS -l$pythonLib"
     echo "Flags: $NIX_LDFLAGS"
   '';
-      
+
   meta = {
     description = "Cellular automata simulation program";
     maintainers = with a.lib.maintainers;
@@ -35,7 +35,7 @@ rec {
     ];
     platforms = with a.lib.platforms;
       linux;
-    license = "GPLv2";
+    license = with a.lib.licenses;
+      gpl2;
   };
 }) x
-
diff --git a/pkgs/applications/science/misc/megam/default.nix b/pkgs/applications/science/misc/megam/default.nix
new file mode 100644
index 000000000000..a0ee505dc97f
--- /dev/null
+++ b/pkgs/applications/science/misc/megam/default.nix
@@ -0,0 +1,46 @@
+{ fetchurl, stdenv, ocaml, makeWrapper, ncurses }:
+
+let version = "0.92"; in
+stdenv.mkDerivation rec {
+  name = "megam-${version}";
+
+  src = fetchurl {
+    url = "http://hal3.name/megam/megam_src.tgz";
+    sha256 = "dc0e9f59ff8513449fe3bd40b260141f89c88a4edf6ddc8b8a394c758e49724e";
+  };
+
+  patches = [ ./ocaml-includes.patch ./ocaml-3.12.patch ];
+  
+  buildInputs = [ ocaml ncurses ];
+
+  nativeBuildInputs = [ makeWrapper ];
+
+  makeFlags = "CAML_INCLUDES=${ocaml}/lib/ocaml/caml";
+
+  # see https://bugzilla.redhat.com/show_bug.cgi?id=435559
+  dontStrip = true;
+
+  installPhase = ''
+    mkdir -pv $out/bin
+    cp -Rv megam $out/bin
+  '';
+
+
+  meta = {
+    description = "MEGA Model Optimization Package";
+
+    longDescription =
+      ''  The software here is an implementation of maximum likelihood
+          and maximum a posterior optimization of the parameters of
+          these models.  The algorithms used are much more efficient
+          than the iterative scaling techniques used in almost every
+          other maxent package out there.  '';
+
+    homepage = http://www.umiacs.umd.edu/~hal/megam;
+
+    license = "non-commercial";
+
+    maintainers = [ ];
+    platforms = stdenv.lib.platforms.gnu;  # arbitrary choice
+  };
+}
diff --git a/pkgs/applications/science/misc/megam/ocaml-3.12.patch b/pkgs/applications/science/misc/megam/ocaml-3.12.patch
new file mode 100644
index 000000000000..8265acf6e4a7
--- /dev/null
+++ b/pkgs/applications/science/misc/megam/ocaml-3.12.patch
@@ -0,0 +1,12 @@
+diff -ru megam_0.92/Makefile megam_0.92-b/Makefile
+--- megam_0.92/Makefile	2007-10-08 18:06:04.000000000 +0100
++++ megam_0.92-b/Makefile	2013-11-25 10:14:20.000000000 +0000
+@@ -59,7 +59,7 @@
+ 
+ WITHUNIX =unix.cma -cclib -lunix
+ 
+-WITHSTR =str.cma -cclib -lstr
++WITHSTR =str.cma -cclib -lcamlstr
+ 
+ WITHBIGARRAY =bigarray.cma -cclib -lbigarray
+ 
diff --git a/pkgs/applications/science/misc/megam/ocaml-includes.patch b/pkgs/applications/science/misc/megam/ocaml-includes.patch
new file mode 100644
index 000000000000..b3a56643448c
--- /dev/null
+++ b/pkgs/applications/science/misc/megam/ocaml-includes.patch
@@ -0,0 +1,21 @@
+diff -ru megam_0.92/Makefile megam_0.92-b/Makefile
+--- megam_0.92/Makefile	2007-10-08 18:06:04.000000000 +0100
++++ megam_0.92-b/Makefile	2013-11-25 10:14:20.000000000 +0000
+@@ -41,7 +41,7 @@
+ #
+ # The Caml compilers. #
+ # You may fix here the path to access the Caml compiler on your machine
+-CAMLC = ocamlc -g
++CAMLC = ocamlc -g $(WITHCLIBS)
+ CAMLOPT = ocamlopt -unsafe -ccopt -O4 -ccopt -ffast-math -inline 99999 
+ CAMLDEP = ocamldep
+ CAMLLEX = ocamllex
+@@ -70,7 +70,7 @@
+ WITHDBM =dbm.cma -cclib -lmldbm -cclib -lndbm
+ 
+ #WITHCLIBS =-I /usr/lib/ocaml/3.09.2/caml
+-WITHCLIBS =-I /usr/lib/ocaml/caml
++WITHCLIBS =-I $(CAML_INCLUDES) 
+ 
+ ################ End of user's variables #####################
+ 
diff --git a/pkgs/applications/science/misc/root/cmake.patch b/pkgs/applications/science/misc/root/cmake.patch
new file mode 100644
index 000000000000..b6efd7444fe9
--- /dev/null
+++ b/pkgs/applications/science/misc/root/cmake.patch
@@ -0,0 +1,11 @@
+--- cmake/modules/RootBuildOptions.cmake	1969-12-31 20:30:01.000000000 -0330
++++ cmake/modules/RootBuildOptions.cmake	2014-01-10 14:09:29.424937408 -0330
+@@ -149,7 +149,7 @@
+ 
+ #---General Build options----------------------------------------------------------------------
+ # use, i.e. don't skip the full RPATH for the build tree
+-set(CMAKE_SKIP_BUILD_RPATH  FALSE)
++set(CMAKE_SKIP_BUILD_RPATH  TRUE)
+ # when building, don't use the install RPATH already (but later on when installing)
+ set(CMAKE_BUILD_WITH_INSTALL_RPATH FALSE) 
+ # add the automatically determined parts of the RPATH
diff --git a/pkgs/applications/science/misc/root/default.nix b/pkgs/applications/science/misc/root/default.nix
new file mode 100644
index 000000000000..1227e76ac0c5
--- /dev/null
+++ b/pkgs/applications/science/misc/root/default.nix
@@ -0,0 +1,27 @@
+{ stdenv, fetchurl, cmake, mesa, libX11, gfortran, libXpm, libXft, libXext, zlib }:
+
+stdenv.mkDerivation rec {
+  name = "root-${version}";
+  version = "5.34.15";
+
+  src = fetchurl {
+    url = "ftp://root.cern.ch/root/root_v${version}.source.tar.gz";
+    sha256 = "1bkiggcyya39a794d3d2rzzmmkbdymf86hbqhh0l1pl4f38xvp6i";
+  };
+
+  buildInputs = [ cmake gfortran mesa libX11 libXpm libXft libXext zlib ];
+
+  # CMAKE_INSTALL_RPATH_USE_LINK_PATH is set to FALSE in
+  # <rootsrc>/cmake/modules/RootBuildOptions.cmake.
+  # This patch sets it to TRUE.
+  patches = [ ./cmake.patch ];
+  patchFlags = "-p0";
+
+  enableParallelBuilding = true;
+
+  meta = {
+    homepage = "http://root.cern.ch/drupal/";
+    description = "A data analysis framework";
+    platforms = stdenv.lib.platforms.linux;
+  };
+}
diff --git a/pkgs/applications/science/misc/simgrid/default.nix b/pkgs/applications/science/misc/simgrid/default.nix
index 5fdede1abcdf..29a7caf769be 100644
--- a/pkgs/applications/science/misc/simgrid/default.nix
+++ b/pkgs/applications/science/misc/simgrid/default.nix
@@ -1,20 +1,19 @@
-{ fetchurl, stdenv, cmake, perl, ruby }:
+{ fetchurl, stdenv, cmake, perl, ruby, boost, lua5_1, graphviz, libsigcxx
+, libunwind, elfutils
+}:
 
 stdenv.mkDerivation rec {
-  name = "simgrid-3.5";
+  version = "3.11.1";
+  name = "simgrid-${version}";
 
   src = fetchurl {
-    url = "https://gforge.inria.fr/frs/download.php/28017/${name}.tar.gz";
-    sha256 = "1vd4pvrcyii1nfwyca3kpbwshbc965lfpn083zd8rigg6ydchq8y";
+    url = "https://gforge.inria.fr/frs/download.php/33686/${name}.tar.gz";
+    sha256 = "0mkrzxpf42lmn96khfl1791vram67r2nqsgmppd2yil889nyz5kp";
   };
 
-  /* FIXME: Ruby currently disabled because of this:
-
-     Linking C shared library ../src/.libs/libsimgrid.so
-     ld: cannot find -lruby-1.8.7-p72
-
-   */
-  buildInputs = [ cmake perl /* ruby */ ];
+  buildInputs = [ cmake perl ruby boost lua5_1 graphviz libsigcxx libunwind
+    elfutils
+    ];
 
   preConfigure =
     # Make it so that libsimgrid.so will be found when running programs from
@@ -22,8 +21,17 @@ stdenv.mkDerivation rec {
     '' export LD_LIBRARY_PATH="$PWD/src/.libs"
        export cmakeFlags="-Dprefix=$out"
 
-       # Enable tracing.
-       export cmakeFlags="$cmakeFlags -Denable_tracing=on"
+       export NIX_CFLAGS_COMPILE="$NIX_CFLAGS_COMPILE
+         -isystem $(echo "${libsigcxx}/lib/"sigc++*/include)
+	 -isystem $(echo "${libsigcxx}/include"/sigc++* )
+	 "
+       export CMAKE_PREFIX_PATH="$CMAKE_PREFIX_PATH:$(echo "${libsigcxx}/lib/"sigc++*)"
+
+       # Enable more functionality.
+       export cmakeFlags="$cmakeFlags -Denable_tracing=on -Denable_jedule=on
+         -Denable_latency_bound_tracking=on -Denable_lua=on
+	 -Denable_ns3=on -Denable_gtnets=on
+	 "
     '';
 
   makeFlags = "VERBOSE=1";
@@ -45,6 +53,7 @@ stdenv.mkDerivation rec {
   patchPhase =
     '' for i in "src/smpi/"*
        do
+         test -f "$i" &&
          sed -i "$i" -e's|/bin/bash|/bin/sh|g'
        done
 
@@ -71,7 +80,7 @@ stdenv.mkDerivation rec {
 
     homepage = http://simgrid.gforge.inria.fr/;
 
-    license = "LGPLv2+";
+    license = stdenv.lib.licenses.lgpl2Plus;
 
     maintainers = [ ];
     platforms = stdenv.lib.platforms.gnu;  # arbitrary choice
diff --git a/pkgs/applications/science/misc/tulip/default.nix b/pkgs/applications/science/misc/tulip/default.nix
index e58183a4f40b..da6e0cb2805d 100644
--- a/pkgs/applications/science/misc/tulip/default.nix
+++ b/pkgs/applications/science/misc/tulip/default.nix
@@ -30,7 +30,7 @@ stdenv.mkDerivation rec {
 
     homepage = http://tulip.labri.fr/;
 
-    license = "GPLv3+";
+    license = stdenv.lib.licenses.gpl3Plus;
 
     maintainers = [ ];
     platforms = stdenv.lib.platforms.gnu;  # arbitrary choice
diff --git a/pkgs/applications/science/misc/vite/default.nix b/pkgs/applications/science/misc/vite/default.nix
index 4c1cf318b5a2..2e25ff582ee9 100644
--- a/pkgs/applications/science/misc/vite/default.nix
+++ b/pkgs/applications/science/misc/vite/default.nix
@@ -44,5 +44,7 @@ stdenv.mkDerivation {
 
     maintainers = [ stdenv.lib.maintainers.ludo ];
     platforms = stdenv.lib.platforms.gnu;  # arbitrary choice
+
+    broken = true;
   };
 }
diff --git a/pkgs/applications/science/molecular-dynamics/gromacs/default.nix b/pkgs/applications/science/molecular-dynamics/gromacs/default.nix
index de4bb171497c..b9abf7b55b48 100644
--- a/pkgs/applications/science/molecular-dynamics/gromacs/default.nix
+++ b/pkgs/applications/science/molecular-dynamics/gromacs/default.nix
@@ -6,11 +6,11 @@
 
 
 stdenv.mkDerivation {
-  name = "gromacs-4.5.5";
+  name = "gromacs-4.6.5";
 
   src = fetchurl {
-    url = "ftp://ftp.gromacs.org/pub/gromacs/gromacs-4.5.5.tar.gz";
-    md5 = "6a87e7cdfb25d81afa9fea073eb28468";
+    url = "ftp://ftp.gromacs.org/pub/gromacs/gromacs-4.6.5.tar.gz";
+    sha256 = "02ggrplh8fppqib86y3rfk4qm08yddlrb1yjgzl138b3b4qjy957";
   };
 
   buildInputs = [cmake fftw];
diff --git a/pkgs/applications/science/spyder/default.nix b/pkgs/applications/science/spyder/default.nix
index cd2bd4fecf3d..1079a153ca16 100644
--- a/pkgs/applications/science/spyder/default.nix
+++ b/pkgs/applications/science/spyder/default.nix
@@ -8,12 +8,12 @@
 }:
 
 buildPythonPackage rec {
-  name = "spyder-2.1.13.1";
+  name = "spyder-2.2.5";
   namePrefix = "";
 
   src = fetchurl {
     url = "https://spyderlib.googlecode.com/files/${name}.zip";
-    sha256 = "1sg88shvw6k2v5428k13mah4pyqng43856rzr6ypz5qgwn0677ya";
+    sha256 = "1bxc5qs2bqc21s6kxljsfxnmwgrgnyjfr9mkwzg9njpqsran3bp2";
   };
 
   buildInputs = [ unzip ];
@@ -52,6 +52,6 @@ buildPythonPackage rec {
     homepage = https://code.google.com/p/spyderlib/;
     license = licenses.mit;
     platforms = platforms.linux;
-    maintainers = [maintainers.bjornfor];
+    maintainers = [ maintainers.bjornfor ];
   };
 }