diff --git a/nix/frama-c.nix b/nix/frama-c.nix index a5e914062d7968ca56c4065a572fe8d454a0865e..4a1a02b544e2fa584a266ec93f6549c2bf31ad3f 100644 --- a/nix/frama-c.nix +++ b/nix/frama-c.nix @@ -24,7 +24,6 @@ , dune-configurator , dune-site , fpath -, jq , gcc9 , graphviz , lablgtk3 @@ -35,7 +34,6 @@ , mlmpfr , ocaml , ocamlgraph -, ocamlgraph_gtk , ocp-indent , ppx_deriving , ppx_deriving_yaml @@ -47,12 +45,9 @@ , yaml , zarith , zmq -# Frama-C extra (other targets do not reconfigure) -, check-jsonschema -, dos2unix -, doxygen +# For Python3 tests configuration , python3 -, python3Packages +# Target parameters , cover ? true , release_mode ? false }: @@ -82,13 +77,11 @@ stdenvNoCC.mkDerivation rec { bisect_ppx camlzip camomile - check-jsonschema dune_3 dune-configurator dune-site findlib fpath - jq gcc9 graphviz lablgtk3 @@ -99,7 +92,6 @@ stdenvNoCC.mkDerivation rec { mlmpfr ocaml ocamlgraph - ocamlgraph_gtk ocp-indent ppx_deriving ppx_deriving_yaml @@ -112,8 +104,6 @@ stdenvNoCC.mkDerivation rec { zarith zmq # For other CI targets - dos2unix - doxygen python3 ]; diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix index 5ad5c381a4e2ce4d3ad73a893d55db4fe763dada..7fcfc01bc5b2a9ceec939ca09d29e391906d8927 100644 --- a/nix/internal-tests.nix +++ b/nix/internal-tests.nix @@ -19,6 +19,7 @@ , dune_3 , dune-configurator , dune-site +, fpath , gcc9 , graphviz , lablgtk3 @@ -35,23 +36,24 @@ , ppx_deriving_yojson , unionFind , yojson -, which , why3 , yaml , zarith , zmq # Frama-C tests , alt-ergo +, check-jsonschema , dos2unix -, doxygen +, jq , perl -, pkgs , python3 , python3Packages -, yq , swiProlog , time +, unixtools +, which , wp-cache +, yq }: # We do not use buildDunePackage because Frama-C still uses a Makefile to build @@ -73,7 +75,6 @@ stdenvNoCC.mkDerivation rec { buildInputs = [ apron - alt-ergo camlzip camomile clang @@ -81,6 +82,7 @@ stdenvNoCC.mkDerivation rec { dune-configurator dune-site findlib + fpath gcc9 graphviz lablgtk3 @@ -98,21 +100,24 @@ stdenvNoCC.mkDerivation rec { unionFind yojson which - yaml why3 + yaml zarith zmq # Tests alt-ergo + check-jsonschema dos2unix - doxygen + jq perl - pkgs.getopt python3 + python3Packages.jsonschema python3Packages.pyaml - yq swiProlog time + unixtools.getopt + which + yq ]; outputs = [ "out" ]; diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix index 4a54d793df4e03181c10f31f7b7a997a7f56b727..81e3c3f6a6e2b65859b8a075e24cd4ad24ec783d 100644 --- a/nix/mk_tests.nix +++ b/nix/mk_tests.nix @@ -28,15 +28,18 @@ , alt-ergo , cvc4 , clang +, check-jsonschema +, dos2unix , frama-c +, jq , perl , python3Packages , stdenvNoCC , time , unixtools -, yq , which , wp-cache +, yq } : { tests-name @@ -55,13 +58,17 @@ stdenvNoCC.mkDerivation { buildInputs = frama-c.buildInputs ++ [ clang + check-jsonschema + dos2unix frama-c + jq perl python3Packages.jsonschema + python3Packages.pyaml time unixtools.getopt - yq which + yq ] ++ (if has-wp-proofs then [ alt-ergo cvc4 ] else []);