diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 51eb4ef5182c36d78dbf918ff2ea21775c0a5437..86720ed9644ffcc8f9dab66d25620cfd5ecd82a6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -30,7 +30,13 @@ git-update:
frama-c:
stage: build
script:
- - nix/frama-ci.sh build -A frama-c.installed
+ - nix/frama-ci.sh build -A frama-c.main
+ artifacts:
+ when: on_failure
+ paths:
+ - commits.nix
+ - results.log
+ expire_in: 1 day
tags:
- nix
diff --git a/nix/default.nix b/nix/default.nix
index 03228dd27a436ab8cc3b5fb1d6c640af04df9fd9..b6cdc9bdde2d309a9e84b6fa02be0b44a0e48b42 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -1,31 +1,47 @@
# paramaterised derivation with dependencies injected (callPackage style)
-{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_08.ocaml", plugins ? { } }:
+{ pkgs, stdenv, src ? ../., opam2nix, ocaml ? pkgs.ocaml-ng.ocamlPackages_4_08.ocaml, plugins ? { } }:
-let mk_buildInputs = { opamPackages ? [], 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 ++ opam2nix.build {
- specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson" "zmq"
- "ppx_deriving" "ppx_deriving_yojson"
- { name = "coq"; constraint = "=8.12.0"; }
- { name = "alt-ergo" ; constraint = "=2.2.0"; }
- { name = "why3" ; constraint = "=1.4.0"; }
- { name = "why3-coq" ; constraint = "=1.4.0"; }
- ] ++ opamPackages
- );
- ocamlAttr = ocaml_version;
- };
+let mydir = builtins.getEnv("PWD");
+ mk-opam-selection = { name, opamSrc?null, ... }: {
+ inherit ocaml;
+ src = opamSrc;
+ selection = "${mydir}/${name}-${ocaml.version}-opam-selection.nix";
+ };
+ opamPackages =
+ [ "ocamlfind" "zarith" "ocamlgraph" "yojson" "zmq"
+ "ppx_deriving" "ppx_deriving_yojson"
+ "coq=8.12.0" "alt-ergo=2.2.0" "why3=1.4.0" "why3-coq=1.4.0" ];
+ # 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:
- stdenv.mkDerivation ({
+ 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" ];
- } // args);
+ inherit buildInputs;
+ })
+ //
+ { gen-opam-selection =
+ opam2nix.resolve opam-selection my_opam_packages; }
+ ;
in
pkgs.lib.makeExtensible
(self: {
- inherit src mk_buildInputs;
+ inherit src mk_buildInputs opamPackages mk_deriv;
buildInputs = mk_buildInputs {};
installed = self.main.out;
main = mk_deriv {
@@ -74,13 +90,9 @@ pkgs.lib.makeExtensible
lint = mk_deriv {
name = "frama-c-lint";
src = self.src;
+ opamPackages = [ "ocp-indent=1.7.0" "headache=1.05"];
buildInputs =
- (self.mk_buildInputs {
- nixPackages = [ pkgs.bc ];
- opamPackages = [
- { name = "ocp-indent"; constraint = "=1.7.0"; }
- { name = "headache"; constraint = "=1.05"; }
- ];} );
+ self.mk_buildInputs { nixPackages = [ pkgs.bc ]; };
outputs = [ "out" ];
postPatch = ''
patchShebangs .
@@ -120,16 +132,13 @@ pkgs.lib.makeExtensible
installPhase = ''
true
'';
- };
+ } // { other-opam-selection = "main"; };
build-distrib-tarball = mk_deriv {
name = "frama-c-build-distrib-tarball";
src = self.src;
- buildInputs =
- (self.mk_buildInputs {
- opamPackages = [
- { name = "headache"; constraint = "=1.05"; }
- ];} );
+ buildInputs = self.buildInputs;
+ opamPackages = [ "headache=1.05" ];
outputs = [ "out" ];
postPatch = ''
patchShebangs .
@@ -152,6 +161,7 @@ pkgs.lib.makeExtensible
build-from-distrib-tarball = mk_deriv {
name = "frama-c-build-from-distrib-tarball";
buildInputs = self.buildInputs;
+ opamPackages = self.build-distrib-tarball.opamPackages;
src = self.build-distrib-tarball.out ;
outputs = [ "out" ];
configurePhase = ''
@@ -165,7 +175,7 @@ pkgs.lib.makeExtensible
installPhase = ''
true
'';
- };
+ } // { other-opam-selection = "build-distrib-tarball"; };
wp-qualif = mk_deriv {
name = "frama-c-wp-qualif";
@@ -193,7 +203,7 @@ pkgs.lib.makeExtensible
installPhase = ''
true
'';
- };
+ } // { other-opam-selection = "main"; };
aorai-prove = mk_deriv {
name = "frama-c-aorai-prove";
@@ -221,7 +231,7 @@ pkgs.lib.makeExtensible
installPhase = ''
true
'';
- };
+ } // { other-opam-selection = "main"; };
eva-tests = mk_deriv {
name = "frama-c-eva-tests";
@@ -266,17 +276,18 @@ pkgs.lib.makeExtensible
installPhase = ''
true
'';
- };
+ } // { other-opam-selection = "main"; };
internal = mk_deriv {
name = "frama-c-internal";
src = self.src;
- buildInputs = (self.mk_buildInputs { opamPackages = [ "xml-light" ]; } ) ++
- [ pkgs.getopt
- pkgs.libxslt pkgs.libxml2 pkgs.autoPatchelfHook
- pkgs.swiProlog
- stdenv.cc.cc.lib
- ];
+ opamPackages = [ "xml-light" ];
+ buildInputs =
+ self.mk_buildInputs
+ { nixPackages =
+ [ pkgs.getopt pkgs.libxslt pkgs.libxml2 pkgs.autoPatchelfHook
+ pkgs.swiProlog stdenv.cc.cc.lib ];
+ };
counter_examples_src = plugins.counter-examples.src;
genassigns_src = plugins.genassigns.src;
frama_clang_src = plugins.frama-clang.src;
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
index 65141e9684de9637e600df87397aeb97366afdbf..e083c89e2cd9b2e2f16c123ea6bb1f03598e8b42 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -1,13 +1,14 @@
#To copy in other repository
-{ pkgs ? import <nixpkgs> {}, password}:
+{ password}:
let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "f86e807d6f440ac4479b78f8419dfd817803419d";
- "ref" = "feature/wp/versions-bump";
+ "rev" = "c573f802c66f3821d0bac5f0b71eceaed26b26f1";
+ "ref" = "feature/upgrade-opam2nix";
};
+ pkgs = import "${src}/pkgs.nix" {};
in
{
src = src;