From 010ebf351ec4ce3468af579811af9345af44d15d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 31 Mar 2023 14:33:27 +0200
Subject: [PATCH] [nix] AE 2.4.2
---
nix/alt-ergo.nix | 85 ++++++++++++++++++++----------------------
nix/pkgs.nix | 2 -
nix/psmt2-frontend.nix | 48 ------------------------
3 files changed, 41 insertions(+), 94 deletions(-)
delete mode 100644 nix/psmt2-frontend.nix
diff --git a/nix/alt-ergo.nix b/nix/alt-ergo.nix
index 159534d5d6a..75288b5ff80 100644
--- a/nix/alt-ergo.nix
+++ b/nix/alt-ergo.nix
@@ -1,50 +1,47 @@
-{ 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
- ];
+{ fetchFromGitHub, fetchpatch, lib, which, ocamlPackages }:
- buildInputs = [
- ocaml
- findlib
- zarith
- ocplib-simplex
- psmt2-frontend
- lablgtk
- menhir
- ];
-
- propagatedBuildInputs = [ camlzip num ];
+let
+ pname = "alt-ergo";
+ version = "2.4.2";
- enableParallelBuilding = true;
+ configureScript = "ocaml unix.cma configure.ml";
- configureFlags = [ "--enable-verbose-make" ];
+ src = fetchFromGitHub {
+ owner = "OCamlPro";
+ repo = pname;
+ rev = "refs/tags/${version}";
+ hash = "sha256-8pJ/1UAbheQaLFs5Uubmmf5D0oFJiPxF6e2WTZgRyAc=";
+ };
+in
+
+let alt-ergo-lib = ocamlPackages.buildDunePackage rec {
+ pname = "alt-ergo-lib";
+ inherit version src configureScript;
+ configureFlags = [ pname ];
+ nativeBuildInputs = [ which ];
+ buildInputs = with ocamlPackages; [ dune-configurator ];
+ propagatedBuildInputs = with ocamlPackages; [ num ocplib-simplex seq stdlib-shims zarith ];
+ preBuild = ''
+ substituteInPlace src/lib/util/version.ml --replace 'version="dev"' 'version="${version}"'
+ '';
+}; in
+
+let alt-ergo-parsers = ocamlPackages.buildDunePackage rec {
+ pname = "alt-ergo-parsers";
+ inherit version src configureScript;
+ configureFlags = [ pname ];
+ nativeBuildInputs = [ which ocamlPackages.menhir ];
+ propagatedBuildInputs = [ alt-ergo-lib ] ++ (with ocamlPackages; [ camlzip psmt2-frontend ]);
+}; in
+
+ocamlPackages.buildDunePackage {
+
+ inherit pname version src configureScript;
+
+ configureFlags = [ pname ];
+
+ nativeBuildInputs = [ which ocamlPackages.menhir ];
+ buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ];
meta = {
description = "High-performance theorem prover and SMT solver";
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 61270435196..6873f8f8014 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -5,9 +5,7 @@ let
alt-ergo = oself.callPackage ./alt-ergo.nix {};
camlp5 = oself.callPackage ./camlp5.nix {};
headache = oself.callPackage ./headache.nix {};
- menhirLib = oself.callPackage ./menhirLib.nix {};
mlmpfr = oself.callPackage ./mlmpfr.nix {};
- psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
why3 = oself.callPackage ./why3.nix {};
# Helpers
diff --git a/nix/psmt2-frontend.nix b/nix/psmt2-frontend.nix
deleted file mode 100644
index 98836906d46..00000000000
--- a/nix/psmt2-frontend.nix
+++ /dev/null
@@ -1,48 +0,0 @@
-{ callPackage
-, fetchFromGitHub
-, lib
-, stdenv
-, ocaml
-, findlib
-, menhir
-, autoreconfHook
-, which
-}:
-
-stdenv.mkDerivation rec {
- pname = "psmt2-frontend";
- version = "0.1";
-
- src = fetchFromGitHub {
- owner = "Coquera";
- repo = pname;
- rev = version;
- sha256 = "0k7jlsbkdyg7hafmvynp0ik8xk7mfr00wz27vxn4ncnmp20yz4vn";
- };
-
- nativeBuildInputs = [
- autoreconfHook
- which
- ];
-
- buildInputs = [
- ocaml
- findlib
- menhir
- ];
-
- enableParallelBuilding = true;
-
- configureFlags = [ "--enable-verbose-make" ];
-
- createFindlibDestdir = true;
-
- installFlags = "LIBDIR=$(OCAMLFIND_DESTDIR)";
-
- 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