Merge branch 'feature/dune/nix-plugin-template' into 'feature/bobot/jbuilder'

Nix template for external plugins

See merge request frama-c/meta!65

.gitlab-ci.yml

@@ -6,9 +6,9 @@ stages:
 
 variables:
      DEFAULT: "feature/bobot/jbuilder"
+     OCAML: "4_12"
 #     CURRENT: $CI_COMMIT_REF_NAME
 #     FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
-#     OCAML: "4_08"
 
 ################################################################################
 ### TESTS

ci.sh

@@ -3,77 +3,39 @@
 set -euxo pipefail
 
 DEFAULT=${DEFAULT:-master}
+NIX_TARGET="meta"
+PLUGIN_DIR="$(dirname "$(readlink -f "$0")")"
+
+CURRENT_BRANCH="${CI_MERGE_REQUEST_SOURCE_BRANCH_NAME:-}"
+: "${CURRENT_BRANCH:="${CI_COMMIT_REF_NAME:-}"}"
+: "${CURRENT_BRANCH:="$(git branch --show-current)"}"
 
 # prints
-# - "$2" if it is a branch name in remote $1,
+# - "$CURRENT_BRANCH" if it is a branch name in remote $1,
 # - else "$DEFAULT" if it is set and $DEFAULT is a branch name in remote $1,
 # - else master
 get_matching_branch () {
-  if   git ls-remote --quiet --exit-code "$1" "$2" >/dev/null 2>/dev/null;
-  then echo "$2"
+  if   git ls-remote --quiet --exit-code "$1" "$CURRENT_BRANCH" >/dev/null 2>/dev/null;
+  then echo "$CURRENT_BRANCH"
+  elif git ls-remote --quiet --exit-code "$1" "$DEFAULT" >/dev/null 2>/dev/null;
+  then echo "$DEFAULT"
   else echo master
   fi
 }
 
-curdir="$(dirname "$(readlink -f "$0")")"
-git_current_branch="${CI_MERGE_REQUEST_TARGET_BRANCH_NAME:-}"
-: "${git_current_branch:="${CI_COMMIT_REF_NAME:-}"}"
-: "${git_current_branch:="$(git branch --show-current)"}"
-cd "$(mktemp -d)"
-
-### LOAD FRAMA-C
-
-# the hash of the derivation depends on the directory name
-mkdir frama-c
-framac_repo="$(readlink -f frama-c)"
-framac_url="git@git.frama-c.com:frama-c/frama-c.git"
-
-frama_c_branch="$(get_matching_branch "$framac_url" "$git_current_branch")"
-echo "using branch $frama_c_branch of frama-c repo at $framac_repo"
-# clone frama-c
-git clone --depth=1 --branch="$frama_c_branch" "$framac_url" "$framac_repo"
-
-OPTS="--arg frama-c-repo $framac_repo"
-
-### LOAD DEPENDENCIES
-
-declare -A deps=( )
-declare -A dirs=( )
-
-if [[ -f "$curdir/nix/dependencies" ]]; then
-  while read -r var value; do
-    deps[$var]=$value
-  done < "$curdir/nix/dependencies"
-
-  for repo in ${!deps[@]}; do
-    # the hash of the derivation depends on the directory name
-    mkdir $repo
-    directory="$(readlink -f $repo)"
-    dirs[$repo]=$directory
-
-    url=${deps[$repo]}
-    branch="$(get_matching_branch "$url" "$git_current_branch")"
-    echo "using branch $branch of $repo at $directory"
-    # clone
-    git clone --depth=1 --branch="$branch" "$url" "$directory"
-
-    OPTS="$OPTS --arg $repo $directory"
-  done
-fi
+TMP_DIR="$(mktemp -d)"
 
 cleanup () {
-  if [[ -n $framac_repo ]];
-  then rm -rf "$framac_repo"
-  fi
-
-  for repo in ${!dirs[@]}; do
-    if [[ -n ${dirs[$repo]} ]];
-    then rm -rf "${dirs[$repo]}"
-    fi
-  done
+  rm -rf $TMP_DIR
 }
 
 trap cleanup EXIT
 
-# run the build
-nix-build --no-out-link "$curdir/nix/pkgs.nix" $OPTS -A ocaml-ng.ocamlPackages_4_12.meta
+mkdir -p $TMP_DIR/frama-ci
+frama_ci_repo="$(readlink -f $TMP_DIR/frama-ci)"
+frama_ci_url="git@git.frama-c.com:frama-c/Frama-CI.git"
+frama_ci_branch="$(get_matching_branch "$frama_ci_url")"
+echo "using branch $frama_ci_branch of Frama-CI repo at $frama_ci_repo"
+git clone --depth=1 --branch="$frama_ci_branch" "$frama_ci_url" "$frama_ci_repo"
+
+source $frama_ci_repo/common-plugin-ci.sh

nix/meta.nix

-{ lib
-, stdenv
-, frama-c
+{ mk_plugin
 , gitignoreSource
-, alt-ergo
 , swiProlog
-, time
 }:
 
-stdenv.mkDerivation {
-  name = "meta";
-  src = gitignoreSource ./..;
-
-  buildInputs = frama-c.buildInputs ++ [
-    frama-c
-  ];
-  checkInputs = [
-    alt-ergo
-    swiProlog
-    time
-  ];
-
-  # Do not use default parallel building, but allow 2 cores for Frama-C build
-  enableParallelBuilding = false;
-  buildPhase = ''
-    runHook preBuild
-    dune build -j2 --display short @install
-    runHook postBuild
-  '';
-
-  postBuild = ''
-    patchShebangs .
-  '';
-
-  preCheck = ''
-    echo "Patching"
-  '';
-
-  doCheck = true;
-  checkPhase = ''
-    # Setup Why3
-    mkdir home
-    HOME=$(pwd)/home
-    why3 config detect
-    # Test
-    make run-ptests
-    dune build -j1 --display short @tests/ptests
-  '';
-
-  installPhase = ''
-    touch $out
-  '';
+mk_plugin {
+  plugin-name = "metacsl" ;
+  plugin-src = gitignoreSource ./.. ;
+  additional-check-inputs = [ swiProlog ] ;
+  has-wp-proofs = true ;
 }