.gitlab-ci.yml

image: "$IMAGE"

stages:
  - docker
  - build
  - deploy

# When a job has no dependencies, it goes to stage 1. Otherwise, we
# set "needs" to contain all transitive dependencies (with "artifacts:
# false" when we don't want the artifacts). We include the transitive
# dependencies due to gitlab bugs sometimes starting the job even if a
# transitive dep failed, see #10699 / 7b59d8c9d9b2104de7162ec0e40f6182a6830046.

# some default values
variables:
  # Format: $IMAGE-V$DATE-$hash
  # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
  # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
  CACHEKEY: "bionic_coq-V2021-07-23-66f5817edb"
  IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
  # By default, jobs run in the base switch; override to select another switch
  OPAM_SWITCH: "base"
  # Used to select special compiler switches such as flambda, 32bits, etc...
  OPAM_VARIANT: ""
  GIT_DEPTH: "10"

include:
  - local: '/dev/bench/gitlab-bench.yml'

docker-boot:
  stage: docker
  image: docker:stable
  services:
    - docker:dind
  before_script: []
  script:
    - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
    - cd dev/ci/docker/bionic_coq/
    - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
    - docker build -t "$IMAGE" .
    - docker push "$IMAGE"
  except:
    variables:
      - $SKIP_DOCKER == "true"
      - $ONLY_WINDOWS == "true"
  tags:
    - docker

before_script:
  - cat /proc/{cpu,mem}info || true
  - ls -a # figure out if artifacts are around
  - printenv -0 | sort -z | tr '\0' '\n'
  - declare -A switch_table
  - switch_table=( ["base"]="$COMPILER" ["edge"]="$COMPILER_EDGE" )
  - opam switch set -y "${switch_table[$OPAM_SWITCH]}$OPAM_VARIANT"
  - eval $(opam env)
  - opam list
  - opam config list
  - dev/tools/check-cachekey.sh

################ GITLAB CACHING ######################
# - use artifacts between jobs                       #
######################################################

# TODO figure out how to build doc for installed Coq
.build-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci
      - config/Makefile
      - config/coq_config.py
      - config/coq_config.ml
      - config/dune.c_flags
      - dmesg.txt
    expire_in: 1 month
  script:
    - set -e

    - echo 'start:coq.clean'
    - make clean # ensure that `make clean` works on a fresh clone
    - echo 'end:coq.clean'

    - echo 'start:coq.config'
    - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" $COQ_EXTRA_CONF
    - echo 'end:coq.config'

    - echo 'start:coq.build'
    - make -j "$NJOBS" world $EXTRA_TARGET
    - echo 'end:coq:build'

    - echo 'start:coq.install'
    - make install $EXTRA_INSTALL
    - echo 'end:coq.install'

    - set +e

# Template for building Coq + stdlib, typical use: overload the switch
.dune-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  script:
    # flambda can be pretty stack hungry, specially with -O3
    # See also https://github.com/ocaml/ocaml/issues/7842#issuecomment-596863244
    # and https://github.com/coq/coq/pull/11916#issuecomment-609977375
    - ulimit -s 16384
    - set -e
    - make -f Makefile.dune world
    - set +e
    - tar cfj _build.tar.bz2 _build
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  artifacts:
    name: "$CI_JOB_NAME"
    when: always
    paths:
      - _build/log
      - _build.tar.bz2
    expire_in: 1 month

.dune-ci-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  needs:
    - build:edge+flambda:dune:dev
  script:
    - tar xfj _build.tar.bz2
    - set -e
    - echo 'start:coq.test'
    - make -f Makefile.dune "$DUNE_TARGET"
    - echo 'end:coq.test'
    - set +e
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  artifacts:
    when: always
    name: "$CI_JOB_NAME"
    expire_in: 2 months

# every non build job must set "needs" otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail.

.doc-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  needs:
    - not-a-real-job
  script:
    - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/"'
    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
    - make install-doc-sphinx
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci/share/doc/coq/
    expire_in: 2 months

# set "needs" when using
.test-suite-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  needs:
    - not-a-real-job
  script:
    - cd test-suite
    - make clean
    # careful with the ending /
    - BIN=$(readlink -f ../_install_ci/bin)/
    - LIB=$(readlink -f ../_install_ci/lib/coq)/
    - export OCAMLPATH=$(readlink -f ../_install_ci/lib/):"$OCAMLPATH"
    - COQEXTRAFLAGS="${COQEXTRAFLAGS}" make -j "$NJOBS" BIN="$BIN" COQLIB="$LIB" all
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - test-suite/logs
    # Gitlab doesn't support yet "expire_in: never" so we use the instance default
    # expire_in: never

# set "needs" when using
.validate-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  needs:
    - not-a-real-job
  script:
    # exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
    # the validate:quick job is sometimes started before build:quick, without artifacts
    # we ignore these spurious errors so if the job fails it's a real error
    - cd _install_ci || exit 0
    - find lib/coq/ -name '*.vo' -fprint0 vofiles
    - xargs -0 --arg-file=vofiles bin/coqchk -o -m -coqlib lib/coq/ > ../coqchk.log 2>&1 || touch coqchk.failed
    - tail -n 1000 ../coqchk.log # the log is too big for gitlab so pipe to a file and display the tail
    - "[ ! -f coqchk.failed ]" # needs quoting for yml syntax reasons
  artifacts:
    name: "$CI_JOB_NAME.logs"
    paths:
      - coqchk.log
    expire_in: 2 months

.ci-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  script:
    - set -e
    - echo 'start:coq.test'
    - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
    - echo 'end:coq.test'
    - set +e
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci
    when: always
  needs:
    - build:base

.ci-template-flambda:
  extends: .ci-template
  needs:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"

.deploy-template:
  stage: deploy
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  before_script:
    - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
    - eval $(ssh-agent -s)
    - mkdir -p ~/.ssh
    - chmod 700 ~/.ssh
    - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts
    - git config --global user.name "coqbot"
    - git config --global user.email "coqbot@users.noreply.github.com"

build:base:
  extends: .build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
    # coqdoc for stdlib, until we know how to build it from installed Coq
    EXTRA_TARGET: "doc-stdlib"
    EXTRA_INSTALL: "install-doc-stdlib-html install-doc-printable"

# no coqide for 32bit: libgtk installation problems
build:base+32bit:
  extends: .build-template
  variables:
    OPAM_VARIANT: "+32bit"
    COQ_EXTRA_CONF: "-native-compiler yes"
  only: &full-ci
    variables:
      - $FULL_CI == "true"

build:edge+flambda:
  extends: .build-template
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"

build:edge+flambda:dune:dev:
  extends: .dune-template

build:base+async:
  extends: .build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
    COQUSERFLAGS: "-async-proofs on"
  after_script:
    - dmesg > dmesg.txt
  timeout: 100m
  allow_failure: true # See https://github.com/coq/coq/issues/9658
  only:
    variables:
      - $UNRELIABLE =~ /enabled/
  artifacts:
    when: always

build:quick:
  extends: .build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler no"
    QUICK: "1"
  after_script:
    - dmesg > dmesg.txt
  timeout: 100m
  allow_failure: true # See https://github.com/coq/coq/issues/9637
  only:
    variables:
      - $UNRELIABLE =~ /enabled/
  artifacts:
    when: always

lint:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  script: dev/lint-repository.sh
  variables:
    GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"

pkg:opam:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  # OPAM will build out-of-tree so no point in importing artifacts
  script:
    - set -e
    - opam pin add --kind=path coq-core.dev .
    - opam pin add --kind=path coq-stdlib.dev .
    - opam pin add --kind=path coqide-server.dev .
    - opam pin add --kind=path coqide.dev .
    - set +e
  variables:
    OPAM_SWITCH: "edge"
    OPAM_VARIANT: "+flambda"
  only: *full-ci

.nix-template:
  stage: build
  needs: []
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git
  variables:
    GIT_STRATEGY: none # Required because we don't have git
    USER: root # Variable required by Cachix
  before_script:
    - cat /proc/{cpu,mem}info || true
    # Use current worktree as tmpdir to allow exporting artifacts in case of failure
    - export TMPDIR=$PWD
    # Install Cachix as documented at https://github.com/cachix/cachix
    - nix-env -iA cachix -f https://cachix.org/api/v1/install
    - cachix use coq
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - nix-build-coq.drv-0/*/test-suite/logs
    # Gitlab doesn't support yet "expire_in: never" so we use the instance default
    # expire_in: never

pkg:nix:deploy:
  extends: .nix-template
  environment:
    name: cachix
    url: https://coq.cachix.org
  script:
    - nix-build https://coq.inria.fr/nix/toolbox --arg override "{coq = coq:$CI_COMMIT_SHA;}" -K | cachix push coq
  only:
    - master
    - /^v.*\..*$/
  # In the future, add a condition to also have $CACHIX_AUTH_TOKEN set.
  # At the time of writing, we still rely on $CACHIX_SIGNING_KEY for Coq's Cachix.

pkg:nix:deploy:channel:
  extends: .deploy-template
  environment:
    name: cachix
    url: https://coq.cachix.org
  only:
    refs: # Repeat conditions from pkg:nix:deploy
      - master
      - /^v.*\..*$/
    variables:
      - $CACHIX_DEPLOYMENT_KEY
  needs:
    - pkg:nix:deploy
  script:
    - echo "$CACHIX_DEPLOYMENT_KEY" | tr -d '\r' | ssh-add - > /dev/null
    # Remove all pr branches because they could be missing when we run git fetch --unshallow
    - git branch --list 'pr-*' | xargs -r git branch -D
    - git fetch --unshallow
    - git branch -v
    - git push git@github.com:coq/coq-on-cachix "${CI_COMMIT_SHA}":"refs/heads/${CI_COMMIT_REF_NAME}"

pkg:nix:
  extends: .nix-template
  script:
    - nix-build "$CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz" -K

doc:refman:
  extends: .doc-template
  needs:
    - build:base

doc:refman:dune:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: refman-html
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/refman-html

doc:refman-pdf:dune:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: refman-pdf
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/refman-pdf

# currently bugged: dune cleans up the glob files so no links
# see #12699
doc:stdlib:dune:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: stdlib-html
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/stdlib/html

doc:refman:deploy:
  extends: .deploy-template
  environment:
    name: deployment
    url: https://coq.github.io/
  only:
    variables:
      - $DOCUMENTATION_DEPLOY_KEY
  needs:
    - doc:ml-api:odoc
    - doc:refman:dune
    - build:base
  script:
    - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
    - git clone git@github.com:coq/doc.git _deploy
    - rm -rf _deploy/$CI_COMMIT_REF_NAME/api
    - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman
    - rm -rf _deploy/$CI_COMMIT_REF_NAME/stdlib
    - mkdir -p _deploy/$CI_COMMIT_REF_NAME
    - cp -rv _build/default/_doc/_html _deploy/$CI_COMMIT_REF_NAME/api
    - cp -rv _build/default/doc/refman-html _deploy/$CI_COMMIT_REF_NAME/refman
    - cp -rv _install_ci/share/doc/coq/html/stdlib _deploy/$CI_COMMIT_REF_NAME/stdlib
    - cd _deploy/$CI_COMMIT_REF_NAME/
    - git add api refman stdlib
    - git commit -m "Documentation of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
    - git push # TODO: rebase and retry on failure

doc:ml-api:odoc:
  extends: .dune-ci-template
  variables:
    DUNE_TARGET: apidoc
  artifacts:
    paths:
      - _build/log
      - _build/default/_doc/

test-suite:base:
  extends: .test-suite-template
  needs:
    - build:base

test-suite:base+32bit:
  extends: .test-suite-template
  needs:
    - build:base+32bit
  variables:
    OPAM_VARIANT: "+32bit"
  only: *full-ci

test-suite:edge+flambda:
  extends: .test-suite-template
  needs:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  only: *full-ci

test-suite:edge:dune:dev:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  needs:
    - build:edge+flambda:dune:dev
  script:
    - tar xfj _build.tar.bz2
    - make -f Makefile.dune test-suite
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: on_failure
    paths:
      - _build/default/test-suite/logs
    # Gitlab doesn't support yet "expire_in: never" so we use the instance default
    # expire_in: never

.test-suite:ocaml+beta+dune-template:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  script:
    - opam switch create $OCAMLVER --empty
    - eval $(opam env)
    - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git
    - opam update
    - opam install ocaml-variants=$OCAMLVER
    - opam install dune zarith
    - eval $(opam env)
    - export COQ_UNIT_TEST=noop
    - make -f Makefile.dune test-suite
  variables:
    OPAM_SWITCH: base
  artifacts:
    name: "$CI_JOB_NAME.logs"
    when: always
    paths:
      - _build/log
      - _build/default/test-suite/logs
    expire_in: 2 week
  allow_failure: true

# test-suite:4.12+trunk+dune:
#   extends: .test-suite:ocaml+beta+dune-template
#   variables:
#     OCAMLVER: 4.12.0+trunk

test-suite:base+async:
  extends: .test-suite-template
  needs:
    - build:base
  variables:
    COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force"
  timeout: 100m
  allow_failure: true
  only:
    variables:
      - $UNRELIABLE =~ /enabled/

validate:base:
  extends: .validate-template
  needs:
    - build:base

validate:base+32bit:
  extends: .validate-template
  needs:
    - build:base+32bit
  variables:
    OPAM_VARIANT: "+32bit"
  only: *full-ci

validate:edge+flambda:
  extends: .validate-template
  needs:
    - build:edge+flambda
  variables:
    OPAM_SWITCH: edge
    OPAM_VARIANT: "+flambda"
  only: *full-ci

validate:quick:
  extends: .validate-template
  needs:
    - build:quick
  only:
    variables:
      - $UNRELIABLE =~ /enabled/

# Libraries are by convention the projects that depend on Coq
# but not on its ML API

library:ci-argosy:
  extends: .ci-template

library:ci-autosubst:
  extends: .ci-template-flambda

library:ci-bbv:
  extends: .ci-template

library:ci-bedrock2:
  extends: .ci-template-flambda
  variables:
    NJOBS: "1"

library:ci-category_theory:
  extends: .ci-template
  needs:
  - build:base
  - plugin:ci-equations

library:ci-color:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-bignums

library:ci-compcert:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-flocq
  - library:ci-menhir

library:ci-coq_performance_tests:
  extends: .ci-template

library:ci-coq_tools:
  extends: .ci-template

library:ci-coqprime:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-bignums

library:ci-coqtail:
  extends: .ci-template

library:ci-coquelicot:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

library:ci-cross_crypto:
  extends: .ci-template

library:ci-engine_bench:
  extends: .ci-template

library:ci-fcsl_pcm:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

library:ci-fiat_crypto:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-coqprime
  - plugin:ci-bignums
  - plugin:ci-rewriter

library:ci-fiat_crypto_legacy:
  extends: .ci-template-flambda
  allow_failure: true # See https://github.com/coq/coq/wiki/Coq-Call-2020-06-24#adding-back-fiat-crypto-legacy

# We cannot use flambda due to
# https://github.com/ocaml/ocaml/issues/7842, see
# https://github.com/coq/coq/pull/11916#issuecomment-609977375
library:ci-fiat_crypto_ocaml:
  extends: .ci-template
  needs:
  - build:edge+flambda
  - library:ci-coqprime
  - plugin:ci-bignums
  - plugin:ci-rewriter
  - library:ci-fiat_crypto

library:ci-flocq:
  extends: .ci-template-flambda

library:ci-menhir:
  extends: .ci-template-flambda

library:ci-oddorder:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

library:ci-fourcolor:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

library:ci-corn:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-bignums
  - library:ci-math_classes

plugin:ci-gappa:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-flocq

library:ci-geocoq:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

library:ci-hott:
  extends: .ci-template

library:ci-iris:
  extends: .ci-template-flambda
  needs:
    - build:edge+flambda
    - library:ci-autosubst

library:ci-math_classes:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-bignums

library:ci-mathcomp:
  extends: .ci-template-flambda

library:ci-mczify:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

library:ci-sf:
  extends: .ci-template

library:ci-stdlib2:
  extends: .ci-template-flambda

library:ci-tlc:
  extends: .ci-template

library:ci-unimath:
  extends: .ci-template-flambda

library:ci-verdi_raft:
  extends: .ci-template-flambda

library:ci-vst:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-flocq

library:ci-deriving:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

# Plugins are by definition the projects that depend on Coq's ML API

plugin:ci-aac_tactics:
  extends: .ci-template

plugin:ci-bignums:
  extends: .ci-template-flambda

plugin:ci-coq_dpdgraph:
  extends: .ci-template

plugin:ci-coqhammer:
  extends: .ci-template-flambda

plugin:ci-elpi:
  extends: .ci-template

plugin:ci-equations:
  extends: .ci-template

plugin:ci-fiat_parsers:
  extends: .ci-template

plugin:ci-metacoq:
  extends: .ci-template
  needs:
  - build:base
  - plugin:ci-equations

plugin:ci-mtac2:
  extends: .ci-template

plugin:ci-paramcoq:
  extends: .ci-template

plugin:ci-perennial:
  extends: .ci-template-flambda

plugin:plugin-tutorial:
  stage: build
  except:
    variables:
      - $ONLY_WINDOWS == "true"
  interruptible: true
  script:
    - ./configure -profile devel -warn-error yes
    - make -j "$NJOBS" plugin-tutorial

plugin:ci-quickchick:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp

plugin:ci-reduction_effects:
  extends: .ci-template

plugin:ci-relation_algebra:
  extends: .ci-template

plugin:ci-rewriter:
  extends: .ci-template-flambda

plugin:ci-vscoq:
  extends: .ci-template