.gitlab-ci.yml

################################################################################
### STAGES

stages:
  - prepare
  - build
  - tests
  - distrib
  - compatibility
  - release
  - publish

################################################################################
### DEFAULT JOB PARAMETERS

default:
  interruptible: true
  tags: [ nix-v2 ]

################################################################################
### VARIABLES

variables:
  DEFAULT: "master"
  OCAML: "4.11"
  PUBLISH: "no"
  RELEASE: "no"

################################################################################
### PREPARE

check-no-old-frama-c:
  stage: prepare
  script:
    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a HEAD)
    - git merge-base --is-ancestor a35d2118fe6999dddce9e1847eff626fae9cc37c HEAD

.build_template: &do_not_stop_pipeline_template
  stage: prepare
  interruptible: false
  script:
    - echo "This pipeline won't be interrupted"

unstoppable-pipeline:
  <<: *do_not_stop_pipeline_template
  only:
    variables:
      - $DEFAULT == $CI_COMMIT_BRANCH

do-not-stop-pipeline:
  <<: *do_not_stop_pipeline_template
  when: manual
  except:
    variables:
      - $DEFAULT == $CI_COMMIT_BRANCH

check-publish:
  stage: prepare
  script: >
    [[ "$RELEASE" == "no" ]] &&
    [[ "$DEFAULT" == "$CI_COMMIT_BRANCH" ]] &&
    [[ "$DEFAULT" == "master" ]]
  only:
    variables:
      - $PUBLISH == "yes"

check-release:
  stage: prepare
  script: >
    [[ "$PUBLISH" == "no" ]] &&
    [[ "$DEFAULT" == "$CI_COMMIT_BRANCH" ]] &&
    [[ "$DEFAULT" == "stable/$(cat VERSION_CODENAME | tr '[:upper:]' '[:lower:]')" ]] &&
    [[ "$(git describe --tag)" == "$(cat VERSION | sed 's/~/-/')" ]] &&
    [[ "$(cat VERSION)" == "$(cat opam | grep "^version" | sed 's/version: \"\(.*\)\"/\1/')" ]]
  only:
    variables:
      - $RELEASE == "yes"

# Observed: when several shell with same dependencies are started, deadlock may
#           occur when building these dependencies. We build these dependencies
#           before running the rest of the pipeline to avoid that.
prepare-shell-checkers:
  stage: prepare
  script:
    - ./nix/shell-checkers.sh "true"

################################################################################
### BUILD

frama-c:
  stage: build
  script:
    - ./nix/build-proxy.sh frama-c
  artifacts:
    when: on_failure
    paths:
      - commits.nix
      - results.log
    expire_in: 1 day

ivette:
  stage: build
  image: node:lts-gallium
  cache:
    paths:
      - ivette/node_modules/
  script:
    - node --version
    - npm --version
    - yarn --version
    - make -C ivette
  tags:
    - docker

################################################################################
### TESTS

check-ts-api:
  stage: tests
  script:
    - ./nix/build-proxy.sh ts-api

e-acsl-tests:
  stage: tests
  script:
    - ./nix/build-proxy.sh e-acsl-tests

.build_template: &eva_template
  stage: tests
  script:
    - ./nix/build-proxy.sh eva-$CONFIG-tests

eva-default-tests:
  variables:
    CONFIG: "default"
  <<: *eva_template

.build_template: &eva_domains
  parallel:
    matrix:
      - CONFIG: [
          "apron",
          "bitwise",
          "equality",
          "gauges",
          "multidim",
          "octagon",
          "symblocs"
        ]

eva-domains:
  <<: *eva_template
  <<: *eva_domains
  only:
    variables:
      - $CI_COMMIT_BRANCH =~ /.*[-_\/.][Ee]va[-_\/.].*/
      - $CI_COMMIT_BRANCH =~ /^[Ee]va[-_\/.].*/
      - $CI_COMMIT_BRANCH =~ /.*[-_\/.][Ee]va$/

eva-domains-nightly:
  <<: *eva_template
  <<: *eva_domains
  only:
    refs:
      - schedules

eva-domains-release:
  <<: *eva_template
  <<: *eva_domains
  only:
    variables:
      - $RELEASE == "yes"

kernel-tests:
  stage: tests
  script:
    - ./nix/build-proxy.sh kernel-tests

plugins-tests:
  stage: tests
  script:
    - ./nix/build-proxy.sh plugins-tests

wp-tests:
  stage: tests
  script:
    - ./nix/build-proxy.sh wp-tests

external-plugins:
  stage: tests
  script:
    - ./nix/external-plugin-ci.sh $PLUGIN
  parallel:
    matrix:
      - PLUGIN: [
          "acsl-importer",
          "caveat-importer",
          "context-from-precondition",
          "frama-clang",
          "genassigns",
          "linea-cabs",
          "meta",
          "minimal",
          "mthread",
          "security",
          "volatile"
        ]

################################################################################
### DISTRIB

# API documentation

api-doc: # Note: the Nix store avoids rebuilding
  stage: distrib
  variables:
    OUT: "api"
  script:
    - ./nix/build-proxy.sh api-doc
  artifacts:
    paths:
      - api/frama-c-api.tar.gz
      - api/frama-c-server-api.tar.gz
    expire_in: 7 days

# Build distribution tarball

build-distrib-tarball:
  stage: distrib
  variables:
    OPEN_SOURCE: "yes"
    CI_LINK: "yes"
    HDRCK: "frama-c-hdrck"
  script:
    - ./nix/shell-checkers.sh "./dev/make-distrib.sh"
  artifacts:
    paths:
      - ./*.tar.gz
    expire_in: 1 week

# Check files header

header-check:
  stage: distrib
  variables:
    FRAMAC_HDRCK: ""
  script:
    - ./nix/shell-checkers.sh "make -f share/Makefile.headers check-headers"

# Lint files

lint:
  stage: distrib
  variables:
    LINT_MAKEFILE: "share/Makefile.linting"
  script:
    - ./nix/shell-checkers.sh "make -f share/Makefile.linting check-lint"

# Manuals

.build_template: &manuals_template
  stage: distrib
  variables:
    OUT: "manuals"
  script:
    - ./nix/build-proxy.sh manuals
  artifacts:
    paths:
      - manuals/*.pdf
      - manuals/*.tar.gz
      - manuals/*.txt
    expire_in: 7 days # Note: the LAST artifact of the ref is always kept

manuals:
  <<: *manuals_template
  except:
    variables:
      - $RELEASE == "yes"
  when: manual

manuals-for-release:
  <<: *manuals_template
  only:
    variables:
      - $RELEASE == "yes"

release-content:
  stage: distrib
  script:
    - ./nix/shell-checkers.sh "./dev/build-release.sh"
  needs:
    - api-doc
    - build-distrib-tarball
    - manuals-for-release
  artifacts:
    paths:
      - website
      - wiki
      - opam-repository
      - release-data.json
  only:
    variables:
      - $RELEASE == "yes"

################################################################################
### COMPATIBILITY

# Internalized plugins tests

.build_template: &internal_template
  stage: compatibility
  script:
    - ./nix/internal-tests.sh

internal:
  <<: *internal_template
  when: manual
  except:
    - schedules

internal_nightly:
  <<: *internal_template
  # The Opam target may affect this job
  timeout: 2h
  only:
    - schedules

# OCaml versions

.build_template: &ocaml_always_additional_versions_template
  parallel:
    matrix:
      - OCAML: ["4.14"]

.build_template: &ocaml_manual_additional_versions_template
  parallel:
    matrix:
      - OCAML: ["4.12", "4.13"]
  when: manual

.build_template: &ocaml_versions_template
  stage: compatibility
  script:
    - ./nix/build-proxy.sh default-config-tests

ocaml-versions:
  <<: *ocaml_versions_template
  <<: *ocaml_always_additional_versions_template
  # in schedules, each OCAML is tested in its own complete pipeline
  except:
    - schedules

ocaml-versions-more:
  <<: *ocaml_versions_template
  <<: *ocaml_manual_additional_versions_template

ocaml-versions-nightly:
  <<: *ocaml_versions_template
  <<: *ocaml_always_additional_versions_template
  # we still check them for the publisher pipeline job
  only:
    variables:
      - $PUBLISH == "yes"

# Opam pin

.build_template: &opam_pin_template
  stage: compatibility
  image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
  script:
    - sudo apt update
    - opam pin . -n
    - opam depext frama-c --with-test
    - opam install --jobs 2 frama-c --with-test
    - frama-c -version
  tags:
    - docker

opam-pin:
  <<: *opam_pin_template
  except:
    refs:
      - schedules
    variables:
      - $RELEASE == "yes"
  when: manual

opam-pin-nightly:
  <<: *opam_pin_template
  only:
    refs:
      - schedules

opam-pin-release:
  <<: *opam_pin_template
  only:
    variables:
      - $RELEASE == "yes"

# TODO: Enable this rule later:
#
# opam-pin-minimal:
#   variables:
#     OPAMSOLVERTIMEOUT: "500"
#     OPAMCRITERIA: "+count[version-lag,solution]"
#     OPAMEXTERNALSOLVER: "builtin-0install"
#   stage: prepare
#   image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
#   script:
#     - sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam
#     - opam --version
#     - opam init --reinit -ni
#     - opam pin . -n
#     - opam depext frama-c --with-test
#     - opam install --jobs 2 frama-c --with-test
#   tags:
#     - docker

# Distrib

.build_template: &src_distrib_tests_template
  stage: compatibility
  variables:
    DIR: "extracted"
  script:
    - mkdir $DIR && tar -xzf frama-c.tar.gz --strip-components 1 -C ./extracted
    - ./nix/build-proxy.sh src-distrib-tests

src-distrib-tests:
  <<: *src_distrib_tests_template
  except:
    refs:
      - schedules
    variables:
      - $RELEASE == "yes"

src-distrib-tests-scheduled:
  <<: *src_distrib_tests_template
  # The Opam target may affect this job
  timeout: 2h
  only:
    refs:
      - schedules

src-distrib-tests-release:
  <<: *src_distrib_tests_template
  # The Opam target may affect this job
  timeout: 2h
  only:
    variables:
      - $RELEASE == "yes"

################################################################################
### RELEASE

.build_template: &prepare_ssh_template
  before_script:
    - export GIT_SSH=$PWD/nix/frama-c-public/ssh.sh

release-branch:
  stage: release
  variables:
    REPOSITORY: "frama-c"
  <<: *prepare_ssh_template
  script:
    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/$CI_COMMIT_BRANCH)
    - BRANCH="$CI_COMMIT_BRANCH" nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
    # Note: BRANCH must be defined here, since we cannot *evaluate* a variable in 'variables'
  only:
    variables:
      - $RELEASE == "yes"
  when: manual
  interruptible: false

release-create:
  stage: release
  <<: *prepare_ssh_template
  script:
    - nix-shell -p git git-lfs coreutils openssh curl --run './nix/frama-c-public/publish-release.sh'
  needs:
    - release-branch
    - release-content
  only:
    variables:
      - $RELEASE == "yes"
  when: manual
  interruptible: false

release-opam:
  stage: release
  <<: *prepare_ssh_template
  script:
    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-opam.sh'
  only:
    variables:
      - $RELEASE == "yes"
  interruptible: false

release-website:
  stage: release
  <<: *prepare_ssh_template
  script:
    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-website.sh'
  only:
    variables:
      - $RELEASE == "yes"
  interruptible: false

release-wiki:
  stage: release
  <<: *prepare_ssh_template
  script:
    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-wiki.sh'
  only:
    variables:
      - $RELEASE == "yes"
  interruptible: false

################################################################################
### PUBLISH

# publish stage is used to push the current master branch of Frama-C and
# associated plugins from the internal frama-c group to the public pub group.
#
# For that, it uses the 'frama-c to frama-c-public' publish key. Thus, to publish
# a new plugin (while keeping its main repository internal), you can add a new
# target to this stage, adapting the script for MetAcsl or Frama-Clang to your
# own plugin.
#
# You must also activate the publish key on both frama-c/my_plugin
# and pub/my_plugin repositories (the former should be read-only, the latter
# must provide write access to the publish key).
# Do not forget to trigger the target only on schedules, so that all public
# repositories stay synchronized.

publish-frama-c:
  stage: publish
  variables:
    BRANCH: "master"
    REPOSITORY: "frama-c"
  <<: *prepare_ssh_template
  script:
    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/master)
    -  nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
  only:
    variables:
      - $PUBLISH == "yes"
  interruptible: false

publish-fclang:
  stage: publish
  variables:
    BRANCH: "master"
    REPOSITORY: "frama-clang"
  <<: *prepare_ssh_template
  script:
    - nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
  only:
    variables:
      - $PUBLISH == "yes"
  interruptible: false

publish-meta:
  stage: publish
  variables:
    BRANCH: "master"
    REPOSITORY: "meta"
  <<: *prepare_ssh_template
  script:
    - nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
  only:
    variables:
      - $PUBLISH == "yes"
  interruptible: false