.gitlab-ci.yml

stages:
  - build
  - test
  - test-2
  - deploy

# We are using a Docker image that has GHC and Cabal preinstalled.
.haskell:
  image: haskell:8.6.5

# For some jobs we need a Docker image that has Coq preinstalled.
.coq:
  image: coqorg/coq:8.8.2

###############################################################################
# Dependencies                                                                #
###############################################################################

# We want to avoid recompiling dependencies on subsequent runs of the pipeline.
# Thus we save the Cabal directory to the GitLab CI cache. Because we cannot
# cache files outside of the repository, we need to explicitly move the cabal
# directory into our repository.

.cabal-cache:
  cache:
    key: ${CI_COMMIT_REF_SLUG}
    paths:
      - ./dist-newstyle
      - ./.cabal
  before_script:
    - mv ./.cabal /root/.cabal || true
    - echo "Building dependencies..."
    - cabal new-update
    - cabal new-build --only-dependencies
  after_script:
    - mv /root/.cabal ./.cabal

###############################################################################
# Unit tests                                                                  #
###############################################################################

# Compile unit tests.
build-unit-tests:
  extends:
    - .haskell
    - .cabal-cache
  stage: build
  script:
    - echo "Building unit tests..."
    - cabal new-build unit-tests
    - echo "Copy unit test executable to build directory..."
    - mkdir -p ./build/bin
    - cp $(find dist-newstyle -name unit-tests -type f) ./build/bin/unit-tests
  artifacts:
    name: unit-tests
    paths:
      - ./build/bin/unit-tests

# Run unit tests.
run-unit-tests:
  extends: .haskell
  stage:  test
  dependencies:
    - build-unit-tests
  script:
    - echo "Running unit tests..."
    - ./build/bin/unit-tests

###############################################################################
# Executable                                                                  #
###############################################################################

# Compile Haskell to Coq compiler.
build-compiler:
  extends:
    - .haskell
    - .cabal-cache
  stage: build
  script:
    - echo "Building compiler..."
    - cabal new-build haskell-to-coq-compiler
    - echo "Copy executable to build directory..."
    - mkdir -p ./build/bin
    - cp $(find dist-newstyle -name haskell-to-coq-compiler -type f) ./build/bin/haskell-to-coq-compiler
  artifacts:
    name: compiler
    paths:
      - ./build/bin/haskell-to-coq-compiler

###############################################################################
# Documentation                                                               #
###############################################################################

# Build Haddock documentation.
build-docs:
  extends:
    - .haskell
    - .cabal-cache
  stage: build
  script:
    - echo "Building Haddock documentation..."
    - cabal new-haddock --haddock-hyperlink-source
    - echo "Copy documentation to build directory..."
    - mkdir -p ./build/docs
    - cp -r $(dirname $(find dist-newstyle -name "index.html"))/. ./build/docs
  artifacts:
    name: docs
    paths:
      - ./build/docs

# Deploy documentation to `https://$SSH_DEPLOY_HOST/$CI_COMMIT_REF_SLUG/docs`.
deploy-docs:
  extends: .ssh-deploy
  stage: deploy
  dependencies:
    - build-docs
  script:
    - cp -r ./build/docs $DEPLOY_DIR

###############################################################################
# Base library                                                                #
###############################################################################

# Build the Coq Base library.
build-base-library:
  extends: .coq
  stage: build
  script:
    - ./tool/compile-coq.sh base
    - mkdir -p ./build/base
    - cp --parents $(find base -name "*.vo" -or -name "*.glob") ./build
  artifacts:
    name: coq-base-library
    paths:
      - ./build/base

###############################################################################
# Examples                                                                    #
###############################################################################

# Tests the Haskell to Coq compiler with the example modules.
# The artifacts contain the generated `.v` files.
test-examples:
  extends: .haskell
  stage: test
  dependencies:
    - build-compiler
  script:
    - ./build/bin/haskell-to-coq-compiler --transform-pattern-matching --dump-transformed-modules example/transformed -b ./base -o ./example/generated $(find ./example -name "*.hs")
    - mkdir -p ./build/example
    - mkdir -p ./build/example_transformed
    - cp -r ./example/generated ./build/example
    - cp -r ./example/transformed ./build/example_transformed
  artifacts:
    name: examples
    paths:
      - ./build/example
      - ./build/example_transformed

# This job verifies that the Coq code generated during `test-examples` compiles
# and the proofs for the QuickCheck properties pass.
test-generated-code:
  extends: .coq
  stage: test-2
  dependencies:
    - build-base-library
    - test-examples
  script:
    - cp -r ./build/base/. ./base # Restore compiled base library.
    - cp -r ./build/example ./example/generated # Restore compiled examples.
    - ./tool/compile-coq.sh ./example # Compile tests and generated Coq files.

###############################################################################
# SSH Deploy                                                                  #
###############################################################################

# Common parent for jobs of the `deploy` stage that require a minimal docker
# image that has a preinstalled an OpenSSH client.
#
# The server and authentication information is controlled by the following
# variables that should be configured in the GitLab CI web interface.
#
#   * `$SSH_DEPLOY_HOST` name of the host to connect to.
#   * `$SSH_DEPLOY_USER` name of the user on the host to authenticate as.
#      There should be a folder `html` in the home directory of this user,
#      where deployed files can be placed into.
#   * `$SSH_DEPLOY_KEY` private SSH key to use for authentication.
#      The corresponding public key should be listed in the
#      `~/.ssh/authorized_keys` file of the user.
#
# Since, the variables contain sensitive information, they should be
# made available to protected branches and tags only.
# Thus, jobs that extend `.ssh-deploy` are should run for protected branches
# and tags only.
#
# Before the script of the inheriting job is executed the directory
# `$DEPLOY_DIR` is created. All files copied to this directory will be
# uploaded to `$TARGET_DIR` after the script is done.
.ssh-deploy:
  image: jaromirpufler/docker-openssh-client
  variables:
    SERVER: ${SSH_DEPLOY_USER}@${SSH_DEPLOY_HOST}
    TARGET_DIR: html/${CI_COMMIT_REF_SLUG}
    DEPLOY_DIR: "${CI_PROJECT_DIR}/ssh-deploy"
  only:
    variables:
      - "$CI_COMMIT_REF_PROTECTED"
  before_script:
    - mkdir "$DEPLOY_DIR"
  after_script:
    - ssh $SERVER "mkdir -p $TARGET_DIR"
    - scp -r $DEPLOY_DIR/* $SERVER:$TARGET_DIR
  environment:
    name: $CI_COMMIT_REF_NAME
    url: https://${SSH_DEPLOY_HOST}/${CI_COMMIT_REF_SLUG}
    on_stop: stop-ssh-deploy

# Removes deployed files (see `.ssh-deploy`) from the server when a branch gets
# deleted.
stop-ssh-deploy:
  image: jaromirpufler/docker-openssh-client
  stage: deploy
  when: manual
  dependencies: []
  variables:
    GIT_STRATEGY: none
    SERVER: ${SSH_DEPLOY_USER}@${SSH_DEPLOY_HOST}
    TARGET_DIR: html/${CI_COMMIT_REF_SLUG}
  script:
    - ssh $SERVER "rm -r $TARGET_DIR"
  environment:
    name: $CI_COMMIT_REF_NAME
    action: stop