From 6738033727ca7945f1465ad76492891489e133ce Mon Sep 17 00:00:00 2001
From: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
Date: Wed, 10 Oct 2018 21:03:45 +0200
Subject: [PATCH] alt-ergo: 1.30->2.2.0, ocplib-simplex: 0.3->0.4

---
 lib/licenses.nix                                          | 6 ++++++
 pkgs/applications/science/logic/alt-ergo/default.nix      | 8 ++++----
 pkgs/development/ocaml-modules/ocplib-simplex/default.nix | 8 +++++---
 pkgs/top-level/all-packages.nix                           | 4 +---
 4 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/lib/licenses.nix b/lib/licenses.nix
index c4db280645a..2d4e52ae480 100644
--- a/lib/licenses.nix
+++ b/lib/licenses.nix
@@ -500,6 +500,12 @@ lib.mapAttrs (n: v: v // { shortName = n; }) rec {
     fullName = "Non-Profit Open Software License 3.0";
   };
 
+  ocamlpro_nc = {
+    fullName = "OCamlPro Non Commercial license version 1";
+    url = "https://alt-ergo.ocamlpro.com/http/alt-ergo-2.2.0/OCamlPro-Non-Commercial-License.pdf";
+    free = false;
+  };
+
   ofl = spdx {
     spdxId = "OFL-1.1";
     fullName = "SIL Open Font License 1.1";
diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix
index 8cf4bb9b6d2..794430ebbe8 100644
--- a/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -2,21 +2,21 @@
 
 stdenv.mkDerivation rec {
   name = "alt-ergo-${version}";
-  version = "1.30";
+  version = "2.2.0";
 
   src = fetchurl {
     url    = "https://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
     name   = "${name}.tar.gz";
-    sha256 = "025pacb4ax864fn5x8k78mw6hiig4jcazblj18gzxspg4f1l5n1g";
+    sha256 = "106zfgisq6qxr7dlk8z7gi68ly7qff4frn8wab2g8z2nkkwla92w";
   };
 
   buildInputs = with ocamlPackages;
-    [ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex ];
+    [ ocaml findlib camlzip ocamlgraph zarith lablgtk ocplib-simplex psmt2-frontend menhir num ];
 
   meta = {
     description = "High-performance theorem prover and SMT solver";
     homepage    = "https://alt-ergo.ocamlpro.com/";
-    license     = stdenv.lib.licenses.cecill-c; # LGPL-2 compatible
+    license     = stdenv.lib.licenses.ocamlpro_nc;
     platforms   = stdenv.lib.platforms.linux ++ stdenv.lib.platforms.darwin;
     maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
   };
diff --git a/pkgs/development/ocaml-modules/ocplib-simplex/default.nix b/pkgs/development/ocaml-modules/ocplib-simplex/default.nix
index eb25982a69b..1c09edf3a7e 100644
--- a/pkgs/development/ocaml-modules/ocplib-simplex/default.nix
+++ b/pkgs/development/ocaml-modules/ocplib-simplex/default.nix
@@ -2,7 +2,7 @@
 
 let
   pname = "ocplib-simplex";
-  version = "0.3";
+  version = "0.4";
 in
 
 stdenv.mkDerivation {
@@ -11,13 +11,15 @@ stdenv.mkDerivation {
   src = fetchFromGitHub {
     owner = "OCamlPro-Iguernlala";
     repo = pname;
-    rev = version;
-    sha256 = "1fmz38w2cj9fny4adqqyil59dvndqkr59s7wk2gqs47r72b6sisa";
+    rev = "v${version}";
+    sha256 = "09niyidrjzrj8g1qwx4wgsdf5m6cwrnzg7zsgala36jliic4di60";
   };
 
   nativeBuildInputs = [ autoreconfHook ];
   buildInputs = [ ocaml findlib ];
 
+  installFlags = "LIBDIR=$(OCAMLFIND_DESTDIR)";
+
   createFindlibDestdir = true;
 
   meta = {
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index 6c64ccdc34b..f2b38e80b04 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -21171,9 +21171,7 @@ with pkgs;
     ocamlPackages = ocaml-ng.ocamlPackages_4_05;
   };
 
-  alt-ergo = callPackage ../applications/science/logic/alt-ergo {
-    ocamlPackages = ocaml-ng.ocamlPackages_4_05;
-  };
+  alt-ergo = callPackage ../applications/science/logic/alt-ergo {};
 
   aspino = callPackage ../applications/science/logic/aspino {};