diff --git a/nix/frama-c.nix b/nix/frama-c.nix index 36893ce6c84e3dcb0df4746c3620602a1e9cc078..3af9b2d54cd7c54f43b6c5f3acdb06b6f0656de5 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 7266d1ccf542000c6f3e806110fd90468138f551..ac5b8b060beb07d094b72942a685fb27663b5950 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 4f3abc7fbe0145d254eb5f41560d0e67bccb17ef..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..a10f2eb751d05a722bf0f0ce098d5e83a2f0c0ea --- /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 5af58edd806a6085da49018c54e08439d4879b23..7767fb2080b8f6cd09126755217648f3a8b1394e 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 6f30149a133c66f6f3ceb40d0f31b5356312110d..ca9492dd3fffaf29718104a20b8bbe83679f3639 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)