1 files changed, 40 insertions, 0 deletions
diff --git a/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
new file mode 100644
index 000000000000..d84aa5b6918a
--- /dev/null
+++ b/nixpkgs/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -0,0 +1,40 @@
+{ darwin, fetchurl, lib, ocamlPackages, stdenv }:
+
+let
+  pname = "alt-ergo";
+  version = "2.5.2";
+
+  src = fetchurl {
+    url = "https://github.com/OCamlPro/alt-ergo/releases/download/v${version}/alt-ergo-${version}.tbz";
+    hash = "sha256-9GDBcBH49sheO5AjmDsznMEbw0JSrnSOcIIRN40/aJU=";
+  };
+in
+
+let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-lib";
+  inherit version src;
+  buildInputs = with ocamlPackages; [ ppx_blob ];
+  propagatedBuildInputs = with ocamlPackages; [ camlzip dolmen_loop dune-build-info fmt ocplib-simplex seq stdlib-shims zarith ];
+}; in
+
+let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+  pname = "alt-ergo-parsers";
+  inherit version src;
+  nativeBuildInputs = [ ocamlPackages.menhir ];
+  propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ psmt2-frontend ]);
+}; in
+
+ocamlPackages.buildDunePackage {
+
+  inherit pname version src;
+
+  nativeBuildInputs = [ ocamlPackages.menhir ] ++ lib.optionals stdenv.isDarwin [ darwin.sigtool ];
+  buildInputs = [ alt-ergo-parsers ] ++ (with ocamlPackages; [ cmdliner dune-site ]);
+
+  meta = {
+    description = "High-performance theorem prover and SMT solver";
+    homepage    = "https://alt-ergo.ocamlpro.com/";
+    license     = lib.licenses.ocamlpro_nc;
+    maintainers = [ lib.maintainers.thoughtpolice ];
+  };
+}