.gitlab-ci.yml

image: $BASE_IMAGE

include:
  - local: '/dev/ci/gitlab-modes/protected-mode.yml'
    rules:
      - if: $CI_COMMIT_BRANCH == "master"
      - if: $CI_COMMIT_BRANCH =~ /^v.*\..*$/

  - local: "/dev/ci/gitlab-modes/normal-mode.yml"
    rules:
      - if: $CI_COMMIT_BRANCH != "master" && $CI_COMMIT_BRANCH !~ /^v.*\..*$/

  - local: "/dev/ci/gitlab-modes/tagged-runners.yml"
    rules:
      - if: $TAGGED_RUNNERS

  - local: "/dev/ci/gitlab-modes/untagged-runners.yml"
    rules:
      - if: $TAGGED_RUNNERS == null

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

stages:
  - docker
  - build
  - deploy

# We set "needs" to contain all transitive dependencies. We include the
# transitive dependencies as otherwise we don't get their artifacts
# (eg if color had just needs: bignums it wouldn't get the artifact containing coq)

# some default values
variables:
  # Format: image_name-V$DATE-$hash
  # $DATE is so we can tell what's what in the image list
  # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
  # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10)
  # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10)
  BASE_CACHEKEY: "old_ubuntu_lts-V2023-06-30-8ca33f9dfd"
  EDGE_CACHEKEY: "edge_ubuntu-V2023-08-28-93124ee272"
  BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY"
  EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY"

  # Used to select special compiler switches such as flambda, 32bits, etc...
  OPAM_VARIANT: ""
  GIT_DEPTH: "10"

before_script:
  - dev/ci/gitlab-section.sh start before_script before_script
  - cat /proc/{cpu,mem}info || true
  - ulimit -s
  - ls -a # figure out if artifacts are around
  - printenv -0 | sort -z | tr '\0' '\n'
  - opam switch set -y "${COMPILER}${OPAM_VARIANT}"
  - eval $(opam env)
  - opam list
  - opam config list
  - dune printenv --root .
  - dev/tools/check-cachekey.sh
  - dev/ci/gitlab-section.sh end before_script

# Regular "release" build of Coq, with final installed layout
.build-template:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  variables:
    COQIDE: "opt"
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _install_ci
      # All those are for the test-suite jobs, to be discarded soon
      - config/Makefile
      - config/coq_config.py
      - config/coq_config.ml
      - config/dune.c_flags
    expire_in: 1 month
  script:
    - PKGS=coq-core,coq-stdlib,coqide-server,coq
    - if [ "$COQIDE" != "no" ]; then PKGS=${PKGS},coqide; fi
    - dev/ci/gitlab-section.sh start coq.clean coq.clean
    - make clean # ensure that `make clean` works on a fresh clone
    - dev/ci/gitlab-section.sh end coq.clean

    - dev/ci/gitlab-section.sh start coq.config coq.config
    - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" $COQ_EXTRA_CONF
    - dev/ci/gitlab-section.sh end coq.config

    - dev/ci/gitlab-section.sh start coq.build coq.build
    - make dunestrap
    - dune build -p $PKGS
    - dev/ci/gitlab-section.sh end coq.build

    - dev/ci/gitlab-section.sh start coq.install coq.install
    - dune install --prefix="$(pwd)/_install_ci" $(sed -e 's/,/ /g' <<< ${PKGS})
    - dev/ci/gitlab-section.sh end coq.install

# Developer build, with build layout. Faster and useful for those
# jobs needing _build
.build-template:base:dev:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  script:
    - make $DUNE_TARGET
    - find _build -name '*.vio' -exec rm -f {} \;
    - tar cfj _build.tar.bz2 _build
  variables:
    DUNE_TARGET: world
  artifacts:
    name: "$CI_JOB_NAME"
    when: always
    paths:
      - _build/log
      - _build.tar.bz2
      - theories/dune
      - user-contrib/Ltac2/dune
    expire_in: 1 month

.doc-template:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  needs:
    - build:base:dev
  script:
    - ulimit -S -s 16384
    - tar xfj _build.tar.bz2
    - make "$DUNE_TARGET"
  artifacts:
    when: always
    name: "$CI_JOB_NAME"
    expire_in: 2 months

# The used Coq must be set explicitly for each job with "needs:".
# We add a spurious dependency `not-a-real-job` that must be
# overridden otherwise the CI will fail (to help debugging missing needs).

# set "needs" when using
.test-suite-template:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  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
  interruptible: true
  extends: .auto-use-tags
  needs:
    - not-a-real-job
  script:
    # exit 0: workaround for https://gitlab.com/gitlab-org/gitlab/issues/202505
    # the validate:vio job is sometimes started before build:vio, 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

# This template defaults to "needs: build:base"
# Remember to include it as a transitive dependency if you want additional "needs:"
.ci-template:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  script:
    - ulimit -S -s 16384           # For flambda + native
    - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}"
  artifacts:
    name: "$CI_JOB_NAME"
    paths:
      - _build_ci
    when: always
  needs:
    - build:base
  only: &full-ci
    variables:
      - $FULL_CI == "true"

.ci-template-flambda:
  extends: .ci-template
  image: $EDGE_IMAGE
  needs:
    - build:edge+flambda
  variables:
    OPAM_VARIANT: "+flambda"

.deploy-template:
  stage: deploy
  extends: .auto-use-tags
  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"

.pkg:opam-template:
  stage: build
  image: $EDGE_IMAGE
  interruptible: true
  extends: .auto-use-tags
  # OPAM will build out-of-tree so no point in importing artifacts
  script:
    - 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 .
  variables:
    OPAM_VARIANT: "+flambda"
  only: *full-ci

.nix-template:
  stage: build
  needs: []
  interruptible: true
  image: nixos/nix:latest
  extends: .auto-use-tags
  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

##############################################################################
########################## End of templates ##################################
##############################################################################

docker-boot:
  stage: docker
  image: docker:stable
  services:
    - docker:dind
  before_script: []
  script:
    - dev/tools/check-cachekey.sh
    - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
    - cd dev/ci/docker/old_ubuntu_lts
    - if docker pull "$BASE_IMAGE"; then echo "Base image prebuilt!"; else docker build -t "$BASE_IMAGE" .; docker push "$BASE_IMAGE"; fi
    - cd ../edge_ubuntu
    - if docker pull "$EDGE_IMAGE"; then echo "Edge image prebuilt!"; else docker build -t "$EDGE_IMAGE" .; docker push "$EDGE_IMAGE"; fi
  except:
    variables:
      - $SKIP_DOCKER == "true"
  tags:
    - docker

build:base:
  extends: .build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler yes"
  only: *full-ci

# no coqide for 32bit: libgtk installation problems
build:base+32bit:
  extends: .build-template
  variables:
    OPAM_VARIANT: "+32bit"
    COQ_EXTRA_CONF: "-native-compiler yes"
    COQIDE: "no"
  only: *full-ci

build:edge+flambda:
  extends: .build-template
  image: $EDGE_IMAGE
  variables:
    OPAM_VARIANT: "+flambda"
    COQ_EXTRA_CONF: "-native-compiler yes"

build:base:dev:
  extends: .build-template:base:dev

build:base+async:
  extends: .build-template
  variables:
    COQ_EXTRA_CONF: "-native-compiler yes"
    COQ_DUNE_EXTRA_OPT: "-async"
  after_script:
    - dmesg > dmesg.txt
  allow_failure: true # See https://github.com/coq/coq/issues/9658
  only:
    variables:
      - $UNRELIABLE =~ /enabled/ && $FULL_CI == "true"
  artifacts:
    when: always
    paths:
      - _install_ci
      # All those are for the test-suite jobs, to be discarded once we have dune for the test-suite
      - config/Makefile
      - config/coq_config.py
      - config/coq_config.ml
      - config/dune.c_flags
      - dmesg.txt
  timeout: 1h 30min

build:vio:
  extends: .build-template:base:dev
  variables:
    COQ_EXTRA_CONF: "-native-compiler no"
    COQ_DUNE_EXTRA_OPT: "-vio"
    DUNE_TARGET: "vio world"
  after_script:
    - dmesg > dmesg.txt
  allow_failure: true # See https://github.com/coq/coq/issues/9637
  only:
    variables:
      - $UNRELIABLE =~ /enabled/
  artifacts:
    when: always
    paths:
      - _install_ci
      - dmesg.txt

lint:
  stage: build
  image: $EDGE_IMAGE
  script: dev/lint-repository.sh
  extends: .auto-use-tags
  variables:
    GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
    OPAM_VARIANT: "+flambda"

# pkg:opam:
#   extends: .pkg:opam-template

pkg:opam:native:
  extends: .pkg:opam-template
  before_script:
    - opam install -y coq-native
  after_script:
    - eval $(opam env)
    - echo "Definition f x := x + x." > test_native.v
    - coqc -native-compiler yes test_native.v
    - test -f .coq-native/Ntest_native.cmxs

# broken, see eg https://gitlab.com/coq/coq/-/jobs/1754045983
# pkg:nix:deploy:
#   extends: .nix-template
#   environment:
#     name: cachix
#     url: https://coq.cachix.org
#   script:
#     - nix-build https://coq.inria.fr/nix/toolbox --argstr job coq --arg override "{coq = coq:$CI_COMMIT_SHA;}" -K | cachix push coq
#   only:
#     refs:
#       - master
#       - /^v.*\..*$/
#     variables:
#       - $CACHIX_AUTH_TOKEN

# 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_AUTH_TOKEN && $CACHIX_DEPLOYMENT_KEY
#        # if the $CACHIX_AUTH_TOKEN variable isn't set, the job it depends on doesn't exist
#   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
  variables:
    DUNE_TARGET: refman-html
  artifacts:
    paths:
      - _build/log
      - _build/default/doc/refman-html

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

doc:stdlib:
  extends: .doc-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
    - doc:stdlib
  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 _build/default/doc/stdlib/html _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: .doc-template
  variables:
    DUNE_TARGET: apidoc
  artifacts:
    paths:
      - _build/log
      - _build/default/_doc/

test-suite:base:
  extends: .test-suite-template
  needs:
    - build:base
  only: *full-ci

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
  image: $EDGE_IMAGE
  needs:
    - build:edge+flambda
  variables:
    OPAM_VARIANT: "+flambda"

test-suite:base:dev:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  needs:
    - build:base:dev
  script:
    - tar xfj _build.tar.bz2
    - make test-suite
  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
  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 test-suite
  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:base+async:
  extends: .test-suite-template
  needs:
    - build:base
  variables:
    COQEXTRAFLAGS: "-async-proofs on -async-proofs-cache force"
  allow_failure: true
  only:
    variables:
      - $UNRELIABLE =~ /enabled/ && $FULL_CI == "true"

validate:base:
  extends: .validate-template
  needs:
    - build:base
  only: *full-ci

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

validate:edge+flambda:
  extends: .validate-template
  image: $EDGE_IMAGE
  needs:
    - build:edge+flambda
  variables:
    OPAM_VARIANT: "+flambda"

validate:vio:
  extends: .validate-template
  needs:
    - build:vio
  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"
  timeout: 2h

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_1

library:ci-fiat_crypto:
  extends: .ci-template-flambda
  variables:
    COQEXTRAFLAGS: "-async-proofs-tac-j 0"
  needs:
  - build:edge+flambda
  - library:ci-coqprime
  - plugin:ci-bignums
  - plugin:ci-rewriter
  timeout: 3h

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
  timeout: 1h 30min

# 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-flambda
  needs:
  - build:edge+flambda
  - library:ci-coqprime
  - plugin:ci-bignums
  - plugin:ci-rewriter
  - library:ci-fiat_crypto
  artifacts:
    paths: [] # These artifacts would go over the size limit

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
  - plugin:ci-elpi_hb
  - library:ci-mathcomp

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

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

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
  needs:
  - build:edge+flambda
  - plugin:ci-elpi_hb  # for Hierarchy Builder

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

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

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

library:ci-finmap:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp_1

library:ci-bigenough:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp_1

library:ci-analysis:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp_1
  - library:ci-finmap
  - library:ci-bigenough
  - plugin:ci-elpi_hb  # for Hierarchy Builder

library:ci-neural_net_interp:
  extends: .ci-template

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

library:ci-itree:
  extends: .ci-template-flambda
  needs:
    - build:edge+flambda
    - library:ci-paco

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
  variables:
    NJOBS: "1"
  needs:
  - build:edge+flambda
  - library:ci-flocq
  - library:ci-menhir
  - library:ci-compcert
  timeout: 2h

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

library:ci-mathcomp_word:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp_1

library:ci-jasmin:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-mathcomp_1
  - library:ci-mathcomp_word

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

library:ci-http:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - library:ci-menhir
  - library:ci-itree
  - plugin:ci-quickchick

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

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

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

plugin:ci-itauto:
  extends: .ci-template

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

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

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

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

plugin:ci-elpi_hb:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda

plugin:ci-elpi_test:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-elpi_hb

plugin:ci-hb_test:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-elpi_hb

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

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

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

plugin:ci-lean_importer:
  extends: .ci-template

plugin:ci-ltac2_compiler:
  extends: .ci-template

plugin:ci-metacoq:
  extends: .ci-template
  needs:
  - build:base
  - plugin:ci-equations
  timeout: 1h 30min

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

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

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

plugin:plugin-tutorial:
  stage: build
  interruptible: true
  extends: .auto-use-tags
  script:
    - ./configure -prefix "$(pwd)/_install_ci" -warn-error yes
    - make -j "$NJOBS" plugin-tutorial

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

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

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

plugin:ci-relation_algebra:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-elpi_hb
  - library:ci-mathcomp
  - plugin:ci-aac_tactics

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

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

plugin:ci-serapi_test:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-elpi_hb
  - library:ci-mathcomp_1
  - plugin:ci-serapi

plugin:ci-coq_lsp:
  extends: .ci-template-flambda
  needs:
  - build:edge+flambda
  - plugin:ci-serapi

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

plugin:ci-smtcoq:
  extends: .ci-template

plugin:ci-stalmarck:
  extends: .ci-template

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

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