# This file used to contain configuration to also build documentation and CoqIDE,
# run the test-suite and the validate targets,
# including with 32-bits architecture or bleeding-edge compiler.

defaults:
  params: &params
    # Following parameters are used in Coq CircleCI Job (using yaml
    # reference syntax)
    working_directory: ~/coq
    docker:
      - image: $CI_REGISTRY_IMAGE:$CACHEKEY

  environment: &envvars
    CACHEKEY: "bionic_coq-V2018-07-11-V2"
    CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq

version: 2

before_script: &before_script
  name: Setup OPAM Switch
  command: |
    echo export TERM=xterm >> ~/.profile
    source ~/.profile
    echo . ~/.profile >> $BASH_ENV
    printenv | sort
    opam switch "$COMPILER"
    opam config list
    opam list

.build-template: &build-template
  <<: *params
  steps:
    - checkout
    - run: *before_script
    - run: &build-clean
        name: Clean
        command: |
          make clean # ensure that `make clean` works on a fresh clone
    - run: &build-configure
        name: Configure
        command: |
          ./configure -local -native-compiler ${NATIVE_COMP} -coqide no
    - run: &build-build
        name: Build
        command: |
          make -j ${NJOBS} byte
          make -j ${NJOBS}
          make test-suite/misc/universes/all_stdlib.v
    - persist_to_workspace:
        root: &workspace ~/
        paths:
          - coq/

  environment:
    <<: *envvars
    NATIVE_COMP: "yes"

.ci-template: &ci-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: &attach_workspace
        at: *workspace

    - run:
        name: Test
        command: |
          dev/ci/ci-wrapper.sh ${CIRCLE_JOB}
    - persist_to_workspace:
        root: *workspace
        paths:
          - coq/
  environment: *envvars

# Defines individual jobs, see the workflows section below for job orchestration
jobs:

  # Build and prepare test environment
  build: *build-template

  bignums:
    <<: *ci-template

  color:
    <<: *ci-template

  compcert:
    <<: *ci-template

  coq-dpdgraph:
    <<: *ci-template

  coquelicot:
    <<: *ci-template

  cross-crypto:
    <<: *ci-template

  elpi:
    <<: *ci-template

  equations:
    <<: *ci-template

  geocoq:
    <<: *ci-template

  fcsl-pcm:
    <<: *ci-template

  fiat-crypto:
    <<: *ci-template

  fiat-parsers:
    <<: *ci-template

  flocq:
    <<: *ci-template

  math-classes:
    <<: *ci-template

  corn:
    <<: *ci-template

  formal-topology:
    <<: *ci-template

  hott:
    <<: *ci-template

  iris-lambda-rust:
    <<: *ci-template

  ltac2:
    <<: *ci-template

  math-comp:
    <<: *ci-template

  mtac2:
    <<: *ci-template

  pidetop:
    <<: *ci-template

  sf:
    <<: *ci-template

  unimath:
    <<: *ci-template

  vst:
    <<: *ci-template

workflows:
  version: 2

  # Run on each push
  main:
    jobs:
      - build

      - bignums: &req-main
          requires:
            - build
      - color:
          requires:
            - build
            - bignums
      # - compcert: *req-main
      # - coq-dpdgraph: *req-main
      # - coquelicot: *req-main
      # - cross-crypto: *req-main
      # - elpi: *req-main
      # - equations: *req-main
      # - geocoq: *req-main
      # - fcsl-pcm: *req-main
      # - fiat-crypto: *req-main
      # - fiat-parsers: *req-main
      # - flocq: *req-main
      - math-classes:
          requires:
            - build
            - bignums
      # - mtac2: *req-main
      - corn:
          requires:
            - build
            - math-classes
      - formal-topology:
          requires:
            - build
            - corn
      # - hott: *req-main
      # - iris-lambda-rust: *req-main
      # - ltac2: *req-main
      # - math-comp: *req-main
      # - pidetop: *req-main
      # - sf: *req-main
      # - unimath: *req-main
      # - vst: *req-main