From ea37c7b5caa9afbca0e2fc18dc6515da29eb1ec0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 17 May 2022 16:08:19 +0200
Subject: [PATCH] [ci] fix mlgmp -> mlmpfr
---
nix/frama-c.nix | 9 ++++++---
nix/internal-tests.nix | 9 ++++++---
nix/mlgmpidl.nix | 35 -----------------------------------
nix/mlmpfr.nix | 30 ++++++++++++++++++++++++++++++
nix/pkgs.nix | 2 +-
src/plugins/value/dune | 10 +++++-----
6 files changed, 48 insertions(+), 47 deletions(-)
delete mode 100644 nix/mlgmpidl.nix
create mode 100644 nix/mlmpfr.nix
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index 36893ce6c84..3af9b2d54cd 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -21,7 +21,7 @@
, lablgtk3-sourceview3
, ltl2ba
, menhirLib
-, mlgmpidl
+, mlmpfr
, ocaml
, ocamlgraph
, ppx_deriving
@@ -42,7 +42,10 @@
# some files and prepare some information before starting dune.
stdenvNoCC.mkDerivation rec {
pname = "frama-c";
- version = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION);
+ version =
+ lib.strings.replaceStrings ["~"] ["-"]
+ (lib.strings.removeSuffix "\n"
+ (builtins.readFile ../VERSION));
slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
src = gitignoreSource ./..;
@@ -65,7 +68,7 @@ stdenvNoCC.mkDerivation rec {
lablgtk3-sourceview3
ltl2ba
menhirLib
- mlgmpidl
+ mlmpfr
ocaml
ocamlgraph
ppx_deriving
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 7266d1ccf54..ac5b8b060be 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -21,7 +21,7 @@
, lablgtk3-sourceview3
, ltl2ba
, menhirLib
-, mlgmpidl
+, mlmpfr
, ocaml
, ocamlgraph
, ppx_deriving
@@ -47,7 +47,10 @@
# some files and prepare some information before starting dune.
stdenvNoCC.mkDerivation rec {
pname = "frama-c-internal-tests";
- version = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION);
+ version =
+ lib.strings.replaceStrings ["~"] ["-"]
+ (lib.strings.removeSuffix "\n"
+ (builtins.readFile ../VERSION));
slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
src = gitignoreSource ./..;
@@ -71,7 +74,7 @@ stdenvNoCC.mkDerivation rec {
lablgtk3-sourceview3
ltl2ba
menhirLib
- mlgmpidl
+ mlmpfr
ocaml
ocamlgraph
ppx_deriving
diff --git a/nix/mlgmpidl.nix b/nix/mlgmpidl.nix
deleted file mode 100644
index 4f3abc7fbe0..00000000000
--- a/nix/mlgmpidl.nix
+++ /dev/null
@@ -1,35 +0,0 @@
-{ stdenv, lib, fetchFromGitHub, perl, ocaml, findlib, camlidl, gmp, mpfr }:
-
-stdenv.mkDerivation rec {
- name = "ocaml${ocaml.version}-mlgmpidl-${version}";
- version = "1.2.14";
- src = fetchFromGitHub {
- owner = "nberth";
- repo = "mlgmpidl";
- rev = version;
- sha256 = "1wrwg35myp4i962bhj1ah08115w2ksjyc4yypdili1hpcpyhwnnp";
- };
-
- buildInputs = [ perl gmp mpfr ocaml findlib camlidl ];
-
- prefixKey = "-prefix ";
- configureFlags = [
- "--gmp-prefix ${gmp.dev}"
- "--mpfr-prefix ${mpfr.dev}"
- ];
-
- postConfigure = ''
- sed -i Makefile \
- -e 's|^ /bin/rm | rm |'
- mkdir -p $out/lib/ocaml/${ocaml.version}/site-lib/stublibs
- '';
-
-
- meta = {
- description = "OCaml interface to the GMP library";
- homepage = "https://www.inrialpes.fr/pop-art/people/bjeannet/mlxxxidl-forge/mlgmpidl/";
- license = lib.licenses.lgpl21;
- inherit (ocaml.meta) platforms;
- maintainers = [ lib.maintainers.vbgl ];
- };
-}
diff --git a/nix/mlmpfr.nix b/nix/mlmpfr.nix
new file mode 100644
index 00000000000..a10f2eb751d
--- /dev/null
+++ b/nix/mlmpfr.nix
@@ -0,0 +1,30 @@
+
+{ lib
+, fetchFromGitHub
+, gmp
+, mpfr
+, buildDunePackage
+}:
+
+buildDunePackage rec {
+ pname = "mlmpfr";
+ version = "4.1.0-bugfix1";
+
+ minimumOCamlVersion = "4.04";
+
+ src = fetchFromGitHub {
+ owner = "thvnx";
+ repo = pname;
+ rev = pname+"."+version;
+ sha256 = "13n6spgz5p6jhpjackvfsn33iinpadgr3v4gm63d5195mi9fgn8d";
+ };
+
+ buildInputs = [ gmp mpfr ];
+
+ meta = {
+ description = "The package provides bindings for MPFR";
+ license = lib.licenses.lgpl3Only;
+ maintainers = [ ];
+ homepage = "https://github.com/thvnx/mlmpfr";
+ };
+}
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 5af58edd806..7767fb2080b 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -5,7 +5,7 @@ let
alt-ergo = oself.callPackage ./alt-ergo.nix {};
camlzip = oself.callPackage ./camlzip.nix {};
headache = oself.callPackage ./headache.nix {};
- mlgmpidl = oself.callPackage ./mlgmpidl.nix {};
+ mlmpfr = oself.callPackage ./mlmpfr.nix {};
ocp-indent = oself.callPackage ./ocp-indent.nix {};
psmt2-frontend = oself.callPackage ./psmt2-frontend.nix {};
why3 = oself.callPackage ./why3.nix {};
diff --git a/src/plugins/value/dune b/src/plugins/value/dune
index 6f30149a133..ca9492dd3ff 100644
--- a/src/plugins/value/dune
+++ b/src/plugins/value/dune
@@ -3,8 +3,8 @@
(deps (universe))
(action (progn
(echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
- (echo "Numerors:" %{lib-available:frama-c-eva.numerors} "\n")
- (echo " - MLGMPIDL (gmp):" %{lib-available:gmp} "\n")
+ (echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
+ (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
(echo "Apron domains:" %{lib-available:frama-c-eva.apron} "\n")
(echo " - apron.octMPQ:" %{lib-available:apron.octMPQ} "\n")
(echo " - apron.boxMPQ:" %{lib-available:apron.boxMPQ} "\n")
@@ -150,14 +150,14 @@
( library
(name numerors)
- (public_name frama-c-eva.numerors)
+ (public_name frama-c-eva.numerors.core)
(flags -open Frama_c_kernel -open Eva.Private :standard)
(modules numerors_domain numerors_utils numerors_float numerors_interval numerors_arithmetics numerors_value)
- (libraries frama-c.kernel frama-c-eva.core gmp)
+ (libraries frama-c.kernel frama-c-eva.core mlmpfr)
(optional)
)
-;(plugin (optional) (name eva-numerors) (libraries frama-c-eva.numerors) (site (frama-c plugins)))
+;(plugin (optional) (name eva.numerors) (libraries frama-c-eva.numerors.core) (site (frama-c plugins)))
( library
(name apron_domain)
--
GitLab