From ccd6b083e7eb220def514ee914b867f1f801f73f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 18 Feb 2022 11:42:57 +0100
Subject: [PATCH] [ci] Fix alt-ergo version (+ psmt2 dependency)

---
 nix/alt-ergo.nix       | 58 ++++++++++++++++++++++++++++++++++++++++++
 nix/pkgs.nix           |  2 ++
 nix/psmt2-frontend.nix | 49 +++++++++++++++++++++++++++++++++++
 3 files changed, 109 insertions(+)
 create mode 100644 nix/alt-ergo.nix
 create mode 100644 nix/psmt2-frontend.nix

diff --git a/nix/alt-ergo.nix b/nix/alt-ergo.nix
new file mode 100644
index 00000000000..2daf514459d
--- /dev/null
+++ b/nix/alt-ergo.nix
@@ -0,0 +1,58 @@
+{ callPackage
+, fetchzip
+, lib
+, stdenv
+, ocaml
+, findlib
+, ocplib-simplex
+, psmt2-frontend
+, lablgtk
+, zarith
+, menhir
+, camlzip
+, num
+, which
+, autoreconfHook
+}:
+
+stdenv.mkDerivation rec {
+  pname = "alt-ergo";
+  version = "2.2.0-free";
+
+  src =
+    fetchzip {
+      url = "https://alt-ergo.ocamlpro.com/http/alt-ergo-free-2.2.0/alt-ergo-free-2.2.0.tar.gz";
+      sha256 = "11ffm87vsrii8nyhxhbc9gzjmqkspqv7hpjq7ll9xflll7gpnpkj";
+      stripRoot=false;
+    };
+
+  nativeBuildInputs = [
+    autoreconfHook
+    which
+  ];
+
+  buildInputs = [
+    ocaml
+    findlib
+    zarith
+    ocplib-simplex
+    psmt2-frontend
+    lablgtk
+    menhir
+  ];
+
+  propagatedBuildInputs = [ camlzip num ];
+
+  enableParallelBuilding = true;
+
+  configureFlags = [ "--enable-verbose-make" ];
+
+  installTargets = [ "install" ];
+
+  meta = {
+    description = "High-performance theorem prover and SMT solver";
+    homepage    = "https://alt-ergo.ocamlpro.com/";
+    license     = lib.licenses.ocamlpro_nc;
+    maintainers = [ lib.maintainers.thoughtpolice ];
+  };
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 407a1ce6688..02e5e5aebb8 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -2,7 +2,9 @@ let
   sources = import ./sources.nix {};
   ocamlOverlay = oself: osuper: {
     # External Packages
+    alt-ergo = oself.callPackage ./alt-ergo.nix {};
     camlzip = oself.callPackage ./camlzip.nix {};
+    psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
     why3 = oself.callPackage ./why3.nix {};
     # Builds
     frama-c = oself.callPackage ./frama-c.nix {};
diff --git a/nix/psmt2-frontend.nix b/nix/psmt2-frontend.nix
new file mode 100644
index 00000000000..f0502c4bc77
--- /dev/null
+++ b/nix/psmt2-frontend.nix
@@ -0,0 +1,49 @@
+{ callPackage
+, fetchzip
+, lib
+, stdenv
+, ocaml
+, findlib
+, menhir
+, autoreconfHook
+, which
+}:
+
+stdenv.mkDerivation rec {
+  pname = "psmt2-frontend";
+  version = "0.1";
+
+  src =
+    fetchzip {
+      url = "https://github.com/Coquera/psmt2-frontend/archive/0.1.zip";
+      sha256 = "0k7jlsbkdyg7hafmvynp0ik8xk7mfr00wz27vxn4ncnmp20yz4vn";
+    };
+
+  nativeBuildInputs = [
+    autoreconfHook
+    which
+  ];
+
+  buildInputs = [
+    ocaml
+    findlib
+    menhir
+  ];
+
+  enableParallelBuilding = true;
+
+  configureFlags = [ "--enable-verbose-make" ];
+
+  createFindlibDestdir = true;
+
+  installFlags = "LIBDIR=$(OCAMLFIND_DESTDIR)";
+
+  installTargets = [ "install" ];
+
+  meta = {
+    description = "A simple parser and type-checker for polomorphic extension of the SMT-LIB 2 language";
+    license = lib.licenses.asl20;
+    maintainers = [ lib.maintainers.vbgl ];
+    inherit (src.meta) homepage;
+  };
+}
-- 
GitLab