diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7c375041eb9b3d9ed859079db6569a59a888ef4d..f6b89686e1598260cc785f6c959b1c3674077d04 100644 --- a/.gitlab-ci.yml +++ b/.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 diff --git a/ci.sh b/ci.sh index bc15af5d5002e853cdfc090a8085992440bafd4e..58a060aba86b36248730867bcb690d9bb535696d 100755 --- a/ci.sh +++ b/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 diff --git a/nix/meta.nix b/nix/meta.nix index 0b4db6cc6464dea63b5762e81cd06456ceed01e8..e8e6641083da72eef6d01c2f67478a9d23548ee5 100644 --- a/nix/meta.nix +++ b/nix/meta.nix @@ -1,53 +1,11 @@ -{ 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 ; }