diff --git a/default.nix b/default.nix
deleted file mode 100644
index e64150378a86d1a128776f31ba1f5912ea77af15..0000000000000000000000000000000000000000
--- a/default.nix
+++ /dev/null
@@ -1,15 +0,0 @@
-# standalone derivation, for nix-build, nix-shell, etc
-{ pkgs ? import <nixpkgs> {} }:
-let
- src = builtins.fetchGit {
- "url" = ./.git;
- "name" = "frama-c";
- "rev" = "ffa925f404779a3a0c4aacff5bd78b1c502def11";
- "ref" = "test-nix-fetchGit";
- };
- in
-
-pkgs.callPackage ./nix/default.nix {
- opam2nix = pkgs.callPackage ../Frama-CI/opam2nix-packages.nix {};
- src = src;
-}
diff --git a/nix/default.nix b/nix/default.nix
deleted file mode 100644
index 4e146ccd47d633f8737f0183882061de862ed84a..0000000000000000000000000000000000000000
--- a/nix/default.nix
+++ /dev/null
@@ -1,396 +0,0 @@
-# paramaterised derivation with dependencies injected (callPackage style)
-{ pkgs, stdenv, src ? ../., opam2nix, ocaml ? pkgs.ocaml-ng.ocamlPackages_4_08.ocaml, plugins ? { } }:
-
-let mydir = builtins.getEnv("PWD");
- mk-opam-selection = { name, opamSrc?{}, ... }: {
- inherit ocaml;
- src = opamSrc;
- selection = "${mydir}/${name}-${ocaml.version}-opam-selection.nix";
- };
- opamPackages =
- [ "ocamlfind=1.9.3" "zarith" "ocamlgraph" "yojson=1.7.0" "zmq"
- "ppx_import" "ppx_deriving" "ppx_deriving_yojson"
- "coq=8.13.0" "alt-ergo=2.2.0"
- "why3=1.5.0" "why3-coq=1.5.0"
- "menhir=20211012" "dune=2.9.1"
- "easy-format=1.3.2"
- "biniou=1.2.1"
- ];
- # only pure nix packages. See mk_deriv below for adding opam2nix packages
- mk_buildInputs = { nixPackages ? [] } :
- [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages;
- # Extends the call to stdenv.mkDerivation with parameters common for all
- # frama-c derivations
- mk_deriv = args:
- let my_opam_packages =
- if args?opamPackages then
- opamPackages ++ args.opamPackages
- else opamPackages
- ;
- opam-selection = mk-opam-selection args;
- buildInputs = args.buildInputs ++ opam2nix.buildInputs opam-selection;
- in
- stdenv.mkDerivation (
- args //
- {
- # Disable Nix's GCC hardening
- hardeningDisable = [ "all" ];
- inherit buildInputs;
- })
- //
- { gen-opam-selection =
- opam2nix.resolve opam-selection my_opam_packages; }
- ;
-in
-
-pkgs.lib.makeExtensible
-(self: {
- inherit src mk_buildInputs opamPackages mk_deriv;
- buildInputs = mk_buildInputs {};
- installed = self.main.out;
- main = mk_deriv {
- name = "frama-c";
- src = self.src;
- buildInputs =self.buildInputs;
- outputs = [ "out" "build_dir" ];
- postPatch = ''
- patchShebangs .
- '';
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make -j 4
- '';
- installPhase = ''
- make install
- mkdir -p $build_dir
- tar -cf $build_dir/dir.tar .
- pwd > $build_dir/old_pwd
- '';
- setupHook = pkgs.writeText "setupHook.sh" ''
- addFramaCPath () {
- if test -d "$1/lib/frama-c/plugins"; then
- export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN:-}''${FRAMAC_PLUGIN:+:}$1/lib/frama-c/plugins"
- export OCAMLPATH="''${OCAMLPATH:-}''${OCAMLPATH:+:}$1/lib/frama-c/plugins"
- fi
-
- if test -d "$1/lib/frama-c"; then
- export OCAMLPATH="''${OCAMLPATH:-}''${OCAMLPATH:+:}$1/lib/frama-c"
- fi
-
- if test -d "$1/share/frama-c/"; then
- export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE:-}''${FRAMAC_EXTRA_SHARE:+:}$1/share/frama-c"
- fi
-
- }
-
- addEnvHooks "$targetOffset" addFramaCPath
- '';
- };
-
- lint = mk_deriv {
- name = "frama-c-lint";
- src = self.src;
- opamPackages = [ "ocp-indent=1.8.1" "headache=1.05"];
- buildInputs =
- self.mk_buildInputs { nixPackages = [ pkgs.bc pkgs.clang_10 ]; };
- outputs = [ "out" ];
- postPatch = ''
- patchShebangs .
- '';
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make lint
- make stats-lint
- STRICT_HEADERS=yes make check-headers
- '';
- installPhase = ''
- true
- '';
- };
-
- doc = mk_deriv {
- name = "frama-c-doc";
- buildInputs = self.buildInputs;
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postPatch = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make doc
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main";};
-
- tests = mk_deriv {
- name = "frama-c-test";
- buildInputs = self.buildInputs;
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- make tests -j4 PTESTS_OPTS="-error-code -j 4"
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- build-distrib-tarball = mk_deriv {
- name = "frama-c-build-distrib-tarball";
- src = self.src;
- buildInputs = self.buildInputs;
- opamPackages = [ "headache=1.05" ];
- outputs = [ "out" ];
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make DISTRIB="frama-c-archive" src-distrib
- tar -zcf frama-c-tests-archive.tar.gz tests src/plugins/*/tests
- '';
- installPhase = ''
- tar -C $out --strip-components=1 -xzf frama-c-archive.tar.gz
- tar -C $out -xzf frama-c-tests-archive.tar.gz
- '';
- };
-
- build-from-distrib-tarball = mk_deriv {
- name = "frama-c-build-from-distrib-tarball";
- doCheck = true;
- buildInputs = self.buildInputs;
- opamPackages = self.build-distrib-tarball.opamPackages;
- src = self.build-distrib-tarball.out ;
- outputs = [ "out" ];
- postPatch = ''
- patchShebangs .
- '';
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make -j 4
- '';
- checkPhase = ''
- make clean_share_link
- make create_share_link
- make tests -j4 PTESTS_OPTS="-error-code -j 4"
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "build-distrib-tarball"; };
-
- wp-qualif = mk_deriv {
- name = "frama-c-wp-qualif";
- buildInputs = self.mk_buildInputs { };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- make src/plugins/wp/tests/test_config_qualif
- export FRAMAC_WP_CACHE=replay
- export FRAMAC_WP_CACHEDIR=${plugins.wp-cache.src}
- bin/ptests.opt -error-code -config qualif src/plugins/wp/tests
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- aorai-prove = mk_deriv {
- name = "frama-c-aorai-prove";
- buildInputs = self.mk_buildInputs { };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "test_config*" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
-
- buildPhase = ''
- make clean_share_link
- make create_share_link
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- make src/plugins/aorai/tests/ptests_config
- export AORAI_WP_CACHE=replay
- export AORAI_WP_CACHEDIR=${plugins.wp-cache.src}
- make PTESTS_OPTS="-error-code" aorai-test-prove
- '';
-
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- eva-tests = mk_deriv {
- name = "frama-c-eva-tests";
- buildInputs = self.mk_buildInputs { };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- export CONFIGS="equality bitwise symblocs gauges octagon"
- src/plugins/value/vtests.sh -j 4 -error-code
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- e-acsl-tests-dev = mk_deriv {
- name = "frama-c-e-acsl-tests-dev";
- buildInputs = self.mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- make E_ACSL_TESTS PTESTS_OPTS="-error-code" DEV=yes
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- internal = mk_deriv {
- name = "frama-c-internal";
- src = self.src;
- opamPackages = [ "xml-light" ];
- buildInputs =
- self.mk_buildInputs
- { nixPackages =
- [ pkgs.getopt pkgs.libxslt pkgs.libxml2 pkgs.autoPatchelfHook
- pkgs.swiProlog stdenv.cc.cc.lib ];
- };
- genassigns_src = plugins.genassigns.src;
- frama_clang_src = plugins.frama-clang.src;
- pathcrawler_src = plugins.pathcrawler.src;
- mthread_src = plugins.mthread.src;
- caveat_importer_src = plugins.caveat-importer.src;
- acsl_importer_src = plugins.acsl-importer.src;
- volatile_src = plugins.volatile.src;
- security_src = plugins.security.src;
- context_from_precondition_src = plugins.context-from-precondition.src;
- metacsl_src = plugins.meta.src;
- linea_cabs_src = plugins.linea-cabs.src;
- postPatch = ''
- patchShebangs .
- '';
- postUnpack = ''
- cp -r --preserve=mode "$genassigns_src" "$sourceRoot/src/plugins/genassigns"
- chmod -R u+w -- "$sourceRoot/src/plugins/genassigns"
- # cp -r --preserve=mode "$frama_clang_src" "$sourceRoot/src/plugins/frama-clang"
- # chmod -R u+w -- "$sourceRoot/src/plugins/frama-clang"
- cp -r --preserve=mode "$pathcrawler_src" "$sourceRoot/src/plugins/pathcrawler"
- chmod -R u+w -- "$sourceRoot/src/plugins/pathcrawler"
- cp -r --preserve=mode "$mthread_src" "$sourceRoot/src/plugins/mthread"
- chmod -R u+w -- "$sourceRoot/src/plugins/mthread"
- cp -r --preserve=mode "$caveat_importer_src" "$sourceRoot/src/plugins/caveat-importer"
- chmod -R u+w -- "$sourceRoot/src/plugins/caveat-importer"
- cp -r --preserve=mode "$volatile_src" "$sourceRoot/src/plugins/volatile"
- chmod -R u+w -- "$sourceRoot/src/plugins/volatile"
- cp -r --preserve=mode "$acsl_importer_src" "$sourceRoot/src/plugins/acsl-importer"
- chmod -R u+w -- "$sourceRoot/src/plugins/acsl-importer"
- echo IN_FRAMA_CI=yes > "$sourceRoot/in_frama_ci"
- cp -r --preserve=mode "$context_from_precondition_src" "$sourceRoot/src/plugins/context-from-precondition"
- chmod -R u+w -- "$sourceRoot/src/plugins/context-from-precondition"
- cp -r --preserve=mode "$linea_cabs_src" "$sourceRoot/src/plugins/linea-cabs"
- chmod -R u+w -- "$sourceRoot/src/plugins/linea-cabs"
- cp -r --preserve=mode "$security_src" "$sourceRoot/src/plugins/security"
- chmod -R u+w -- "$sourceRoot/src/plugins/security"
- '';
-
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make unpack-eclipse
- sed -i src/plugins/pathcrawler/extern/eclipseCLP/RUNME -e "s/chmod 2755/chmod 755/g"
- rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/dbi_mysql.so
- rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/ic.so
- rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/bitmap.so
- rm -fr src/plugins/pathcrawler/extern/eclipseCLP/lib/i386_linux
- rm src/plugins/pathcrawler/src/generator/COLIBRI/float_util_sparc_sunos5.so
- rm src/plugins/pathcrawler/src/generator/COLIBRI/float_util_i386_linux.so.*
- rm src/plugins/pathcrawler/share/bin/float_util_sparc_sunos5.so
- find src/plugins/pathcrawler -name '*_i386_*.so' -delete
- autoPatchelf src/plugins/pathcrawler/
- make -j 4
- ln -sr src/plugins/pathcrawler/share share/pc
- # Setup Why3
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- # Setup WP related
- export CAVEAT_IMPORTER_NIX_MODE=yes
- export GENASSIGNS_NIX_MODE=yes
- export FRAMAC_WP_CACHE=replay
- export FRAMAC_WP_CACHEDIR=${plugins.wp-cache.src}
- make tests -j4 PTESTS_OPTS="-error-code -j 4"
- '';
- installPhase = ''
- make install
- '';
- };
-
-})
diff --git a/nix/empty b/nix/empty
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
deleted file mode 100644
index eccc033949bb7b58902bedfcbf60a6d6555b59eb..0000000000000000000000000000000000000000
--- a/nix/frama-ci.nix
+++ /dev/null
@@ -1,16 +0,0 @@
-#To copy in other repository
-{ password}:
-
-let
- src = builtins.fetchGit {
- "url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
- "name" = "Frama-CI";
- "rev" = "ceea8c97fc127db159bfd92919eae404e2e67f18";
- "ref" = "master";
- };
- pkgs = import "${src}/pkgs.nix" {};
- in
- {
- src = src;
- compiled = pkgs.callPackage "${src}/compile.nix" { inherit pkgs; };
- }
diff --git a/nix/shell.nix b/nix/shell.nix
deleted file mode 100644
index 1eda48797e573f965fac0f432d345f04f5bdee8a..0000000000000000000000000000000000000000
--- a/nix/shell.nix
+++ /dev/null
@@ -1,13 +0,0 @@
-let
- pkgs = import ./pkgs.nix;
- ocamlPackages_for_shell = pkgs.ocaml-ng.ocamlPackages_4_12;
-in
-pkgs.mkShell {
- nativeBuildInputs = with pkgs; [
- niv
- ocamlPackages_for_shell.merlin
- ocamlPackages_for_shell.ocaml-lsp
- ocamlPackages_for_shell.utop
- ];
- inputsFrom = [ ocamlPackages_for_shell.frama-c ];
-}