2 files changed, 12 insertions, 14 deletions
diff --git a/pkgs/applications/science/logic/why3/default.nix b/pkgs/applications/science/logic/why3/default.nix
index b9bd2172bb1..924ff3fd9fd 100644
--- a/pkgs/applications/science/logic/why3/default.nix
+++ b/pkgs/applications/science/logic/why3/default.nix
@@ -1,45 +1,42 @@
-{ callPackage, fetchurl, fetchpatch, stdenv
+{ callPackage, fetchurl, fetchpatch, lib, stdenv
 , ocamlPackages, coqPackages, rubber, hevea, emacs }:
 
 stdenv.mkDerivation {
   pname = "why3";
-  version = "1.3.1";
+  version = "1.4.0";
 
   src = fetchurl {
-    url = "https://gforge.inria.fr/frs/download.php/file/38291/why3-1.3.1.tar.gz";
-    sha256 = "16zcrc60zz2j3gd3ww93z2z9x2jkxb3kr57y8i5rcgmacy7mw3bv";
+    url = "https://gforge.inria.fr/frs/download.php/file/38425/why3-1.4.0.tar.gz";
+    sha256 = "0lw0cpx347zz9vvwqibmbxgs80fsd16scgk3isscvwxnajpc3rv8";
   };
 
   buildInputs = with ocamlPackages; [
-    ocaml findlib ocamlgraph zarith menhir
-    # Compressed Sessions
+    ocaml findlib ocamlgraph zarith menhir menhirLib
     # Emacs compilation of why3.el
     emacs
     # Documentation
     rubber hevea
     # GUI
-    lablgtk
+    lablgtk3-sourceview3
     # WebIDE
     js_of_ocaml js_of_ocaml-ppx
+    # S-expression output for why3pp
+    ppx_deriving ppx_sexp_conv
     # Coq Support
     coqPackages.coq coqPackages.flocq ocamlPackages.camlp5
   ];
 
-  propagatedBuildInputs = with ocamlPackages; [ camlzip num ];
+  propagatedBuildInputs = with ocamlPackages; [ camlzip num re sexplib ];
 
   enableParallelBuilding = true;
 
-  postPatch = ''
-    substituteInPlace Makefile.in --replace js_of_ocaml.ppx js_of_ocaml-ppx
-  '';
-
   configureFlags = [ "--enable-verbose-make" ];
 
   installTargets = [ "install" "install-lib" ];
 
   passthru.withProvers = callPackage ./with-provers.nix {};
 
-  meta = with stdenv.lib; {
+  meta = with lib; {
     description = "A platform for deductive program verification";
     homepage    = "http://why3.lri.fr/";
     license     = licenses.lgpl21;
diff --git a/pkgs/applications/science/logic/why3/with-provers.nix b/pkgs/applications/science/logic/why3/with-provers.nix
index 3528dbd3a64..d4fdbfd6937 100644
--- a/pkgs/applications/science/logic/why3/with-provers.nix
+++ b/pkgs/applications/science/logic/why3/with-provers.nix
@@ -15,7 +15,8 @@ in stdenv.mkDerivation {
 
   phases = [ "buildPhase" "installPhase" ];
 
-  buildInputs = [ why3 makeWrapper ] ++ provers;
+  nativeBuildInputs = [ makeWrapper ];
+  buildInputs = [ why3 ] ++ provers;
 
   buildPhase = ''
       mkdir -p $out/share/why3/