.gitlab-ci.yml

#
# Copyright (C) BedRock Systems Inc. 2019-2020
#
# SPDX-License-Identifier:AGPL-3.0-or-later
#
################################################
# This file configures the cpp2v CI/CD pipelines.
#
# There are two pipelines:
#
#   1. build_latest -> test_latest
#
#      This builds and tests cpp2v against the current
#      major version of llvm.
#
#   2. build_previous -> test_previous
#
#      This builds cpp2v against the previous major
#      version of llvm. It tests only the cpp2v
#      frontend.
#
# The build* jobs extend the .build template job.
# The test* jobs extend the .test template job.
#
# NOTE: If you need to change the base software in a
# container image used in a pipeline, first update
# Dockerfile and push a new image to the registry
# (see Dockerfile for more information).
################################################

variables:
  LLVM_CUR_MAJ_VER: "10"
  LLVM_PREV_MAJ_VER: "9"

stages:
  - build
  - test
  - release
#  - pages

#This is a template job that's extended below by the real jobs
# build_cur and build_prev (see, e.g., https://docs.gitlab.com/ee/ci/yaml/#extends).
.build:
  image: registry.gitlab.com/bedrocksystems/docker-image:cpp2v-llvm${LLVM_MAJ_VER}
  stage: build
  script:
    - mkdir -p build; cd build; CC=`llvm-config-${LLVM_MAJ_VER} --bindir`/clang CXX=`llvm-config-${LLVM_MAJ_VER} --bindir`/clang++ cmake -DLLVM_CONFIG=`which llvm-config-${LLVM_MAJ_VER}` ../; cd ..
    - make -j ${NJOBS} cpp2v
    - make -j ${NJOBS} plugin coq
    - rm -f build/bedrock
    - cp -r theories build/bedrock
  artifacts:
    name: cpp2v-${LLVM_MAJ_VER}
    paths:
      - build/cpp2v
      - build/libcpp2v_plugin.so
      - build/bedrock

.test:
  image: registry.gitlab.com/bedrocksystems/docker-image:cpp2v-llvm${LLVM_MAJ_VER}
  stage: test
  script:
    - coqc -v
    - opam list
    - ./build/cpp2v --cpp2v-version 0 --
    - PATH=`llvm-config-${LLVM_MAJ_VER} --bindir`:`pwd`/build:$PATH make -C cpp2v-tests -j ${NJOBS} TIMED=1 QPATH=`pwd`/build/bedrock
    - PATH=`llvm-config-${LLVM_MAJ_VER} --bindir`:`pwd`/build:$PATH make -C plugin-tests -j ${NJOBS} TIMED=1 QPATH=`pwd`/build/bedrock
  only:
    - merge_requests
  except:
    variables:
      - $CI_MERGE_REQUEST_TITLE =~ /^WIP:/

build_latest:
  extends: .build
  rules:
    - if: $CI_MERGE_REQUEST_IID
    - if: $CI_COMMIT_TAG
    - if: $CI_COMMIT_BRANCH # == $CI_DEFAULT_BRANCH
  variables:
    LLVM_MAJ_VER: ${LLVM_CUR_MAJ_VER}

build_previous:
  extends: .build
  only:
    - schedules
    - merge_requests
    - tags
    - master
  variables:
    LLVM_MAJ_VER: ${LLVM_PREV_MAJ_VER}

test_latest:
  extends: .test
  dependencies:
    - build_latest
  variables:
    LLVM_MAJ_VER: ${LLVM_CUR_MAJ_VER}

test_previous:
  extends: .test
  dependencies:
    - build_previous
  variables:
    LLVM_MAJ_VER: ${LLVM_PREV_MAJ_VER}

.release:
  stage: release
  script:
    - cp -r build cpp2v-core
  artifacts:
    name: cpp2v-${LLVM_MAJ_VER}
    paths:
      - cpp2v-core/cpp2v
      - cpp2v-core/libcpp2v_plugin.so
      - cpp2v-core/bedrock
  only:
    - tags
    - master

release_latest:
  extends: .release
  dependencies:
    - build_latest
  variables:
    LLVM_MAJ_VER: ${LLVM_CUR_MAJ_VER}

release_previous:
  extends: .release
  dependencies:
    - build_previous
  variables:
    LLVM_MAJ_VER: ${LLVM_PREV_MAJ_VER}




# pages:
#   image: registry.gitlab.com/bedrocksystems/docker-image:cpp2v-llvm${LLVM_CUR_MAJ_VER}
#   stage: pages
#   dependencies:
#     - test_latest
#   script:
#     # this line refreshes the artifact to avoid rebuilding the coq code
#     - make touch_deps
#     - make public
#   only:
#     - master
#   artifacts:
#     paths:
#       - public