From 8f6fa487cf7922dd1e3d4256c224cf4801d7c277 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Fri, 16 Feb 2024 09:31:55 +0100 Subject: [PATCH] [nix] update commit - remove useless packages - fix deprecated symbol - add export for disabling store mangling --- nix/alt-ergo.nix | 34 +++++++++++++++++++++++---------- nix/frama-c-checkers-shell.nix | 4 ++-- nix/headache.nix | 32 ------------------------------- nix/internal-tests.nix | 4 ++++ nix/mk_plugin.nix | 4 ++++ nix/mk_tests.nix | 4 ++++ nix/ocplib-simplex.nix | 4 ++-- nix/pkgs.nix | 5 ++--- nix/plugin-checkers-shell.nix | 4 ++-- nix/sources.json | 6 +++--- nix/src-distrib.nix | 35 ---------------------------------- nix/wp-cache.nix.sh | 1 + 12 files changed, 48 insertions(+), 89 deletions(-) delete mode 100644 nix/headache.nix delete mode 100644 nix/src-distrib.nix diff --git a/nix/alt-ergo.nix b/nix/alt-ergo.nix index 75288b5ff80..0bdce24403b 100644 --- a/nix/alt-ergo.nix +++ b/nix/alt-ergo.nix @@ -1,4 +1,18 @@ -{ fetchFromGitHub, fetchpatch, lib, which, ocamlPackages }: +{ lib +, buildDunePackage +, fetchFromGitHub +, camlzip +, cmdliner +, dune-configurator +, menhir +, num +, ocplib-simplex +, psmt2-frontend +, seq +, stdlib-shims +, which +, zarith +}: let pname = "alt-ergo"; @@ -14,34 +28,34 @@ let }; in -let alt-ergo-lib = ocamlPackages.buildDunePackage rec { +let alt-ergo-lib = 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 ]; + buildInputs = [ dune-configurator ]; + propagatedBuildInputs = [ 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 { +let alt-ergo-parsers = 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 ]); + nativeBuildInputs = [ which menhir ]; + propagatedBuildInputs = [ alt-ergo-lib camlzip psmt2-frontend ]; }; in -ocamlPackages.buildDunePackage { +buildDunePackage { inherit pname version src configureScript; configureFlags = [ pname ]; - nativeBuildInputs = [ which ocamlPackages.menhir ]; - buildInputs = [ alt-ergo-parsers ocamlPackages.cmdliner ]; + nativeBuildInputs = [ which menhir ]; + buildInputs = [ alt-ergo-parsers cmdliner ]; meta = { description = "High-performance theorem prover and SMT solver"; diff --git a/nix/frama-c-checkers-shell.nix b/nix/frama-c-checkers-shell.nix index 1456c7a6e92..356f25ed92e 100644 --- a/nix/frama-c-checkers-shell.nix +++ b/nix/frama-c-checkers-shell.nix @@ -1,7 +1,7 @@ { lib , stdenv , black -, clang_10 +, clang_11 , combinetura , frama-c-hdrck , frama-c-lint @@ -16,7 +16,7 @@ stdenv.mkDerivation rec { name = "frama-c-checkers-shell"; buildInputs = [ black - clang_10 + clang_11 combinetura frama-c-hdrck frama-c-lint diff --git a/nix/headache.nix b/nix/headache.nix deleted file mode 100644 index 258016810dd..00000000000 --- a/nix/headache.nix +++ /dev/null @@ -1,32 +0,0 @@ -{ lib -, camomile -, fetchFromGitHub -, buildDunePackage -, cmdliner -}: - -buildDunePackage rec { - version = "v1.05"; - pname = "headache"; - - src = fetchFromGitHub { - owner = "Frama-C"; - repo = pname; - rev = version; - sha256 = "036lrcxh23j2rrj91wlgq9piyyv1vh82wjy63z1l1ggkkhfs7d8r"; - }; - - useDune2 = true; - - buildInputs = [ - cmdliner - camomile - ]; - - meta = with lib; { - homepage = https://github.com/Frama-C/headache/; - description = "Automatic generation of files headers"; - license = licenses.gpl2; - maintainers = [ ]; - }; -} diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix index bef1ffdc48e..48e04ae1ac9 100644 --- a/nix/internal-tests.nix +++ b/nix/internal-tests.nix @@ -145,8 +145,12 @@ stdenvNoCC.mkDerivation rec { export FRAMAC_WP_CACHEDIR=$wp_cache ''; + # The export NIX_GCC_DONT_MANGLE_PREFIX_MAP is meant to disable the + # transformation of the path of Frama-C into uppercase when using the + # __FILE__ macro. checkPhase = '' runHook preCheck + export NIX_GCC_DONT_MANGLE_PREFIX_MAP= dune exec -- frama-c-ptests -never-disabled tests src/plugins/*/tests dune build -j1 --display short @ptests_config ''; diff --git a/nix/mk_plugin.nix b/nix/mk_plugin.nix index 4cb2f5f666e..dbf03c6ba48 100644 --- a/nix/mk_plugin.nix +++ b/nix/mk_plugin.nix @@ -106,9 +106,13 @@ stdenv.mkDerivation { '' else "") ; + # The export NIX_GCC_DONT_MANGLE_PREFIX_MAP is meant to disable the + # transformation of the path of Frama-C into uppercase when using the + # __FILE__ macro. checkPhase = '' runHook preCheck make run-ptests + export NIX_GCC_DONT_MANGLE_PREFIX_MAP= dune build -j1 --display short @tests/ptests ''; diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix index 4d35f6a6a67..9d71cbf776d 100644 --- a/nix/mk_tests.nix +++ b/nix/mk_tests.nix @@ -103,8 +103,12 @@ stdenvNoCC.mkDerivation { '' else "" ; + # The export NIX_GCC_DONT_MANGLE_PREFIX_MAP is meant to disable the + # transformation of the path of Frama-C into uppercase when using the + # __FILE__ macro. buildPhase = '' runHook preBuild + export NIX_GCC_DONT_MANGLE_PREFIX_MAP= '' + tests-command + '' runHook postBuild diff --git a/nix/ocplib-simplex.nix b/nix/ocplib-simplex.nix index 474f69546d1..0e1226479dc 100644 --- a/nix/ocplib-simplex.nix +++ b/nix/ocplib-simplex.nix @@ -2,7 +2,7 @@ let pname = "ocplib-simplex"; - version = "0.4"; + version = "0.4.1"; in stdenv.mkDerivation { @@ -12,7 +12,7 @@ stdenv.mkDerivation { owner = "OCamlPro-Iguernlala"; repo = pname; rev = "v${version}"; - sha256 = "09niyidrjzrj8g1qwx4wgsdf5m6cwrnzg7zsgala36jliic4di60"; + sha256 = "sha256-bhlTBpJg031x2lUjwuVrhQgOGmDLW/+0naN8wRjv6i4="; }; nativeBuildInputs = [ autoreconfHook ocaml findlib ]; diff --git a/nix/pkgs.nix b/nix/pkgs.nix index 5e313453a1d..861ae8aeed1 100644 --- a/nix/pkgs.nix +++ b/nix/pkgs.nix @@ -4,7 +4,6 @@ let # External Packages alt-ergo = oself.callPackage ./alt-ergo.nix {}; combinetura = oself.callPackage ./combinetura.nix {}; - headache = oself.callPackage ./headache.nix {}; mlmpfr = oself.callPackage ./mlmpfr.nix {}; ocplib-simplex = oself.callPackage ./ocplib-simplex.nix {}; why3 = oself.callPackage ./why3.nix {}; @@ -68,8 +67,8 @@ let niv = (import sources.niv {}).niv; ocaml-ng = super.lib.mapAttrs ( name: value: - if builtins.hasAttr "overrideScope'" value - then value.overrideScope' ocamlOverlay + if builtins.hasAttr "overrideScope" value + then value.overrideScope ocamlOverlay else value ) super.ocaml-ng; inherit (super.callPackage sources."gitignore.nix" {}) gitignoreSource; diff --git a/nix/plugin-checkers-shell.nix b/nix/plugin-checkers-shell.nix index d64816338da..cc1d340f645 100644 --- a/nix/plugin-checkers-shell.nix +++ b/nix/plugin-checkers-shell.nix @@ -1,6 +1,6 @@ { lib , stdenv -, clang_10 +, clang_11 , frama-c , frama-c-hdrck , frama-c-lint @@ -12,7 +12,7 @@ stdenv.mkDerivation rec { name = "plugin-checkers-shell"; buildInputs = [ - clang_10 + clang_11 frama-c frama-c-hdrck frama-c-lint diff --git a/nix/sources.json b/nix/sources.json index cb4337bbbcb..3619413b613 100644 --- a/nix/sources.json +++ b/nix/sources.json @@ -29,10 +29,10 @@ "homepage": "https://github.com/NixOS/nixpkgs", "owner": "NixOS", "repo": "nixpkgs", - "rev": "fdd898f8f79e8d2f99ed2ab6b3751811ef683242", - "sha256": "05i97acjry4pk1br8glwl97gbfjafq058kblpfpd39r0qr8j6x4s", + "rev": "3030f185ba6a4bf4f18b87f345f104e6a6961f34", + "sha256": "0v5q4zadnmdiv8hwcsx804l8radx562aqdw0r5nld127c8f7jzz8", "type": "tarball", - "url": "https://github.com/NixOS/nixpkgs/archive/fdd898f8f79e8d2f99ed2ab6b3751811ef683242.tar.gz", + "url": "https://github.com/NixOS/nixpkgs/archive/3030f185ba6a4bf4f18b87f345f104e6a6961f34.tar.gz", "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz" }, "why3": { diff --git a/nix/src-distrib.nix b/nix/src-distrib.nix deleted file mode 100644 index 053764b047c..00000000000 --- a/nix/src-distrib.nix +++ /dev/null @@ -1,35 +0,0 @@ -{ lib -, stdenv -, frama-c -# , headache -, git -} : - -stdenv.mkDerivation rec { - pname = "src-distrib"; - version = frama-c.version; - slang = frama-c.slang; - - src = ./.. ; - - nativeBuildInputs = frama-c.nativeBuildInputs; - - buildInputs = frama-c.buildInputs ++ [ - # headache - git - ]; - - preBuild = '' - patchShebangs ./devel_tools/make-distrib.sh - ''; - - buildPhase = '' - runHook preBuild - ./devel_tools/make-distrib.sh - ''; - - installPhase = '' - mkdir -p $out - cp frama-c.tar.gz $out - ''; -} diff --git a/nix/wp-cache.nix.sh b/nix/wp-cache.nix.sh index d633e7332bd..0130917c1d8 100755 --- a/nix/wp-cache.nix.sh +++ b/nix/wp-cache.nix.sh @@ -32,5 +32,6 @@ stdenv.mkDerivation rec { rev = "$commit" ; shallow = true ; }; + installPhase = "touch \$out"; } EOL -- GitLab